11institutetext: The University of Manchester, Manchester, UK
11email<EMAIL_ADDRESS>
11email<EMAIL_ADDRESS>Arm®
22email<EMAIL_ADDRESS>
# Verifying components of Arm® Confidential Computing Architecture with ESBMC

Tong Wu 11 0000-0002-0986-4150 Shale Xiong 22 0000-0001-9312-195X Edoardo
Manino 11 0000-0001-9312-195X Gareth Stockwell 22 0009-0004-1773-2846 Lucas C.
Cordeiro 11 0000-0002-6235-4272

###### Abstract

_Realm Management Monitor_ (RMM) is an essential firmware component within the
recent Arm _Confidential Computing Architecture_ (Arm CCA). Previous work
applies formal techniques to verify the specification and prototype reference
implementation of RMM. However, relying solely on a single verification tool
may lead to the oversight of certain bugs or vulnerabilities. This paper
discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo
Theories (SMT)-based software model checker to further enhance RRM
verification. We demonstrate ESBMC’s ability to precisely parse the source
code and identify specification failures within a reasonable time frame.
Moreover, we propose potential improvements for ESBMC to enhance its
efficiency for industry engineers. This work contributes to exploring the
capabilities of formal verification techniques in real-world scenarios and
suggests avenues for further improvements to better meet industrial
verification needs.

###### Keywords:

Formal verification Software model checking Software testing Firmware
Security.

##  1 Introduction

The rise of Confidential Computing is driven by the need to secure
computations in Cloud Computing, where sensitive information is delegated to a
third party, posing potential security risks [22]. For example, hundreds of
millions of Facebook user records were exposed on Amazon cloud server [20].

Confidential Computing technologies, including Arm _Confidential Computing
Architecture_ (Arm CCA) [15], introduce protected execution environments, for
example _Realms_ in Arm CCA, to ensure confidentiality and integrity of
sensitive information. In particular, Arm CCA allows multiple Realms to
execute in parallel; to manage all instances, Arm CCA then introduces a new
privileged firmware component called _Realm Management Monitor_ (RMM). RMM
also provides a necessary interface to the outside, non-secure world. Arm is
committed to specifying the behavior of RMM [16] and providing an
implementation in C, and the code is already open-sourced to the community
[17].

RMM is a critical component, and any end-user must trust it. Arm provides a
specification [16] for all the interfaces via pairs of pre/post conditions. To
verify the correctness of the RMM implementation concerning the RMM
specification, formal methods such as interactive theorem provers and symbolic
model checking can be applied to automate the verification workflow [14]. Arm
engineers automatically generate a verification harness from a machine-
readable specification of the RMM by evaluating the pre- and post-conditions
to constrain the inputs and outputs. This harness can be consumed by a
software verification tool such as _C Bounded Model Checker_ (CBMC) [11, 13].
Arm researchers and engineers are gradually deploying these auto-generated
verification harnesses and CBMC in the CI/CD system. Several violations in the
implementations detected by CBMC have been confirmed and fixed by Arm
engineers, thus demonstrating the value of software model checking techniques
[7] in strengthening safety-critical systems.

Given the fact that there exist some violated properties in the current draft
implementation of the RMM [7], we are keen to explore the following questions:

  * $\bullet$

Is the existing verification enough to secure RMM?

  * $\bullet$

If not, can other state-of-the-art techniques find additional violations?

To explore these questions, we further apply ESBMC, an efficient model checker
based on SMT theories that can automatically detect or prove the absence of
runtime errors in software written in C/C++, Kotlin, Python, and Solidity [9,
18]. According to the recent Competitions on Software Verification (SV-COMP)
[2, 3], ESBMC consistently outperforms CBMC in proving more safety properties
while producing fewer incorrect results. However, there is little evidence of
whether this superior performance could uncover more vulnerabilities in real-
world low-level software systems. Through our exploration of ESBMC on some RMM
verification cases, we achieved the following contribution:

  * $\bullet$

We reproduced the same failures reported by CBMC, which were confirmed by Arm
engineers previously.

  * $\bullet$

We identified inconsistent results from CBMC and reported them to the
developers.

  * $\bullet$

We found 23 new violations in the RMM code that only ESBMC can detect.

  * $\bullet$

We showed that the verification performance could be significantly improved by
efficiently configuring the bounds for each loop in the program.

  * $\bullet$

We highlighted the challenge of checking multiple properties and contributed
to its development within ESBMC.

##  2 Background

###  2.1 Bounded Model Checking (BMC)

SAT/SMT-based BMC is a formal verification technique to falsify or prove the
correctness of finite-state systems [5]. This method explores a system’s state
space up to a specified depth or bound $k$, searching for potential errors or
violations within that limited scope. Then the program is encoded into an
SAT/SMT formula, and it is satisfiable iff there exists a counterexample that
violates the property [4].

As a BMC tool, ESBMC implements various algorithms for bounded and incremental
verification [1, 6, 8]:  (1) incremental BMC, which unrolls the loops and
checks the property incrementally;  (2) k-induction [10] proof-rule algorithm,
which aims to prove the safety based on induction; and  (3) default BMC
approach that bounds the program up to a given depth and call the SMT solver
once to solve the entire SMT formula.

Similar to CBMC, ESBMC takes an RMM test case as input and checks the safety
of the properties in the given program. In particular, ESBMC can check for
user-defined assertions, pointer safety, buffer overflow, data races, and so
on through configurations. The ESBMC documentation about the supported
safety/security properties, underlying verification algorithms, and integrated
SMT solvers is available
online.111https://ssvlab.github.io/esbmc/documentation.html

###  2.2 Realm Management Monitor

EL-3EL-2EL-1EL-0RootMonitor Realm Management
---
Monitor (RMM)
Hypervisor Secure Partition
---
Manager (SPM)
KernelKernelAppAppRVMRVMVMOS KernelTrusted OSSecure
PartitionAppAppTATARealmNon-secureSecure Figure 1: An architecture of an Arm
CCA [7]. The physical memory space is separated into four worlds: Non-secure,
Secure, Root and the Realm.

Fig. 1 illustrates the architecture of Arm CCA; more can be learned from [15].
Executions Arm’s _Processing Element_ (PE) is associated with levels EL0 to
EL3, where user-space executes at EL0 and most privileged low-level firmware,
or monitor, executes at EL3. The physical memory space also separates into
four parts, or four worlds, namely, _Non-secure_ World, _Secure_ World, _Root_
World, and the newly-introduced _Realm_. In the _Realm_ World, an end-user
application, referred to as a realm, is executed at the level of EL0 and EL1.
To administer Realms, Arm CCA introduces a new privileged firmware component
called the _Realm Management Monitor_ (RMM), executing at EL2 in the Realm
world, which acts as a separation kernel isolating Realms from each other.
Also, RMM provides interfaces to the Non-secure World for managing and
scheduling realms indirectly.

Fig. 2 illustrates an example of RMM specification of the RMI_GRANULE_D
ELEGATE command.222This is an example from the drafted specification version
accessed on early 2022 [17].

Figure 2: RMI_GRANULE_DELEGATE command specification (draft) [7]

The specification takes a single granule address as input from the Host (the
addr parameter, in general purpose register X1, is the physical address
location of the granule to be delegated). If the corresponding granule
metadata is UNDELEGATED, meaning that the granule is not in the REALM PAS, and
it is currently in the NS PAS, then the granule is moved to the REALM PAS. The
failure conditions consist of several pairs of pre/post conditions, each of
which is a possible error condition. When no failure occurs, the success
conditions describe the expected updates to the RMM machine state.

##  3 RMM Verification with ESBMC

Listing 1 illustrates a C example of a verification harness generated from the
RMM specification. It initializes a non-deterministic global state from line
$1$ to $7$. In line $9$, it executes the actual command of the specification.
Line $8$ and line $10$ evaluate the pre- and post-conditions using the Boolean
variables failure_src_align_pre and failure_src_align_post, respectively.
Lines 11-16 are the boolean conditions of the pre- and post-conditions.
Finally, the assertion in line 17 checks the post-condition if the pre-
condition fails. From this verification harness, we can use any off-the-shelf
software model checker to automatically check the assertion for the post-
condition. Properly choosing the underlying verification strategy and
parameters to configure ESBMC is essential to achieving efficient verification
of RMM. Here, we introduce two main verification techniques available in
ESBMC: bounded verification to unwind each loop occurring in the program with
a different upper bound and multi-property check to verify all properties
incrementally using the underlying SMT solver.

⬇

1struct tb_regs __tb_regs = __tb_arb_regs();

2__tb_regs.X0 = SMC_RMM_DATA_CREATE;

3__tb_regs.X1 = nondet_uint64_t(); // data

4__tb_regs.X2 = nondet_uint64_t(); // rd

5__tb_regs.X3 = nondet_uint64_t(); // map_addr

6__tb_regs.X4 = nondet_uint64_t(); // src

7__init_global_state(__tb_regs.X0); // Generate non-deterministic state

8bool failure_src_align_pre = !AddrIsGranuleAligned(src); // Precondition

9uint64_t result = tb_handle_smc(&__tb_regs); // Execute command

10bool failure_src_align_post = ResultEqual(result, RMI_ERROR_INPUT); //
Postcondition

11// Failure condition assertions (excerpt)

12bool prop_failure_src_align_ante = failure_src_align_pre;

13__COVER(prop_failure_src_align_ante);

14if (prop_failure_src_align_ante) {

15bool prop_failure_src_align_cons = failure_src_align_post;

16__COVER(prop_failure_src_align_cons);

17__ASSERT(prop_failure_src_align_cons , "prop_failure_src_align_cons"); }

Listing 1: Verification harness from the specification [7]

###  3.1 Bounded Verification

We can configure the loops’ unrolling depth for BMC tools to reduce the
program state space for refutation/verification. In particular, we must limit
the unwinding bound to avoid an unbounded loop being unrolled infinitely.
However, we must carefully configure the bounds for complex programs such as
with nested loops because the verification time could increase dramatically.
Both ESBMC and CBMC support setting different upper bounds for each loop in
the program. While this setup can be complicated compared to setting a unified
bound for all loops or unrolling them incrementally, it can result in smaller
state spaces and faster checking speeds, as shown in our experimental
evaluation. This happens because iteratively unrolling loops and calling a
solver via incremental and induction methods can be costly, especially for
programs containing various nested loops. We refer the reader to our previous
work about handling loops in BMC for a detailed discussion about this topic
[1, 8], including comparisons to state-of-the-art verification methods. To
verify the components of the Arm Confidential Computing Architecture, which is
the focus of this paper, our preliminary experiments on incremental BMC have
shown a significant performance difference when we set different upper bounds
for each loop, which will be presented in Section 4.

###  3.2 Multi-Property Check

