#40 Secure Voting - Joe Kiniry
Type Theory Forall
Deep Dive
What is the historical significance of the Australian secret ballot in voting systems?
The Australian secret ballot introduced notions of privacy and decoupled the voter from their vote, which was a significant shift from earlier methods like public hand-raising. This change brought new opportunities and challenges, particularly in ensuring the security and integrity of elections.
Why is plurality voting considered problematic in the United States?
Plurality voting, where the candidate with 50% plus one vote wins, leads to troublesome outcomes in a split electorate. It often results in two dominant parties that deeply oppose each other, creating polarization and reducing the representation of minority views.
What are the challenges with tabulators in voting systems?
Tabulators often have flaws due to complex legal specifications that are not written by experts. For example, in Ireland, the legal text for vote counting was so convoluted that it required a PhD thesis to translate it into a mathematical specification, revealing numerous issues in the process.
What is the role of computers in electronic voting systems?
Computers are used in various ways in voting, including tabulation, auditing, and facilitating election operations. However, their use in voter-facing systems, such as voting booths, has raised concerns about transparency and security, especially when proprietary systems are involved.
Why do experts advocate for paper ballots in electronic voting systems?
Paper ballots are essential because they provide human-readable, verifiable records that voters can understand and trust. They ensure transparency and prevent leakage of sensitive information, which is critical for maintaining the integrity of elections.
What is the StarVote system, and why is it considered a model for secure voting?
StarVote is an end-to-end verifiable supervised voting system that uses plain paper ballots and cryptographic methods to ensure trustworthiness. It allows for software independence, meaning errors can be detected cryptographically, and facilitates statistically valid risk-limiting audits. Despite its potential, its development was halted due to resistance from existing vendors.
What are the main challenges in implementing secure internet voting systems?
Internet voting systems face significant challenges, including a larger attack surface and potential side channels like coercion from abusive spouses or employers. These systems are only recommended for low-value elections, such as primaries, and require advancements in high-assurance hardware and cryptographic protocols to mitigate risks.
How do formal methods contribute to the design of secure voting systems?
Formal methods help ensure that voting systems are built with rigorous specifications and correctness proofs. They address inconsistencies in legal requirements, provide traceability from requirements to implementation, and enable formal verification of software and hardware to meet high-assurance standards.
What was the outcome of analyzing a black box tabulator in Ireland?
The analysis revealed that the proprietary black box tabulator used in Ireland was incorrect in its tabulation. Despite being a closed system, counterexample generation based on a formal model exposed flaws, highlighting the lack of rigor in its design and implementation.
- Evolution of voting methods from ancient times to modern digital systems
- Challenges of secure and accurate vote tabulation
- Complexities of different electoral schemes and flaws in existing tabulators