Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Improving the Security of United States Elections with Robust Optimization

Braden L. Crimmins, J. Alex Halderman, Bradley Sturt

TL;DR

The paper reframes LAT as a robust optimization problem to preempt misconfigurations in computerized voting machines, introducing RLAT with a swap-uncertainty set that guarantees detection of any bijective candidate-to-target swaps. It develops an exact cutting-plane algorithm with MILP reformulations to compute minimum-length test decks, and demonstrates practical scalability via Michigan’s 6928 ballot styles, where the robust decks require only a 1.2% average increase in ballots and complete statewide computation in under seven hours. The approach provides interpretable security guarantees, integrates with existing election workflows, and offers an open-source codebase for broader adoption and extension to other threat models. The results show RLAT as a low-cost, scalable defense that can enhance public trust in elections while maintaining administrative practicality.

Abstract

For more than a century, election officials across the United States have inspected voting machines before elections using a procedure called Logic and Accuracy Testing (LAT). This procedure consists of election officials casting a test deck of ballots into each voting machine and confirming the machine produces the expected vote total for each candidate. We bring a scientific perspective to LAT by introducing the first formal approach to designing test decks with rigorous security guarantees. Specifically, our approach employs robust optimization to find test decks that are guaranteed to detect any voting machine misconfiguration that would cause votes to be swapped across candidates. Out of all the test decks with this security guarantee, our robust optimization problem yields the test deck with the minimum number of ballots, thereby minimizing implementation costs for election officials. To facilitate deployment at scale, we develop a practically efficient exact algorithm for solving our robust optimization problems based on the cutting plane method. In partnership with the Michigan Bureau of Elections, we retrospectively applied our approach to all 6928 ballot styles from Michigan's November 2022 general election; this retrospective study reveals that the test decks with rigorous security guarantees obtained by our approach require, on average, only 1.2% more ballots than current practice. Our approach has since been piloted in real-world elections by the Michigan Bureau of Elections as a low-cost way to improve election security and increase public trust in democratic institutions.

Improving the Security of United States Elections with Robust Optimization

TL;DR

The paper reframes LAT as a robust optimization problem to preempt misconfigurations in computerized voting machines, introducing RLAT with a swap-uncertainty set that guarantees detection of any bijective candidate-to-target swaps. It develops an exact cutting-plane algorithm with MILP reformulations to compute minimum-length test decks, and demonstrates practical scalability via Michigan’s 6928 ballot styles, where the robust decks require only a 1.2% average increase in ballots and complete statewide computation in under seven hours. The approach provides interpretable security guarantees, integrates with existing election workflows, and offers an open-source codebase for broader adoption and extension to other threat models. The results show RLAT as a low-cost, scalable defense that can enhance public trust in elections while maintaining administrative practicality.

Abstract

For more than a century, election officials across the United States have inspected voting machines before elections using a procedure called Logic and Accuracy Testing (LAT). This procedure consists of election officials casting a test deck of ballots into each voting machine and confirming the machine produces the expected vote total for each candidate. We bring a scientific perspective to LAT by introducing the first formal approach to designing test decks with rigorous security guarantees. Specifically, our approach employs robust optimization to find test decks that are guaranteed to detect any voting machine misconfiguration that would cause votes to be swapped across candidates. Out of all the test decks with this security guarantee, our robust optimization problem yields the test deck with the minimum number of ballots, thereby minimizing implementation costs for election officials. To facilitate deployment at scale, we develop a practically efficient exact algorithm for solving our robust optimization problems based on the cutting plane method. In partnership with the Michigan Bureau of Elections, we retrospectively applied our approach to all 6928 ballot styles from Michigan's November 2022 general election; this retrospective study reveals that the test decks with rigorous security guarantees obtained by our approach require, on average, only 1.2% more ballots than current practice. Our approach has since been piloted in real-world elections by the Michigan Bureau of Elections as a low-cost way to improve election security and increase public trust in democratic institutions.
Paper Structure (55 sections, 17 theorems, 81 equations, 10 figures)

This paper contains 55 sections, 17 theorems, 81 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Logic and Accuracy Testing
  4. Contributions
  5. Vulnerabilities of Existing Heuristics for Designing Test Decks
  6. Swaps of Individual Candidates.
  7. Swaps of Entire Contests.
  8. Deliberately Flawed Test Decks.
  9. Robust Logic and Accuracy Testing
  10. Preliminaries
  11. Formulation of RLAT
  12. Election Administrators.
  13. Policy Makers and Voters.
  14. Computer Security Community.
  15. RLAT with the Swap Uncertainty Set
  16. ...and 40 more sections

Key Result

Theorem 1

Let $\beta_1, \ldots, \beta_B \in \mathscr{B}$ and $\sigma \in \Sigma$. Then $T^\sigma(\beta_1,\ldots,\beta_B) \neq T^*(\beta_1,\ldots,\beta_B)$ if and only if at least one of the following two conditions hold:

Figures (10)

  • Figure 1: Visualization of Logic and Accuracy Testing (LAT). The procedure is conducted chronologically from left to right on voting machines before each election. The modification to LAT proposed in this paper is denoted by the white box with the text "Test deck is chosen as the solution to an optimization problem".
  • Figure 2: A test deck composed of six ballots for a simple election with two contests. The first contest is a presidential contest with three candidates; the second contest is a senatorial contest with two candidates. In each contest, a voter is allowed to vote for at most one candidate.
  • Figure 3: Each example shows a misconfiguration of the mapping between voting targets and candidates (left), the misconfigured voting machine's interpretation of the test deck from Figure \ref{['fig:testdeck']} (center), and the vote tally that is output by the misconfigured voting machine (right). The color red indicates the aspects of the interpretation of the test deck and the machine output that are impacted by the misconfiguration of the voting machine. Diagonal lines through a contest indicate that the filled-out ballot is interpreted as containing an overvote in that contest, in which case the voting machine interprets the filled-out ballot as if no candidates were selected in that contest. (a) The misconfiguration is detected because the output of the voting machine includes incorrect vote totals for Washington, Jefferson, and Lincoln. (b) The misconfiguration is detected because the output of the voting machine includes incorrect vote totals for Jefferson, Lincoln, and Clay. (c) The misconfiguration is not detected because the output of the voting machine includes correct vote totals for all candidates (see Figure \ref{['fig:testdeck']}).
  • Figure 4: Histogram of the total number of contests (orange) and total number of candidates (blue) that appeared across the 6928 ballot styles in Michigan's November 2022 general election.
  • Figure 5: Visualization of our exact algorithm from §\ref{['appx:cutting']} for solving the optimization problem \ref{['prob:robust']}.
  • ...and 5 more figures

Theorems & Definitions (42)

  • Remark 1
  • Remark 2
  • Theorem 1
  • Corollary 1
  • Remark 3
  • Remark 4
  • Lemma 1
  • Lemma 2
  • Proposition 1
  • Definition 1: Equivalence of contests
  • ...and 32 more