Most real-world verification instances contain multiple assertions [21]. This
is because any non-trivial program must satisfy several invariants at once.
However, multiple assertions create a crucial dilemma for software
verification tools: whether we encode them all in a single large formula or
split them into separate smaller ones. A single large formula is faster to
solve than smaller ones because the latter have multiple (or incremental)
queries to a solver [18]. However, it also raises the problem that the
counterexample in a single formula can only expose one property violation in
the program.

By default, ESBMC runs in single property check mode, which encodes all
verification conditions (VCs) into one single SMT formula and terminates once
if it finds a violation by the underlying SMT solver across the program path.
ESBMC uses Boolector as its default SMT solver [19]. Recently, ESBMC added
verification support for multi-property checks (see Listing 2) to report all
property violations for a single call. During the multi-property check, each
property assumes the other properties are unreachable by keeping the current
encoded property. In the example of Listing 2, none of the two assertions hold
because the value of $a$ is non-deterministic and can reach both cases to
trigger the assertion. ESBMC, in single property check mode, will terminate
once it finds a violation, e.g., `assert(a>1)`, while multi-property check
mode aims at reporting both of these violations.

⬇

#include <assert.h>

extern int nondet_int();

int main() {

int a = nondet_int();

switch (a) {

case 0: assert(a > 0); break;

case 1: assert(a > 1); break;

default: return 0;

}

}

Listing 2: A program with two property violations.

##  4 Experiment Results

In this section, we evaluate the capability of ESBMC single- and multi-
property checks on RMM.

#### Experimental Setup.

We conduct the experiments on a Ubuntu OS with $16$GB memory and an Intel i$7$
processor, limiting the timeout to $5000$ s. The benchmarks are listed in
Table 1 and are open-source [17]. We compare the results between ESBMC v7.4
and CBMC v5.94. Unless we state otherwise, we run ESBMC with the flag
\--unwindset. This flag ensures it uses the same default approach of CBMC,
i.e., unrolling each loop to the maximum number of loop iterations occurring
in the program without producing under-approximation. ESBMC adds explicit
assertions to check whether the loop is fully unrolled.

#### Number of Violations Found.

Table 1 shows the total number of failures found by ESBMC and CBMC. The main
finding is that ESBMC reports more failures than CBMC in three test cases.

#### Confirmed and Unconfirmed Violations.

We are still working on confirming every bug reported by ESBMC due to the
complexity and readability of the output traces. In particular, ESBMC provides
traces that describe hundreds or thousands of states, where each state
contains information about the program location and the value of the
local/global variables. Still, we confirmed a correct positive in the test
case `RMI_REALM_DESTROY`, which is caused by converting a pointer to an
integer and can affect the global verification conditions in that test case.
The actual RMM code was fixed, though waiting for code review, before we
conducted this experiment, as it involved undefined behavior due to that
conversion. We present a characterized example in Listing 3, and we have
reported the issue to the CBMC team so that they could improve their verifier.
A CBMC developer has confirmed the bug in their memory model (see
https://github.com/diffblue/cbmc/issues/8161).

0510152025$\infty$$0$$100$$200$$300$$400$$500$$600$$700$$800$$900$k-stepTime
(s)–incremental-bmc–unwindset

Figure 3: Verification time for different k-steps during each loop rolling.
The red node at the bottom left represents unrolling the loops completely
until the given bounds.

#### Impact of step $k$ in incremental BMC.

ESBMC provides an option to set the $k$-step when incrementally unrolling the
loops. For example, a $k$-step of $5$ will unfold a given loop incrementally
as $5$, $10$, $15$, and $20$ (maximum $k$-step). We conduct an extra
experiment on a single but representative RMM test case to check the impact of
step $k$ in incremental BMC. In Fig. 3, it can be seen that although
increasing the k-steps can reduce looping unrolling and solving time since we
can find a property violation faster, it is not as efficient as ESBMC non-
iterative mode, i.e., via unwindset that unrolls the loops directly to the
upper bound. These results explain our chosen methodology as described in
Section 3.1.

⬇

#include<assert.h>

int arr[8] = {1,2,3,4,5,6,7,8};

int main() {

int *a = &arr[7];

if((unsigned long)a >= (unsigned long)(-4095))

assert((unsigned long)(-1*(long)a) < 6); //esbmc fails, cbmc success

}

Listing 3: Pointer to integer convertion example extracted from rmm, where the assertion should fail if the address falls into a negative value, for example, -2048. Table 1: Verification results of multi-property checks using ESBMC and CBMC.  Command | Assert Fail | VCCs/Solver Calls
---|---|---
ESBMC | CBMC | ESBMC | CBMC
`RMI_REC_DESTROY` | 20 | 20 | 113/113 | 142/19
`RMI_GRANULE_DELEGATE` | safe | safe | 54/54 | 132/2
`RMI_GRANULE_UNDELEGATE` | 1 | 1 | 45/45 | 132/1
`RMI_REALM_ACTIVATE` | 3 |  safe | 53/53 | 140/1
`RMI_REALM_DESTROY` | 17 |  1 | 114/114 | 148/2
`RMI_REC_AUX_COUNT` | 1 | 1 | 48/48 | 139/2
`RMI_FEATURES` | safe | safe | 21/21 | 125/1
`RMI_DATA_DESTROY` | >=26 |  22 | 82/82 | 151/18

#### Performance Comparison.

Fig. 4 illustrates the verification time of the test cases for three runs:
ESBMC single property check, CBMC multi-property check, and ESBMC multi-
property check. Note that the default option of CBMC always checks all
properties in one execution, which is relevant when verifying industrial code.
CBMC and ESBMC single property checks can finish most verification tasks
within a few seconds. However, the ESBMC multi-property check needs a few
minutes for each task and even longer for the last case in the figure, which
has exceeded the timeout of $5000$ s. Table 1 provides an insight into the
performance difference. ESBMC naively calls an SMT solver when there is a
generated SMT formula (per property to check), and it takes time to solve them
individually. Meanwhile, CBMC can exploit the power of incremental SAT solving
by MiniSAT to reuse solved instances for new problems [12]. Another important
factor is that CBMC implements a string solver to solve frequent string
operations at RMM code, while ESBMC has not implemented one yet, which results
in a performance slowdown for strings.

RMI_REC_DESTROYRMI_GRANGULE_DELEGATERMI_GRANGULE_UNDELEGATERMI_REALM_ACTIVATERMI_REALM_DESTROYRMI_REC_AUX_COUNTRMI_FEATURESRMI_DATA_DESTROYRTT_MAP_UNPROTECTED$10$$100$$1{,}000$Time
(s)ESBMC-singleCBMC-multiESBMC-multi

Figure 4: Experiment result, where x-axis represents the RMM testcases, and
y-axis represents the verification time in seconds. Different colors: blue on
the left is for ESBMC single-property check, red on the middle is for CBMC
multi-property check, and yellow on the right is for ESBMC multi-property
check.

#### Syntax Errors.

In addition to the correctness and performance, there exists an interesting
aspect related to the deployed front-end parsers: CBMC uses a modified C
parser, while ESBMC implements Clang API to transform the source code into
Clang AST [9], without having details of the input program compiled away. The
latter can do strict and elegant code syntax checks before starting model
checking. ESBMC can also provide compilation error messages as expected from a
compiler and leverage Clang’s static analyzer to provide meaningful warnings
when parsing the program. For example, consider Listing 4 that illustrates an
example from the RMM implementation, where a declaration of struct object is
in the switch case but without curly braces. ESBMC reports the error using
Clang, while the C parser in CBMC ignores it.

⬇

...

case SMC_RMM_RTT_READ_ENTRY:

struct smc_result rst;

smc_rtt_read_entry(*X1, *X2, *X3, &rst);

result = rst.x[0]; *X1 = rst.x[1]; *X2 = rst.x[2];

*X3 = rst.x[3]; *X4 = rst.x[4];

break;

...

Listing 4: Code segement did not compile for Clang since it cannot declare
variables inside a case block without enclosing it in braces.

##  5 Conclusions

We present our application of ESBMC to verify newly introduced RMM components
in Arm CCA. On the one hand, we show that to ensure firmware correctness, we
can fully verify it by applying various techniques, each with its strengths
and weaknesses. In our experiment, we applied ESBMC and found more violation
properties than CBMC. On the other hand, we show the community that we have to
write more scalable verifiers to check large and complex code bases for multi-
property checks. In addition, we recommend that software verifiers connect
their verification algorithms with industrial-strength compilers, as we find
that self-developed parsers may not be precise enough. Lastly, we should not
only focus on the verification algorithms but also try to produce more
readable verification results to promote the power of formal verification
techniques in the software industry. Future work for ESBMC includes more
efficient algorithms for faster SMT solving for multiple property verification
and checking data races in multi-threaded programs.

## Acknowledgments

The work in this paper is partially funded by the Arm Center of Excellence at
the University of Manchester, UK, EPSRC grants EP/T026995/1, EP/V000497/1, EU
H2020 ELEGANT 957286, and Soteria project awarded by the UK Research and
Innovation for the Digital Security by Design (DSbD) Programme. We acknowledge
Franz Brauße and Chenfeng Wei, who helped refine ESBMC for RMM verification.
We would also like to thank engineers from tf-rmm team
(https://www.trustedfirmware.org/projects/tf-rmm/).

##  Appendix 0.A Appendix

This section lists the details from above results where ESBMC reports more
failures from RMM testcases than CBMC.

Table 2: Unique results from ESBMC No. | Location | Description
---|---|---
1 |  tb_rmi_realm_activate.c line 107 | prop_success_realm_state_cons
1 |  tb_rmi_realm_activate.c line 98 | prop_result_cons
1 |  tb_rmi_realm_activate.c line 89 | prop_failure_realm_state_cons
2 |  tb_rmi_realm_destroy.c line 123 | prop_success_rd_state_cons
2 |  tb_rmi_realm_destroy.c line 115 | prop_success_rtt_state_cons
2 |  tb_rmi_realm_destroy.c line 106 | prop_result_cons
2 |  granule.h line 70 |  assertion false
2 |  granule.h line 66 |  assertion g->refcount == 0UL
2 |  granule.h line 63 |  assertion g->refcount <= GRANULE_SIZE / sizeof(uint64_t)
2 |  granule.h line 59 |  assertion g->refcount == 0UL
2 |  granule.h line 56 |  assertion granule_refcount_read_relaxed(g) <= 1UL
2 |  granule.h line 46 |  assertion g->refcount == 0UL
2 |  granule.h line 43 |  assertion granule_refcount_read_relaxed(g) == 0UL
2 |  tb_lock.c line 80 | The granule must be locked.
2 |  granule.h line 120 | assertion locked
2 |  tb_lock.c line 49 | The granule lock must be free.
2 |  status.h line 90 |  assertion (unsigned int)(-1 * (long)ptr) < RMI_ERROR_COUNT
2 |  vmid.c line 63 |  assertion vmid < vmid_count
2 |  realm.c line 337 | unwinding assertion loop
3 |  granule.h line 120 | assertion locked
3 |  granule.c line 47 |  assertion idx < RMM_MAX_GRANULES
3 |  tb_lock.c line 49 | The granule lock must be free.
3 |  s2tt.c line 358 |  assertion map_addr < (1UL << ipa_bits)
3 |  s2tt.c line 357 |  assertion level >= start_level
3 |  s2tt.c line 356 |  assertion start_level >= MIN_STARTING_LEVEL

## References

  * [1] Omar M. Alhawi et al.  “Verification and refutation of C programs based on k-induction and invariant inference”  In _Int. J. Softw. Tools Technol. Transf._ 23.2, 2021, pp. 115–135
  * [2] Dirk Beyer  “Competition on Software Verification and Witness Validation: SV-COMP 2023”  In _TACAS. LNCS_ 13994 Springer, 2023, pp. 495–522  DOI: 10.1007/978-3-031-30820-8\\_29
  * [3] Dirk Beyer  “State of the Art in Software Verification and Witness Validation: SV-COMP 2024”  In _30th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS_ 14572, LNCS  Springer, 2024, pp. 299–329
  * [4] Armin Biere  “Bounded Model Checking”  In _Handbook of Satisfiability_ 185 IOS Press, 2009, pp. 457–481  DOI: 10.3233/978-1-58603-929-5-457
  * [5] Edmund M. Clarke, Armin Biere, Richard Raimi and Yunshan Zhu  “Bounded Model Checking Using Satisfiability Solving”  In _Formal Methods Syst. Des._ 19.1, 2001, pp. 7–34  DOI: 10.1023/A:1011276507260
  * [6] Lucas C. Cordeiro, Bernd Fischer and João Marques-Silva  “SMT-Based Bounded Model Checking for Embedded ANSI-C Software”  In _IEEE Trans. Software Eng._ 38.4, 2012, pp. 957–974
  * [7] Anthony C.. Fox et al.  “A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations”  In _Proc. ACM Program. Lang._ 7.OOPSLA1, 2023, pp. 376–405  DOI: 10.1145/3586040
  * [8] Mikhail Y.. Gadelha, Hussama Ibrahim Ismail and Lucas C. Cordeiro  “Handling loops in bounded model checking of C programs via k-induction”  In _Int. J. Softw. Tools Technol. Transf._ 19.1, 2017, pp. 97–114  DOI: 10.1007/S10009-015-0407-9
  * [9] Mikhail Y.. Gadelha et al.  “ESBMC 5.0: an industrial-strength C model checker”  In _ASE_ ACM, 2018, pp. 888–891
  * [10] Mikhail Y.. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro and Denis A. Nicole  “ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution)”  In _TACAS. LNCS_ 11429 Springer, 2019, pp. 209–213  DOI: 10.1007/978-3-030-17502-3\\_15
  * [11] Amazon Inc.  “AWS CBMC Viewer” Last viewed June 2022, https://github.com/model-checking/cbmc-viewer, 2022
  * [12] Daniel Kroening and Ofer Strichman  “Decision Procedures - An Algorithmic Point of View, Second Edition”, Texts in Theoretical Computer Science. An EATCS Series  Springer, 2016  DOI: 10.1007/978-3-662-50497-0
  * [13] Daniel Kroening and Michael Tautschnig  “CBMC - C Bounded Model Checker - (Competition Contribution)”  In _TACAS, LNCS_ 8413 Springer, 2014, pp. 389–391  DOI: 10.1007/978-3-642-54862-8\\_26
  * [14] Xupeng Li et al.  “Design and Verification of the Arm Confidential Compute Architecture”  In _16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022_ USENIX Association, 2022, pp. 465–484  URL: https://www.usenix.org/conference/osdi22/presentation/li
  * [15] Arm Ltd.  “Arm Confidential Compute Architecture”, https://www.arm.com/architecture/security-features/armconfidential-compute-architecture, 2021
  * [16] Arm Ltd.  “Realm Management Monitor beta0 Specification” Accessed 25th October 2022, final version to be published 2022, https://developer.arm.com/documentation/den0137/a/, 2022
  * [17] Arm Ltd.  “TF-RMM Homepage” Last accessed 14 Jan 2024, https://www.trustedfirmware.org/projects/tf-rmm/
  * [18] Rafael Sá Menezes et al.  “ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)”  In _TACAS, LNCS_ 14572 Springer, 2024, pp. 376–380  DOI: 10.1007/978-3-031-57256-2\\_24
  * [19] Aina Niemetz, Mathias Preiner and Armin Biere  “Boolector 2.0”  In _J. Satisf. Boolean Model. Comput._ 9.1, 2014, pp. 53–58  DOI: 10.3233/SAT190101
  * [20] Jason Silverstein  “Hundreds of millions of Facebook user records were exposed on Amazon cloud server”  In _CBS News_ 4, 2019
  * [21] Janislley Oliveira Sousa et al.  “Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking”  In _CoRR_ abs/2311.05281, 2023  DOI: 10.48550/ARXIV.2311.05281
  * [22] S. Subashini and V. Kavitha  “A survey on security issues in service delivery models of cloud computing”  In _J. Netw. Comput. Appl._ 34.1, 2011, pp. 1–11  DOI: 10.1016/J.JNCA.2010.07.006


#  Algorithmic Pluralism
A Structural Approach Towards Equal Opportunity

Shomik Jain1, Vinith Suriyakumar2, Ashia Wilson1,2 MIT Institute for Data,
Systems, and Society, MIT1 Department of Electrical Engineering and Computer
Science, MIT2MIT

###### Abstract.

While the idea of equal opportunity enjoys a broad consensus, many disagree
about what it means for opportunities to be equal. The algorithmic fairness
community often relies on formal approaches to quantitatively determine if
opportunities are allocated equally. A more structural approach put forth by
Joseph Fishkin focuses on the wider network of decisions that determine which
opportunities are allocated to whom. In this so-called opportunity structure,
decision points represent bottlenecks that are often chained together so that
the output of one decision is an input to the next. By evaluating the severity
and legitimacy of these bottlenecks, Fishkin offers a qualitative framework to
assess whether equal opportunity is infringed upon in a structural way. We
adopt this structural viewpoint and use it to reframe many interdisciplinary
discussions about equal opportunity in systems of algorithmic decision-making.
Drawing on examples from education, healthcare, and criminal justice, we
recommend prioritizing regulatory and design-based interventions that
alleviate severe bottlenecks in order to help expand access to opportunities
in a pluralistic way.

algorithmic fairness, bottlenecks, equal opportunity, discrimination,
structural injustice

††copyright: none††copyright: none

##  1\. Introduction

Many works propose centering equal opportunity in systems of decision-making.
This is primarily because of the profound impact that opportunities have on
our skills, talents and future endeavors. Indeed, “we do not come into the
world with fixed preferences, ambitions, or capacities, but develop all these
through processes of interaction with the world and with the opportunities we
see before us” (Fishkin, 2014). In this way, the principle of equal
opportunity offers us a greater ability to shape our lives. Additionally, when
opportunities are more equal and plentiful, more people have the freedom to
choose among disparate life paths, as opposed to having these paths be
dictated by societal constraints. This notion of freedom makes equal
opportunity foundational to many democratic societies. Finally, it is worth
pointing out that the idea of equal opportunity enjoys a broad consensus. It
is a value that is singled out in several founding documents and is regularly
invoked by advocates of radically different political and social agendas
(Fishkin and Forbath, 2014).

Despite its wide appeal, many disagree deeply about the meaning of equal
opportunity. This debate unsurprisingly extends to the algorithmic fairness
community, especially given the ways in which our data-driven economy can
create circumstances that severely limit opportunities for swaths of the
population (Bommasani et al., 2022; Creel and Hellman, 2022). Many prior works
focus on what it means for a single opportunity to be “equal.” Formal views of
equal opportunity contend that specific decision points should only consider
features relevant to one’s future success in the opportunity being decided
(Rawls, 2004). This perspective has inspired several algorithmic fairness
metrics such as demographic parity (Calders et al., 2009; Zliobaite, 2015) and
equalized odds (Hardt et al., 2016). However, a growing number of scholars
have criticized the narrow scope of these quantitative interventions,
advocating instead for more structural views of equal opportunity that better
consider one’s life chances and pathways overall (Green, 2022; Arif Khan et
al., 2022; Kasirzadeh, 2022; Hoffmann, 2019; Selbst et al., 2019).

In this work, we adopt Joseph Fishkin’s structural approach towards equal
opportunity (Fishkin, 2014) and extend it to algorithmic decision-making.
Fishkin emphasizes the need for more pluralistic systems of decision-making in
order to preserve what makes equal opportunity so valued in the first place.
His viewpoint focuses on the concept of a bottleneck, which is a decision
point in the broad structure of how opportunities in our society are created,
distributed, and controlled. In these real-world networks of decisions,
bottlenecks often chain together so that the output of one decision point is
an input to the next. Each bottleneck involves some level of severity, or
degree to which it constrains opportunities, that juxtaposes with its
legitimacy, or justification in relation to how it allocates opportunities.
Fishkin highlights that systems of decision-making with severe bottlenecks
greatly compromise the principles of equal opportunity, regardless of their
legitimacy. He therefore argues that alleviating severity should be an urgent
priority. We extend this idea of opportunity pluralism (Fishkin, 2014) to
systems of algorithmic decision-making – what we define as algorithmic
pluralism. Specifically, we make the following contributions:

  * •

We review fundamental problems with equal opportunity introduced by a variety
of scholars that complicate its formulation in systems of decision-making
(Section 2).

  * •

We present Fishkin’s theory of bottlenecks and use the framework to center
several structural concerns about equal opportunity raised by a variety of
scholars who focus on algorithms and issues of justice (Section 3).

  * •

We show why greater opportunity requires alleviating severity and discuss
implications for regulation and design (Section 4).

  * •

We validate this framework through current debates about equal opportunity in
education, healthcare, and criminal justice (Section 5).

  * •

We end our discussion by situating bottleneck theory within the context of
related work (Section 6).

##  2\. Equal Opportunity and Its Problems

Formal views of equal opportunity propose that at any particular decision
point, a person should be evaluated only on features relevant to one’s future
success in the opportunity at hand (Rawls, 2004). While this sort of normative
reasoning seems compelling, several issues complicate the possibility and
desire to achieve this ideal in any system of decision-making, algorithmic or
not. Like Fishkin, we review Bernard Williams’ provocative thought experiment
of an imaginary society consisting of a dominating warrior class to first,
illustrate why it is surprisingly hard to specify the idea of equal
opportunity; and second, argue that even if practically achievable, formal
approaches offer an unsatisfactorily narrow view of the opportunity structure
(Williams et al., 1962; Fishkin, 2014).

###  2.1. Equal Opportunity Cannot Be Achieved

Consider a hypothetical society with two castes: warriors and non-warriors.
Warriors defend the society and are rewarded with all the valued goods that
society has. Since there are a fixed number of positions in the army, an
algorithm chooses who becomes a warrior at the age of sixteen based on various
characteristics such as athletic ability and intelligence tests. In principle,
the algorithm manifests the formal notion of equal opportunity by choosing
warriors based on features relevant to their success on the battlefield.
However, it turns out that the children of warrior parents have a significant
advantage. They are chosen more often because they are healthier, smarter,
stronger, and more confident – all traits that are reflected in the historical
data for successful warriors.

####  2.1.1. The problem of developmental opportunities

The children of warrior parents have advantageous experiences and resources
prior to the algorithm’s evaluation, such as family wealth and access to
better education. These developmental opportunities make it impossible for
warrior and non-warrior children to have a fair contest. While non-warrior
children are not explicitly excluded because of their caste, the data
collected on them reflects their lack of developmental opportunities. For this
reason, selecting warriors based on who will perform best will rationally omit
non-warrior children because of their disadvantages. As Fishkin explains, “if
success breeds success, and we reinforce achievement with new and richer
developmental opportunities, then the project of equalizing opportunities
comes squarely into conflict with rewarding performance. In that case, the
very earliest developmental opportunities, which precede any meaningful
performances worth rewarding, begin to take on an outsized significance”
(Fishkin, 2014).

####  2.1.2. The problem of isolating merit

Despite differences in developmental opportunities, views rooted in the
principle of formal equal opportunity still contend that decisions can be
based solely on merit, such as talent and effort (Rawls, 2004). But it is
practically impossible to isolate merit from circumstances of birth and
advantageous life experiences: “everything we are and everything we do is the
product of layer upon layer of interaction between person and environment –
between our selves, our efforts, and our opportunities – that in a sedimentary
way, over time, build each of us into the person we become” (Fishkin, 2014).
Moreover, real-world data and features will inherently combine aspects of
merit with developmental opportunities. Warrior children may score higher on
any test of athletic ability, for example, because of special coaching that
actually improves their scores more than it actually improves their
battlefield performance.

###  2.2. Formal Equal Opportunity Artificially Narrows the Solution Space

The warrior society thought experiment also illustrates how formal approaches
take an overly narrow view of the opportunity structure. As Dewey astutely
points out, “the way in which [a] problem is conceived decides what specific
suggestions are entertained and which are dismissed” (Dewey, 1938). Formal
fairness methods often reduce considerations to relative advantages or
disadvantages at a particular decision point. This type of single-axis
thinking comes at the expense of attention to what produces the systematic
benefits or privileges in the first place (Hoffmann, 2019). In doing so,
formal approaches do not account for the fact that having a plurality of
opportunities (and not just equal opportunities) is a prerequisite for the
accompanying virtues of “freedom” and ability to “shape our lives.”

####  2.2.1. The problem of a starting gate

Many formal notions of equal opportunity assert that if we could somehow
obtain a fair representation of data before some set point (a starting gate),
then algorithmic decision-making after that point would be fair as well
(Rawls, 2004). Some scholars have even attempted to solve this starting gate
issue through statistical methods (Hardt and Kim, 2022). While there are
epistemological and practical challenges with these approaches, the warrior
society reveals additional reasons for why they may be insufficient for
maintaining the virtues associated with equal opportunity. Suppose we could
equalize developmental opportunities by placing all children into warrior
skill academies from the moment of birth. While those not selected to become
warriors may no longer dispute the fairness of the algorithm, they still might
object at the severity of the decisions. Such a severe narrowing of their
entire life paths might be considered arbitrary, and compromises the notion
that equal opportunity is a principle which offers the freedom to shape our
lives. That is, it is not enough that opportunities be equal, there must also
be a plurality of opportunities.

####  2.2.2. The problem of zero-sum thinking

Focusing on specific decision points sometimes needlessly reduces
considerations of equal opportunity to zero-sum thinking. For example, if we
choose to give compensatory bonus points to non-warrior children, some warrior
children may object at no longer being selected. This distributive view forces
zero-sum trade-offs between mathematically incompatible notions of fairness,
magnifying the stakes of choosing between these definitions (Kleinberg et al.,
2016). As Green argues, restricting analysis to specific decision points also
cannot fully “account for the inequalities that often surround those decision
points [and] is therefore prone to reproducing existing patterns of injustice”
(Green, 2022). By expanding our view to the broader structure of
opportunities, we can better account for the important contexts in which
decisions are made and consider interventions that diminish or even eliminate
the zero-sum framing.

##  3\. Bottleneck Theory: A Structural View of Equal Opportunity

A growing number of interdisciplinary works have called for interventions
beyond formal approaches in order to better account for the broader structure
of opportunities (Green, 2022; Arif Khan et al., 2022; Kasirzadeh, 2022;
Selbst et al., 2019; Corbett-Davies and Goel, 2018). Fishkin’s bottleneck
theory (Fishkin, 2014) offers a novel framework for understanding the entire
network of decisions that determine which opportunities are allocated to whom.
A bottleneck is a decision point in the structure of how opportunities are
created, distributed, and controlled. As algorithms are increasingly used to
inform or make decisions about our lives, they represent bottlenecks for many
real-world opportunities. Bottlenecks are often chained together given that in
systems of decision-making, the outcomes of upstream decisions usually factor
into downstream decisions. Fishkin proposes the qualitative measures of
severity and legitimacy to assess the impact of each bottleneck on the broader
opportunity structure. We show how this framework maps to several predominant
concerns about algorithmic decision-making and its potential to infringe upon
equal opportunity in a structural way.

###  3.1. Severity

The severity of a bottleneck is the degree to which it constrains
opportunities. This is a combination of two factors: pervasiveness and
strictness (Fishkin, 2014). A bottleneck’s pervasiveness is the range of
affected people and opportunities. For example, the algorithm in the warrior
society has maximum pervasiveness because it controls everyone’s access to all
the valued goods in the society. Strictness refers to how directly a
bottleneck controls opportunities, or in other words, whether it is an
absolute bar, strong preference, or weak preference. The warrior society also
has maximum strictness because it is an absolute bar in determining who
becomes a warrior. While the warrior society represents an extreme case, many
severe bottlenecks can naturally arise in systems of data-driven decision-
making, as illustrated by the concerns expressed in the ideas of patterned
inequality and algorithmic monoculture.

####  3.1.1. The concern about patterned inequality is a concern about severe
bottlenecks

Patterned inequality refers to two observations made by Benjamin Eidelson: (1)
real-world inequalities in status, resources, and opportunities are often
patterned in terms of certain discernible, socially salient features; (2)
allocating future outcomes based on an individual’s likelihood of success will
predictably reproduce and aggravate patterns of this kind (Eidelson, 2021).
The problem of developmental opportunities makes it inevitable that some
patterns of inequality will exist. Once an observable trait, perhaps implicit
or arbitrary in itself, is correlated with less visible attributes relevant
for deciding opportunities, decision-makers will rationally tend to use that
trait as a proxy for allocating future outcomes (c.f. the problem of isolating
merit). For example, consider the strong correlation between credit score and
job performance, which led to its controversial use as a proxy for hiring
decisions (Ballance et al., 2020). Given algorithms are developed to identify
these patterns in a more explicit way, the concern is that allocating
opportunities using them “will tend to reproduce existing patterns in
inequality and cement the matrix of stereotypes and social meanings that both
cause and result from those patterns” (Eidelson, 2021). This stronger tendency
towards the comparatively privileged creates the possibility of stricter
bottlenecks, while the denial of even more opportunities to members of worse-
off groups represents more pervasive bottlenecks.

####  3.1.2. The concern about algorithmic monoculture is a concern about
severe bottlenecks

Algorithmic monoculture (Bommasani et al., 2022) occurs when multiple
decision-makers controlling access to a large quantity of valued goods rely on
similar datasets and/or models. This is increasingly common in high-stakes
screening decisions across many domains, including in employment, healthcare,
lending, and criminal justice (O’Neil, 2017). One reason why monoculture
occurs is that few decision-makers have the resources to build their own
automated systems. For example, over 30% of Fortune 100 companies use the same
resume-screening service for hiring (Raghavan et al., 2020). Recent works have
also demonstrated the performance gains of using pre-trained foundation models
instead of training new models from scratch and illustrated how this can lead
to homogenized outcomes (Bommasani et al., 2021, 2022). In other domains, the
data collection itself may be expensive or unfeasible, such as in healthcare
algorithms which disproportionately use data from only three states:
California, Massachusetts, and New York (Creel and Hellman, 2022).

The standardization of decision-making processes could create stricter
bottlenecks because certain features will be stronger preferences for the
opportunities at hand. In certain ranking problems like comparing job
candidates, sharing an algorithm across multiple decision-makers can also
reduce the overall quality of decisions, even if the algorithm is more
accurate for any one decision-maker in isolation (Kleinberg and Raghavan,
2021). Moreover, if similar algorithms are uniformly applied across wide
swathes of a single domain, outcomes could become homogenized resulting the
systematic exclusion of groups and individuals from opportunities of great
consequence (Creel and Hellman, 2022; Bommasani et al., 2022). This type of
outcome homogenization constitutes a more pervasive bottleneck for those that
repeatedly receive undesirable decisions because they may find themselves
locked out of many paths in the opportunity structure.

###  3.2. Legitimacy

Many other structural concerns about equal opportunity center on a model’s
legitimacy, or its justification in relation to how opportunities are
allocated (Fishkin, 2014). The justification for an algorithm is often argued
on two grounds: mathematical legitimacy and social legitimacy. Mathematical
legitimacy is simply the algorithm’s accuracy with respect to a particular
problem formulation. As we saw in the warrior society, however, a high
accuracy alone does not fully justify the use of an algorithm to control real-
world outcomes. The other necessary aspect to consider is an algorithm’s
social legitimacy: what is the rationale for using a particular problem
formulation (e.g. choosing a specific model, features, or training objective)
to constrain the specific opportunity at hand? As we will see in Section 5,
the COMPAS algorithm for predicting recidivism illustrates a canonical debate
about social legitimacy from the perspective of two formal fairness
approaches: calibration and error rate parity. While many scholars have raised
concerns about legitimacy (Green and Viljoen, 2020; Hoffmann, 2019;
Kasirzadeh, 2022), we highlight two in particular that direct their legitimacy
critique at the way opportunities are structured.

####  3.2.1. The concern about compounding injustice is a concern about
illegitimate bottlenecks.

Compounding injustice refers to Deborah Hellman’s critique of decisions that
take a prior wrong that a person has suffered, or its effects, as a reason for
allocating future opportunities in a way that makes them still worse off
(Hellman, 2018). In many cases, adverse predictions by algorithms may involve
the use of features that relate to prior victimization. For example, a
prominent healthcare algorithm selecting patients for high-risk care programs
used prior health costs as a proxy for future health needs (Obermeyer et al.,
2019). This ignored the well-documented injustices of the U.S. healthcare
system that cause less money to be spent on black patients who have the same
level of need as equally sick white patients. By denying future care on the
basis of prior health costs, the algorithm “compounded the initial injustice”
of unequal access to care. From the perspective of bottleneck theory,
Hellman’s formulation of compounding injustice and Eidelson’s patterned
inequality both surface similar concerns about the structure of opportunities;
however, Hellman’s argument raises the illegitimacy of the initial condition
as central to moral considerations, whereas Eidelson centers the severity of
unequal patterns of opportunity as sufficient to warrant moral concern.

####  3.2.2. The concern about relational harms is a concern about
illegitimate bottlenecks.

Relational harms refer to when algorithms fail to account for the power
relations, social dynamics, and structural contexts that surround systems of
decision-making in the real-world (Green and Viljoen, 2020; Green, 2022). In
particular, this involves scrutinizing what institutions, values, and norms
cause social and material disparities in opportunities (Anderson, 1999; Minow,
1990). Explicitly considering the potential for relational harms can help
justify algorithmic design choices and problem formulations. Whether or not
certain input features and output predictions are legitimate, for instance,
can depend on if they reduce dignitary and material disparities that reflect
social hierarchies (Green, 2022). For example, arguments against the
legitimacy of COMPAS highlight that predictions of recidivism fail to account
for the racial biases in policing that make re-arrest rates higher for
minority populations (Corbett-Davies et al., 2016). In addition, how much a
decision-maker values mitigating various relational harms can also inform the
choice of a training objective (Davis et al., 2021). Companies making hiring
decisions may have different values such as hiring from the local community,
creating more diverse teams, or addressing past discrimination. Training an
algorithm based on who has been hired in the past may undervalue the
contributions that underrepresented applicants bring to a company. Ultimately,
considerations of these broader contexts and how they affect an algorithm’s
social legitimacy will depend on one’s choice of worldview (Friedler et al.,
2021). This may differ from the perspective of various stakeholders, such as
those making decisions versus those seeking opportunities.

Severe(Pervasive & Strict) LegitimateArbitraryMild Figure 1. (Fig. 6 in
(Fishkin, 2014)) Fishkin’s framework for classifying bottlenecks. He proposes
mapping the structural impact of bottlenecks along the axes of severity and
legitimacy.

##  4\. Algorithmic Pluralism: Why Greater Opportunity Requires Alleviating
Severity

The previous section showed how structural concerns about equal opportunity
relate to ameliorating bottlenecks in the direction of less severity and more
legitimacy. But as many including Fishkin have argued, severity alone is
sufficient to warrant intervention even if a bottleneck is legitimate.
Moreover, while concerns about legitimacy matter immensely, severity is often
necessary to find consensus and compel intervention. This motivates Fishkin to
center severity as the prioritized axis for intervention in his proposal of
opportunity pluralism. By making bottlenecks less severe, it becomes “more
possible, both in ideal theory and the real world, to achieve the goals that
lead us to value equal opportunity in the first place” (Fishkin, 2014). In
this section, we recommend alleviating severity in systems of algorithmic
decision-making – what we define as algorithmic pluralism – and discuss
implications for regulation and design.

###  4.1. Severity Necessitates Intervention On Its Own

When a bottleneck becomes so severe that it significantly constrains a
person’s range of opportunities, it magnifies each of the problems with
achieving formal equal opportunity. Developmental opportunities will orient
themselves to the severe bottleneck; zero-sum debates will intensify over what
aspects of merit are legitimate; and the problem of determining a starting
gate will matter more because there are fewer paths to the opportunity of
consequence. For these reasons, Fishkin centers severity as the axis for
intervention in his proposal of opportunity pluralism (Fishkin, 2014), which
has four principles:

  1. (1)

There should be plurality of values and goals.

  2. (2)

As many as possible of the valued goods should be less positional and the
valued roles less competitive.

  3. (3)

As far as possible, there should be a plurality of paths leading to these
different valued goods and roles, without bottlenecks constraining people’s
ability to pursue those paths.

  4. (4)

There should be a plurality of sources of authority regarding the elements
described in the other principles.

In algorithmic systems, we similarly contend that severity warrants
intervention on its own, as many other works have argued (Eidelson, 2021;
Bommasani et al., 2022; Creel and Hellman, 2022). Eidelson’s concern about
patterned inequality is a concern about severe bottlenecks “not because it
necessarily treats any individual unfairly, but because it cuts against the
urgent project of scrambling existing patterns in societal inequalities.” The
sole existence of this patterned inequality “poses grave problems for a range
of widely endorsed values: it greatly undermines future equality of
opportunity; it makes it less likely that people will relate to one another as
equals; and, all issues of equality aside, it just means more overall misery
and less overall flourishing” (Eidelson, 2021). These concerns are independent
of any claims about the bottlenecks’ legitimacy or causal history by which the
patterns arose. Likewise, algorithmic monoculture constitutes a moral concern
because of its potential to create severe bottlenecks that homogenize outcomes
(Bommasani et al., 2022), regardless of how legitimate these outcomes are
considered to be. A society where some individuals and groups find themselves
locked out of significant parts of the opportunity structure compromises the
very virtue of freedom that we often associate with equal opportunity. As
Creel and Hellman add, “this moral problem will plague both arbitrary and non-
arbitrary algorithms” (Creel and Hellman, 2022).

###  4.2. Legitimacy Matters, But Severity Takes Precedent

The importance of ensuring legitimacy in algorithmic decisions cannot be
overstated. The primary aim of legitimacy is to align ML models with
fundamental human values such as equality and justice (Costanza-Chock, 2018;
Kasy and Abebe, 2021). Interventions to promote such values and make decisions
more “fair” have been the central focus of the algorithmic fairness community.
Moreover, recent critiques rightfully encourage the community to consider the
legitimacy of the broader opportunity structure in addition to formal fairness
approaches (Green, 2022; Kasirzadeh, 2022; Hoffmann, 2019). As Green points
out, however, addressing the legitimacy of decisions and reforms that might
alter them “can be a difficult and politically contested task” as it will
involve “grappling with contested notions of what types of inequalities are
unjust and what evidence constitutes sufficient proof of social hierarchy”
(Green, 2022). Society is built on a plurality of values existing inside the
boundaries of a human rights framework, and such plurality naturally extends
to debates over the legitimacy of algorithmic systems. Fishkin concludes that:
“all this leaves us with complex problems of prioritization. In a world of
myriad bottlenecks, we need to decide which ones to devote our efforts and
scare resources to ameliorating. The question of how important it is to loosen
any given bottleneck turns in significant part on how severe the bottleneck
is” (Fishkin, 2014). In other words, the severity of decisions on the
structure of opportunities – especially (but not only) when illegitimate –
should take precedent.

###  4.3. Implications for Regulators and Policymakers

Regulators and policymakers are often in the best position to intervene on the
basis of severity because they are explicitly tasked with considering the
broader structure of opportunities and its impacts. One can view all U.S.
anti-discrimination laws as intervening in practices that amount to a severe
bottleneck, and attempting to alter those practices so that the bottleneck is
somewhat less severe (Fishkin, 2014). For instance, many federal and state
anti-discrimination laws extend protections to groups that we would not
ordinarily expect the law to show solicitude, such as those with low-credit,
predispositions to disease, and even prior criminal convictions. While
businesses and other decision-makers may have many legitimate reasons for
denying opportunities on the basis of these characteristics, each category (as
an empirical matter in our society) severely constrains a person’s range of
opportunities making it sufficient and necessary to warrant concern. This idea
stems back to the very origins of anti-discrimination law and protected
classes such as race and gender. The longstanding legal theory of disparate
impact prohibits practices in employment, housing, and certain other areas
that have an “unjustified adverse impact on members of a protected class”
(Commission, 1979). As Fishkin explains, “there is nothing fundamental or
primordial about protecting a category like race. From the perspective of the
anti-bottleneck principle, the validity of anti-discrimination statutes
covering race is entirely contingent on the empirical reality that race is a
bottleneck in the opportunity structure” (Fishkin, 2014). Cases of disparate
impact further prioritize severity in how they unfold: the courts first
determine if there is an adverse impact (i.e. severity); and if so, they only
carve out exceptions if there is some justification or business necessity
(i.e. legitimacy). Fishkin’s view of anti-discrimination law as prioritizing
severity also aligns with Eidelson’s claim that “the objection from patterned
inequality is more plausible [than Hellman’s objection from compounding
injustice] as a matter of moral theory and better fits and justifies the
ambitious conception of anti-discrimination norms [that] animate both views”
(Eidelson, 2021).

###  4.4. Implications for Designers and Decision-Makers

Many technical interventions may also have practical applications for
alleviating severity in systems of algorithmic decision-making. For example,
broader analyses of how humans and algorithms should collaborate (Hedden,
2021; Donahue et al., 2022; Siddarth et al., 2021), better representations of
risk and uncertainty (Gebru et al., 2021; Mitchell et al., 2019), and learning
algorithms that account for long-term impacts (Perdomo et al., 2020; Taori and
Hashimoto, 2022; Mendler-Dünner et al., 2020) can all help account for the
overall structure of opportunities. However, the algorithmic fairness
community tends to view these interventions from the perspective of how they
can make decisions more legitimate, rather than from the perspective of how
they can disrupt the severity of decisions. Algorithmic recourse
(Venkatasubramanian and Alfano, 2020) represents one example of a severity-
oriented solution. Recourse provides a way to contest and overturn
predictions, which reduces strictness by making the algorithm less of an
absolute bar for the final outcome. Another intervention which could target
the pervasiveness of algorithmic decisions is model multiplicity (Black et
al., 2022), which refers to the existence of multiple models with varying
predictions but similar accuracy. This could counteract the risk of
algorithmic monoculture, but in practice these varying models may only affect
the outcomes of individuals near the decision boundary (Bommasani et al.,
2022). To provide a path for those who may still be locked out by all models,
Creel and Hellman propose intentionally introducing randomness into the
decision-making process (Creel and Hellman, 2022). In addition to these
methods, we also encourage designers and decision-makers to develop more
technical solutions that center severity as the axis for intervention.

##  5\. Case Studies

We discuss severe bottlenecks existing within the institutions of education,
healthcare, and criminal justice. We also show how severity amplifies debates
about legitimacy and discuss possible interventions for its mitigation.

###  5.1. Education

The college admissions process constitutes one of the more severe bottlenecks
in society today (Fishkin, 2014), and reinforces many patterns of inequality
across race and socioeconomic status. With the increasing number of
applications in recent years, acceptance rates dropped to new lows in 2022,
with Harvard only admitting 3.2% of applicants (Walsh, 2023). Nearly 20% of
these admissions comprise of those with legacy status, which overwhelmingly
favor white and wealthier students (Jeremy Ashkenas and Pearce, 2017).
Meanwhile, black and Hispanic students make up just 19% of enrolled students
despite representing 37% of the college-aged population, a gap that has
remained unchanged since 1980 (Jeremy Ashkenas and Pearce, 2017). College also
remains a pervasive and strict bottleneck for many career paths, with over 75%
of new jobs requiring a bachelor’s degree (Trend, 2022). Moreover, college
entrance itself depends on many upstream bottlenecks, such as the quality of
high school, standardized testing, and parental wealth. All these bottlenecks
severely constrain the paths of many prospective students, making a fallacy of
the notion that this process satisfies anything close to equality of
opportunity.

The goal of affirmative action policies, which allow the consideration of race
in admissions decisions, is to offer one way to loosen the bottleneck for
minority students. However, the current debate almost entirely focuses on how
it affects the legitimacy of the college admissions process. In oral arguments
from cases pending before the Supreme Court, Justice Sotomayor emphasized the
problems of isolating merit and developmental opportunities: “Sometimes race
does correlate to some experiences and not others. If you’re black, you’re
more likely to be in an underresourced school. You’re more likely to be taught
by teachers who are not as qualified as others. You’re more likely to be
viewed [as] having less academic potential…how do you want an admissions
officer to say, I’m not going to look at the race of the child to see if they
had all of those socioeconomic barriers present?” (of the United States,
2022b). Justice Kagan added how colleges justify the use of race for more
downstream legitimacy: “a lot of the argument here is about a [university’s]
compelling interest in collecting a diverse class, including along racial
dimensions and maybe especially along racial dimensions given the kinds of
challenges that our society faces” (of the United States, 2022a).

These debates over how to make the college admissions process more legitimate
overshadow the fact that the vast majority of students face difficult or
almost no paths to enrollment at elite institutions. Such severe constraints
pose grave challenges for the urgent priority of breaking existing patterns of
racial and socioeconomic inequalities (Eidelson, 2021). For these reasons,
some proposals call for more randomness in the admissions process, such as a
lottery among students that meet some academic criteria that could depend on
their high school (Walsh, 2023; Conley, 2018; Baker and Bastedo, 2022). Given
that there are many more qualified applicants than spots at elite
institutions, “an element of chance is already built into the system. The
difference is that a lottery [would make] that element transparent to all,
while eliminating many of the subjective biases that can creep into the
admissions process” (Walsh, 2023). Another proposed reform aimed at decreasing
severity of the admissions process involves increasing the range of paths to
entry-level jobs that do not require a bachelor’s degree. Many European
countries, for instance, have a well-developed system of apprenticeships and
training programs to prepare people for a substantial range of career paths
(Fishkin, 2014). These structural reforms would lessen the stakes of zero-sum
debates about legitimate aspects of merit, such as those in the ongoing
affirmative action cases: “In a zero-sum game like college admissions, if race
is going to be counted, that means some people are going to get in and some
people are going to be excluded based on race” (of the United States, 2022b).
More interventions that target the severity of the college admissions process
will not just benefit those that are currently disadvantaged; a more
pluralistic system of college education in relation to prior and future
opportunities would help all prospective students.

###  5.2. Healthcare

The management of chronic kidney disease (CKD) is a global health problem
associated with high levels of morbidity and mortality. More than 37 million
people in the US are estimated to have CKD, but only 10% of these individuals
are aware they have it (ckd, 2022). Many of the individuals who are
underdiagnosed and undertreated are racial minorities and the
socioeconomically disadvantaged, who already face many other inequalities in
the U.S. healthcare system (Briggs and Wesson, 2021). For example, black
Americans are almost four times more likely to suffer from kidney failure than
whites. Moreover, they are often not diagnosed until later stages of the
condition and spend months longer waiting for kidney transplants than white
patients. Another study found that 70% of individuals on Medicare are widely
underdiagnosed even when they have a lab test that indicated early CKD (Desai
et al., 2019).

To help manage the CKD population, researchers developed an algorithm called
the estimated glomerular filtration rate (eGFR) (Levey et al., 1999, 2009) to
gauge how fast a person’s kidneys filter blood, with lower filtration rates
suggesting worse kidney function. The use of eGFR is pervasive, with doctors
using it to make several decisions about patients’ overall care and access to
medical resources, including (but not limited to): (1) early detection of
kidney decline, (2) the level of antibiotic dosing, (3) risk assessments for
stroke and other conditions, and (4) placement on dialysis or transplant
lists. All of these algorithmically-supported decisions constitute severe
bottlenecks for care and treatment with varying levels of pervasiveness and
strictness. For (1) and (4), most patients are only considered for further
screening or placed on dialysis and transplant lists if their eGFR is below a
certain threshold (Delgado et al., 2022) resulting in maximum strictness. For
(2) and (3), eGFR is used for dosing a large number of commonly used
antibiotics such as Amoxicillin, Azithromycin, and Doxycycline (Crass et al.,
2019) and impacts risk assessment across a large number of comorbidities
(Delgado et al., 2022), resulting in its high pervasiveness across medical
decisions.

The severity of these bottlenecks in CKD management amplifies debates about
the eGFR algorithm and its legitimacy. Several equations for eGFR have noted
that using race improves overall accuracy and removes a systemic bias towards
underestimation in black patients. Specifically, algorithms using race result
in higher eGFR values (which suggest better kidney function) for anyone
identified as black. Some researchers claim that the systematically higher
eGFR scores from incorporating race leads to disadvantages for black patients,
such as late referral for kidney transplants (Ahmed et al., 2021). Meanwhile,
others note that underestimation without incorporating race could lead to
unintended consequences such as early dialysis initiation, inadequate dosing
of drugs, and limited access to treatments (Levey et al., 2020). Ultimately,
the National Kidney Foundation and the American Society of Nephrology decided
on a new algorithm without a race correction, even though it had lower overall
accuracy. They reached this decision with considerable input from hundreds of
stakeholders “to achieve consensus for an unbiased and most reasonably
accurate estimation of GFR so that laboratories, clinicians, patients and
public health officials can make informed decisions to ensure equity and
personalized care for patients with kidney diseases” (Delgado et al., 2022).

While these steps to improve the legitimacy of eGFR are imperative, further
steps could have been taken to reduce the severity of harms in CKD management,
especially for black patients. Instead of recommending one less accurate but
“race-free” algorithm, several different algorithms could have been
recommended for different decision points in the care process with mechanisms
for transparency regarding their potential biases and what impact this could
have on various patients. For example, the original equation with race
correction prevented underdosing and qualified more black patients as organ
donors, while the new equation results in much earlier transplant referrals
for black patients than before (Delgado et al., 2022). In addition to multiple
algorithms, having formal processes for patient recourse would also reduce the
severity of CKD management decisions. Power differentials between the patient
and the doctor make it imperative to create an equitable process for
contesting medical decisions (Goodyear-Smith and Buetow, 2001). While these
goals would require systemic changes in CKD management, prioritizing ways to
reduce the severity of harms would go a long way in addressing the structural
injustices of the healthcare system that even the most legitimate algorithms
cannot solve alone.

###  5.3. Criminal Justice

The cycle of mass incarceration in the U.S. criminal justice system
constitutes a severe bottlenecks for many defendants and their families. When
compared to other nations, defendants in the U.S. are more likely to end up in
prison, serve longer sentences, and commit future crimes. In particular,
almost 80% of those released from state prisons are re-arrested within five
years (Mauer, 2018). This pervasive cycle has led to the current state of mass
incarceration, with over 1 million people locked up in prison and over 500,000
in jail. Moreover, the overwhelming majority of those in jail are not
convicted and simply awaiting trial (Sawyer and Wagner, 2023). This severe
state of pretrial detention is directly influenced by risk assessment
algorithms, which increasingly inform bail and sentencing decisions. In fact,
over 60% of the U.S. population lives in a jurisdiction using these algorithms
(Project, [n. d.]).

The severe consequences of ending up in the criminal justice system make it
imperative to ensure the legitimacy of risk assessment algorithms. The
canonical debate around the COMPAS algorithm centers on the social legitimacy
of different formal fairness approaches (Corbett-Davies et al., 2016). On one
side, COMPAS argued for their tool’s legitimacy on the basis of calibration:
the algorithm predicted a risk score between 1 and 10, and at each level,
black and white defendants were roughly equally likely to reoffend. On the
other side, ProPublica argued that this problem formulation ignored the social
context that black defendants have a higher overall recidivism rate than white
defendants, in part due to biases in the criminal justice system and over-
policing of minority neighborhoods (Angwin et al., 2016). This causes black
defendants who don’t reoffend to be predicted as riskier by the algorithm than
white defendants who don’t reoffend. The courts grappled with this dilemma
when considering COMPAS’s legality in Wisconsin v. Loomis: “[We] caution
circuit courts that because COMPAS risk assessment scores are based on group
data, they are able to identify groups of high-risk offenders–not a particular
high-risk individual. Accordingly, a circuit court is expected to consider
this caution as it weighs all the factors that are relevant to sentencing an
individual defendant” (of Wisconsin, 2016).

While the courts left it open to individual cases to determine the legitimacy
of COMPAS, they placed clear bounds on its severity: “Although we ultimately
conclude that a COMPAS risk assessment can be used at sentencing, we do so by
circumscribing its use…we set forth the corollary limitation that risk scores
may not be used as the determinative factor in deciding whether the offender
can be supervised safely and effectively in the community” (of Wisconsin,
2016). This severity-oriented view should further extend to other aspects of
pretrial detention. Many less severe options could be adopted for defendants
awaiting trial, such as community service, rehabilitation programs, house
arrest, and electronic-monitoring devices (Mauer, 2018). Moreover, high-risk
predictions could be used as an indicator that an individual needs additional
support and resources to mitigate the chances of recidivism (Mayson, 2019).
Reducing the severity of the pretrial detention process would lessen the
stakes of risk assessment algorithms and debates about its legitimacy.

##  6\. Related Work

A formal approach to fairness has been the primary philosophical lens of the
algorithmic fairness community. Central aspects of this approach consist of
formulating mathematical definitions of fairness and developing methods that
satisfy or check for violations of these definitions (Joseph et al., 2016;
Hashimoto et al., 2018). Many of these methods adopt the perspective of formal
equal opportunity to introduce fairness metrics (Hardt et al., 2016; Joseph et
al., 2016; Hashimoto et al., 2018), map these metrics to various principles
(Heidari et al., 2019; Arif Khan et al., 2022), and present theories of
justice for artificial intelligence (Gabriel, 2022).

Our work joins the many in the algorithmic fairness community that have
criticized the narrow scope of distributive fairness interventions and their
reliance on formal equal opportunity principles, which offer an incomplete
normative palette for thinking about discrimination. As pointed out by Green
(2022) and Kasirzadeh (2022), formal approaches often suffer from the same
methodological limitations as formal equal opportunity principles and are
subsequently susceptible to “ethics washing”. These limitations include zero-
sum thinking as well as the tendency to ignore the power relations, social
dynamics, and the structural contexts that surround systems of algorithmic
decision-making in the real world (Kasirzadeh, 2022; Selbst et al., 2019;
Hoffmann, 2019). A fundamentally equitable path must adopt a wider frame,
considering all “unquestioned or intuitive assumptions in datasets, current
and historical injustices, and power asymmetries,” (Birhane, 2021) as well as
the larger opportunity structure itself. Although many mathematical
evaluations reflexively nod at these challenges, there remains a significant
gap between mathematical evaluations of fairness and an algorithm’s real world
impacts. Thus, algorithms satisfying fairness standards run the risk of
exacerbating oppression and legitimizing institutional injustices. These
notable deficiencies have inspired many other approaches and perspectives,
such as a structural injustice view from feminist political philosophy
(Kasirzadeh, 2022), relational approaches to substantive fairness (Green,
2022; Green and Viljoen, 2020), and consequentialist approaches to fairness
(Chohlas-Wood et al., 2021; Corbett-Davies and Goel, 2018).

The work of Ben Green (2022) is the most similar to our work, offering a
similar critique of formal equal opportunity through a subtly different
analysis and intervention. Green (2022) proposes an approach termed
“substantive algorithmic fairness,” which promotes a justice-oriented agenda
for developing and deploying algorithms. His approach is two-pronged,
consisting of (1) reducing the upstream social disparities that feed into the
decision-making process, and (2) reducing the downstream harms that result for
those judged unfavorably within decision-making processes. The first
intervention is meant to target the relational harms of “social and material
disparities grounded in social hierarchy,” and therefore address the
legitimacy concerns raised by Anderson (Anderson, 1999) and Minow (Minow,
1990). The second intervention is meant to target the structural aim of
“reducing the scope and stakes of decisions that act on social disparities,”
and thus address the severity concerns highlighted by Fishkin (Fishkin, 2014).

While Green’s approach is undoubtedly useful, our outlooks differ in two ways.
First, our framework makes clear that legitimacy and severity concerns don’t
just lie either upstream or downstream of a decision-point, but rather are
both structural concerns implicating the entire decision-making process. Take
the example of college education, where regardless of any upstream relational
differences or harms that have occurred between groups, colleges might still
adopt a consequentialist approach and consider the diversity that occurs
downstream of the decision to be a legitimate value to prioritize. Accounting
for severity, as well, requires understanding bottlenecks that exist both
upstream and downstream of the decision point. Second, while substantive
algorithmic fairness calls for both legitimacy- and severity-targeted
interventions equally, our framework of algorithmic pluralism argues that
severity-targeted interventions should often be prioritized (c.f. Section 4 –
legitimacy matters, but severity takes precedent).

##### Concluding Remarks

Fishkin’s idea of opportunity pluralism makes the case that societies ought to
move their structures of opportunity towards a more pluralistic model, where
there are many gatekeepers and paths towards opportunities (Fishkin, 2014). As
our economy increasingly relies on artificial intelligence, we emphasize the
importance of extending this idea to systems of data-driven decision-making
through algorithmic pluralism. Towards the end of his book, Fishkin emphasizes
that opportunity pluralism has vast implications for various institutions and
stakeholders. He aspires to encourage gatekeepers who wish to help build a
more pluralistic opportunity structure to reexamine and ameliorate the
bottlenecks that result from how they make decisions. We similarly implore the
data scientists responsible for designing models, gatekeepers who ultimately
make decisions, and policymakers regulating algorithmic systems to isolate
where they have the leverage to ameliorate bottlenecks, especially those that
are most severe.

## References

  * (1)
  * ckd (2022) 2022\.  Chronic Kidney Disease in the United States, 2021.  Centers for Disease Control and Prevention.  Accessed: 2023-5-10.
  * Ahmed et al. (2021) Salman Ahmed, Cameron T Nutt, Nwamaka D Eneanya, Peter P Reese, Karthik Sivashanker, Michelle Morse, Thomas Sequist, and Mallika L Mendu. 2021\.  Examining the potential impact of race multiplier utilization in estimated glomerular filtration rate calculation on African-American care outcomes.  _Journal of General Internal Medicine_ 36 (2021), 464–471.
  * Anderson (1999) Elizabeth S. Anderson. 1999\.  What Is the Point of Equality?  _Ethics_ 109, 2 (1999), 287–337.  https://doi.org/10.1086/233897
  * Angwin et al. (2016) Julia Angwin, Jeff Larson, Surya Mattu, and Lauren Kirchner. 2016.  Machine bias.  In _Ethics of data and analytics_. Auerbach Publications, 254–264.
  * Arif Khan et al. (2022) Falaah Arif Khan, Eleni Manis, and Julia Stoyanovich. 2022\.  Towards Substantive Conceptions of Algorithmic Fairness: Normative Guidance from Equal Opportunity Doctrines. In _Equity and Access in Algorithms, Mechanisms, and Optimization_ (Arlington, VA, USA) _(EAAMO ’22)_. Association for Computing Machinery, New York, NY, USA, Article 18, 10 pages.  https://doi.org/10.1145/3551624.3555303
  * Baker and Bastedo (2022) Dominique J Baker and Michael N Bastedo. 2022.  What If We Leave It Up to Chance? Admissions Lotteries and Equitable Access at Selective Colleges.  _Educational Researcher_ 51, 2 (2022), 134–145.
  * Ballance et al. (2020) Joshua Ballance, Robert Clifford, and Daniel Shoag. 2020\.  “No more credit score”: Employer credit check bans and signal substitution.  _Labour Economics_ 63 (2020), 101769.
  * Birhane (2021) Abeba Birhane. 2021\.  Algorithmic injustice: a relational ethics approach.  _Patterns_ 2, 2 (2021), 100205.  https://doi.org/10.1016/j.patter.2021.100205
  * Black et al. (2022) Emily Black, Manish Raghavan, and Solon Barocas. 2022\.  Model Multiplicity: Opportunities, Concerns, and Solutions. In _2022 ACM Conference on Fairness, Accountability, and Transparency_ (Seoul, Republic of Korea) _(FAccT ’22)_. Association for Computing Machinery, New York, NY, USA, 850–863.  https://doi.org/10.1145/3531146.3533149
  * Bommasani et al. (2022) Rishi Bommasani, Kathleen A. Creel, Ananya Kumar, Dan Jurafsky, and Percy S Liang. 2022\.  Picking on the Same Person: Does Algorithmic Monoculture lead to Outcome Homogenization?. In _Advances in Neural Information Processing Systems_ , S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh (Eds.), Vol. 35. Curran Associates, Inc., 3663–3678.  https://proceedings.neurips.cc/paper_files/paper/2022/file/17a234c91f746d9625a75cf8a8731ee2-Paper-Conference.pdf
  * Bommasani et al. (2021) Rishi Bommasani, Drew A Hudson, Ehsan Adeli, Russ Altman, Simran Arora, Sydney von Arx, Michael S Bernstein, Jeannette Bohg, Antoine Bosselut, Emma Brunskill, et al. 2021\.  On the opportunities and risks of foundation models.  _arXiv preprint arXiv:2108.07258_ (2021).
  * Briggs and Wesson (2021) Josephine P Briggs and Donald Wesson. 2021.  Introducing a Special Series: Addressing Racial and Ethnic Disparities in Kidney Disease.  _Journal of the American Society of Nephrology_ 32, 10 (2021), 2417–2418.
  * Calders et al. (2009) Toon Calders, Faisal Kamiran, and Mykola Pechenizkiy. 2009\.  Building classifiers with independency constraints. In _2009 IEEE international conference on data mining workshops_. IEEE, 13–18.
  * Chohlas-Wood et al. (2021) Alex Chohlas-Wood, Madison Coots, Henry Zhu, Emma Brunskill, and Sharad Goel. 2021.  Learning to be fair: A consequentialist approach to equitable decision-making.  _arXiv preprint arXiv:2109.08792_ (2021).
  * Commission (1979) US Equal Employment Opportunity Commission. 1979.  Questions and Answers to Clarify and Provide a Common Interpretation of the Uniform Guidelines on Employee Selection Procedures.
  * Conley (2018) Dalton Conley. 2018\.  Enough fretting over college admissions: It’s time for a lottery.  Washington Post.
  * Corbett-Davies and Goel (2018) Sam Corbett-Davies and Sharad Goel. 2018.  The measure and mismeasure of fairness: A critical review of fair machine learning.  _arXiv preprint arXiv:1808.00023_ (2018).
  * Corbett-Davies et al. (2016) Sam Corbett-Davies, Emma Pierson, Avi Feller, and Sharad Goel. 2016\.  A computer program used for bail and sentencing decisions was labeled biased against blacks. It’s actually not that clear.  _Washington Post_ 17 (2016).
  * Costanza-Chock (2018) Sasha Costanza-Chock. 2018\.  Design justice, AI, and escape from the matrix of domination.  _Journal of Design and Science_ 3, 5 (2018).
  * Crass et al. (2019) Ryan L Crass, Keith A Rodvold, Bruce A Mueller, and Manjunath P Pai. 2019.  Renal dosing of antibiotics: are we jumping the gun?  _Clinical Infectious Diseases_ 68, 9 (2019), 1596–1602.
  * Creel and Hellman (2022) Kathleen Creel and Deborah Hellman. 2022.  The Algorithmic Leviathan: Arbitrariness, Fairness, and Opportunity in Algorithmic Decision-Making Systems.  _Canadian Journal of Philosophy_ 52, 1 (2022), 26–43.  https://doi.org/10.1017/can.2022.3
  * Davis et al. (2021) Jenny L Davis, Apryl Williams, and Michael W Yang. 2021\.  Algorithmic reparation.  _Big Data & Society_ 8, 2 (2021), 20539517211044808\.
  * Delgado et al. (2022) Cynthia Delgado, Mukta Baweja, Deidra C Crews, Nwamaka D Eneanya, Crystal A Gadegbeku, Lesley A Inker, Mallika L Mendu, W Greg Miller, Marva M Moxey-Mims, Glenda V Roberts, et al. 2022\.  A unifying approach for GFR estimation: recommendations of the NKF-ASN task force on reassessing the inclusion of race in diagnosing kidney disease.  _American Journal of Kidney Diseases_ 79, 2 (2022), 268–288.
  * Desai et al. (2019) Nisa Desai, Claudia M Lora, James P Lash, and Ana C Ricardo. 2019.  CKD and ESRD in US Hispanics.  _Am. J. Kidney Dis._ 73, 1 (Jan. 2019), 102–111.
  * Dewey (1938) John Dewey. 1938\.  Logic: The Theory of Inquiry.  (1938).
  * Donahue et al. (2022) Kate Donahue, Alexandra Chouldechova, and Krishnaram Kenthapadi. 2022\.  Human-Algorithm Collaboration: Achieving Complementarity and Avoiding Unfairness. In _2022 ACM Conference on Fairness, Accountability, and Transparency_ (Seoul, Republic of Korea) _(FAccT ’22)_. Association for Computing Machinery, New York, NY, USA, 1639–1656.  https://doi.org/10.1145/3531146.3533221
  * Eidelson (2021) Benjamin Eidelson. 2021\.  Patterned Inequality, Compounding Injustice, and Algorithmic Prediction.  _American Journal of Law and Equality_ 1 (2021), 252–276.
  * Fishkin (2014) Joseph Fishkin. 2014\.  _Bottlenecks: A new theory of equal opportunity_.  Oxford University Press, USA.
  * Fishkin and Forbath (2014) Joseph Fishkin and William E Forbath. 2014.  The anti-oligarchy constitution.  _BUL Rev._ 94 (2014), 669.
  * Friedler et al. (2021) Sorelle A Friedler, Carlos Scheidegger, and Suresh Venkatasubramanian. 2021\.  The (im) possibility of fairness: Different value systems require different mechanisms for fair decision making.  _Commun. ACM_ 64, 4 (2021), 136–143.
  * Gabriel (2022) Iason Gabriel. 2022\.  Toward a theory of justice for artificial intelligence.  _Daedalus_ 151, 2 (2022), 218–231.
  * Gebru et al. (2021) Timnit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daumé Iii, and Kate Crawford. 2021\.  Datasheets for datasets.  _Commun. ACM_ 64, 12 (2021), 86–92.
  * Goodyear-Smith and Buetow (2001) Felicity Goodyear-Smith and Stephen Buetow. 2001.  Power issues in the doctor-patient relationship.  _Health care analysis_ 9 (2001), 449–462.
  * Green (2022) Ben Green. 2022\.  Escaping the Impossibility of Fairness: From Formal to Substantive Algorithmic Fairness.  _Philosophy and Technology_ 35 (12 2022).  Issue 4.
  * Green and Viljoen (2020) Ben Green and Salomé Viljoen. 2020.  Algorithmic Realism: Expanding the Boundaries of Algorithmic Thought. In _Proceedings of the 2020 Conference on Fairness, Accountability, and Transparency_ (Barcelona, Spain) _(FAT* ’20)_. Association for Computing Machinery, New York, NY, USA, 19–31.  https://doi.org/10.1145/3351095.3372840
  * Hardt and Kim (2022) Moritz Hardt and Michael P Kim. 2022.  Backward baselines: Is your model predicting the past?  _arXiv preprint arXiv:2206.11673_ (2022).
  * Hardt et al. (2016) Moritz Hardt, Eric Price, and Nati Srebro. 2016.  Equality of opportunity in supervised learning.  _Advances in neural information processing systems_ 29 (2016).
  * Hashimoto et al. (2018) Tatsunori Hashimoto, Megha Srivastava, Hongseok Namkoong, and Percy Liang. 2018.  Fairness without demographics in repeated loss minimization. In _International Conference on Machine Learning_. PMLR, 1929–1938.
  * Hedden (2021) Brian Hedden. 2021\.  On statistical criteria of algorithmic fairness.  _Philosophy and Public Affairs_ 49, 2 (2021).
  * Heidari et al. (2019) Hoda Heidari, Michele Loi, Krishna P Gummadi, and Andreas Krause. 2019.  A moral framework for understanding fair ml through economic models of equality of opportunity. In _Proceedings of the conference on fairness, accountability, and transparency_. 181–190.
  * Hellman (2018) Deborah Hellman. 2018\.  Indirect discrimination and the duty to avoid compounding injustice.  _Foundations of Indirect Discrimination Law, Hart Publishing Company_ (2018), 2017–53.
  * Hoffmann (2019) Anna Lauren Hoffmann. 2019\.  Where fairness fails: data, algorithms, and the limits of antidiscrimination discourse.  _Information, Communication & Society_ 22, 7 (2019), 900–915.
  * Jeremy Ashkenas and Pearce (2017) Haeyoun Park Jeremy Ashkenas and Adam Pearce. 2017.  Even With Affirmative Action, Blacks and Hispanics Are More Underrepresented at Top Colleges Than 35 Years Ago.  New York Times.
  * Joseph et al. (2016) Matthew Joseph, Michael Kearns, Jamie Morgenstern, Seth Neel, and Aaron Roth. 2016.  Rawlsian fairness for machine learning.  _arXiv preprint arXiv:1610.09559_ (2016).
  * Kasirzadeh (2022) Atoosa Kasirzadeh. 2022\.  Algorithmic Fairness and Structural Injustice: Insights from Feminist Political Philosophy. In _Proceedings of the 2022 AAAI/ACM Conference on AI, Ethics, and Society_. 349–356.
  * Kasy and Abebe (2021) Maximilian Kasy and Rediet Abebe. 2021.  Fairness, equality, and power in algorithmic decision-making. In _Proceedings of the 2021 ACM Conference on Fairness, Accountability, and Transparency_. 576–586.
  * Kleinberg et al. (2016) Jon Kleinberg, Sendhil Mullainathan, and Manish Raghavan. 2016\.  Inherent trade-offs in the fair determination of risk scores.  _arXiv preprint arXiv:1609.05807_ (2016).
  * Kleinberg and Raghavan (2021) Jon Kleinberg and Manish Raghavan. 2021.  Algorithmic monoculture and social welfare.  _Proceedings of the National Academy of Sciences_ 118, 22 (2021), e2018340118.  https://doi.org/10.1073/pnas.2018340118 arXiv:https://www.pnas.org/doi/pdf/10.1073/pnas.2018340118
  * Levey et al. (1999) Andrew S Levey, Juan P Bosch, Julia Breyer Lewis, Tom Greene, Nancy Rogers, David Roth, and Modification of Diet in Renal Disease Study Group*. 1999\.  A more accurate method to estimate glomerular filtration rate from serum creatinine: a new prediction equation.  _Annals of internal medicine_ 130, 6 (1999), 461–470.
  * Levey et al. (2009) Andrew S Levey, Lesley A Stevens, Christopher H Schmid, Yaping Zhang, Alejandro F Castro III, Harold I Feldman, John W Kusek, Paul Eggers, Frederick Van Lente, Tom Greene, et al. 2009\.  A new equation to estimate glomerular filtration rate.  _Annals of internal medicine_ 150, 9 (2009), 604–612.
  * Levey et al. (2020) Andrew S Levey, Silvia M Titan, Neil R Powe, Josef Coresh, and Lesley A Inker. 2020.  Kidney disease, race, and GFR estimation.  _Clinical Journal of the American Society of Nephrology_ 15, 8 (2020), 1203–1212.
  * Mauer (2018) Marc Mauer. 2018\.  Long-Term Sentences: Time to Reconsider the Scale of Punishment.  https://www.sentencingproject.org.
  * Mayson (2019) Sandra G Mayson. 2019\.  Bias in, bias out.  _The Yale Law Journal_ 128, 8 (2019), 2218–2300.
  * Mendler-Dünner et al. (2020) Celestine Mendler-Dünner, Juan Perdomo, Tijana Zrnic, and Moritz Hardt. 2020.  Stochastic optimization for performative prediction.  _Advances in Neural Information Processing Systems_ 33 (2020), 4929–4939.
  * Minow (1990) Martha Minow. 1990\.  _Making all the difference: Inclusion, exclusion, and American law_.  Cornell University Press.
  * Mitchell et al. (2019) Margaret Mitchell, Simone Wu, Andrew Zaldivar, Parker Barnes, Lucy Vasserman, Ben Hutchinson, Elena Spitzer, Inioluwa Deborah Raji, and Timnit Gebru. 2019.  Model cards for model reporting. In _Proceedings of the conference on fairness, accountability, and transparency_. 220–229.
  * Obermeyer et al. (2019) Ziad Obermeyer, Brian Powers, Christine Vogeli, and Sendhil Mullainathan. 2019.  Dissecting racial bias in an algorithm used to manage the health of populations.  _Science_ 366, 6464 (2019), 447–453.  https://doi.org/10.1126/science.aax2342 arXiv:https://www.science.org/doi/pdf/10.1126/science.aax2342
  * of the United States (2022a) Supreme Court of the United States. 2022a.  Students For Fair Admission, Inc., v. President and Fellows of Harvard College.
  * of the United States (2022b) Supreme Court of the United States. 2022b.  Students For Fair Admission, Inc., v. University of North Carolina, et al.
  * of Wisconsin (2016) Supreme Court of Wisconsin. 2016\.  State of Wisconsin v. Eric L. Loomis.
  * O’Neil (2017) Cathy O’Neil. 2017\.  _Weapons of math destruction: How big data increases inequality and threatens democracy_.  Crown.
  * Perdomo et al. (2020) Juan Perdomo, Tijana Zrnic, Celestine Mendler-Dünner, and Moritz Hardt. 2020.  Performative prediction. In _International Conference on Machine Learning_. PMLR, 7599–7609.
  * Project ([n. d.]) Movement Alliance Project. [n. d.].  Where are risk assessments being used?  https://pretrialrisk.com.
  * Raghavan et al. (2020) Manish Raghavan, Solon Barocas, Jon Kleinberg, and Karen Levy. 2020.  Mitigating Bias in Algorithmic Hiring: Evaluating Claims and Practices. In _Proceedings of the 2020 Conference on Fairness, Accountability, and Transparency_ (Barcelona, Spain) _(FAT* ’20)_. Association for Computing Machinery, New York, NY, USA, 469–481.  https://doi.org/10.1145/3351095.3372828
  * Rawls (2004) John Rawls. 2004\.  A theory of justice.  In _Ethics_. Routledge, 229–234.
  * Sawyer and Wagner (2023) Wendy Sawyer and Peter Wagner. 2023.  Mass Incarceration: The Whole Pie 2023.  https://www.prisonpolicy.org.
  * Selbst et al. (2019) Andrew D Selbst, Danah Boyd, Sorelle A Friedler, Suresh Venkatasubramanian, and Janet Vertesi. 2019\.  Fairness and abstraction in sociotechnical systems. In _Proceedings of the conference on fairness, accountability, and transparency_. 59–68.
  * Siddarth et al. (2021) Divya Siddarth, Daron Acemoglu, Danielle Allen, Kate Crawford, James Evans, Michael Jordan, and E Weyl. 2021.  How AI fails us.  _arXiv preprint arXiv:2201.04200_ (2021).
  * Taori and Hashimoto (2022) Rohan Taori and Tatsunori B Hashimoto. 2022.  Data Feedback Loops: Model-driven Amplification of Dataset Biases.  _arXiv preprint arXiv:2209.03942_ (2022).
  * Trend (2022) David Trend. 2022\.  75% of New Jobs Require a Degree While Only 40% of Potential Applicants Have One.  https://truthout.org.
  * Venkatasubramanian and Alfano (2020) Suresh Venkatasubramanian and Mark Alfano. 2020.  The philosophical basis of algorithmic recourse. In _Proceedings of the 2020 conference on fairness, accountability, and transparency_. 284–293.
  * Walsh (2023) Bryan Walsh. 2023\.  Why we should run elite college admissions like a lottery.  Vox.
  * Williams et al. (1962) Bernard Williams, Peter Laslett, and Walter G Runciman. 1962\.  _The idea of equality_.
  * Zliobaite (2015) Indre Zliobaite. 2015\.  On the relation between accuracy and fairness in binary classification.  _arXiv preprint arXiv:1505.05723_ (2015).