Accurate and reliable elections are a critical component of an effective democracy. However, completely secure and trustworthy voting procedures are difficult to design, and no perfect solutions are known. Ideally, a trustworthy voting system should guarantee both verifiability (the ability to prove that the counted vote matches the submitted ballots) and privacy (the inability to link the contents of a vote with the voter who cast it).These guarantees may now be achievable. Many researchers have proposed voting protocols that achieve verifiability and privacy in theory, and a few do so under assumptions that are satisfied by current election practices. Most of the protocols involve posting an encrypted version of the contents of every ballot in some public place (likely a web site), and depend on the properties of cryptographic operations to achieve privacy while allowing anyone to verify the final tally.Now that practical, secure voting protocols exist, the time has come to bring them into use. One existing solution that comes close to achieving these goals while retaining compatibility with current voting practices is the Scantegrity II system. It has the advantage that it can operate under current US election conditions, without requiring any modification to existing optical ballot scanners, and with very little change to the individual voting process.However, the software used in this system is only a prototype, with a number of shortcomings. Voter privacy depends on ability of a computer system to keep a key database completely secret, and accurate vote counting depends on the correct implementation of complex cryptographic algorithms. The software is tens of thousands of lines of code, and as with any other software of that size, many bugs certainly exist.We believe that the importance of trustworthy election results and the past lack of success in creating reliable solutions warrants a new approach to the design of voting systems. In particular, we advocate a class of techniques known as formal methods that allow us to make precise mathematical assertions about how software should behave, and determine whether it satisfies those assertions. Government agencies within the Department of Defense make use of formal methods to ensure the reliability of important computer systems, and the draft update to the development standards used by the Federal Aviation Administration, DO178C, includes provisions for the use of formal methods. Voting systems deserve similar care.
One Approach
Formal Methods
Software designers employ a number of techniques to combat the difficulty of producing correct software. At the simple extreme, running the software directly through a few scenarios that match expected operating conditions and observing the results can help eliminate egregious mistakes, but does little to prevent subtle mistakes or malicious attacks. Most software, including that in existing voting machines, undergoes little more than this preliminary sanity checking.The goal of formal methods is instead to prove that a piece of software necessarily behaves properly under all possible circumstances. The first step toward this goal is to make a connection between the concrete software and some well-defined mathematical model. It can be possible to extract a model directly from the concrete software. Alternatively, software architects can build the model first, and derive the concrete software from the mathematical abstraction.In either case, the connection between the model and the concrete software should be such that a proving a property of the model guarantees that the property holds of the software.
A Formal Model of the Voting Process
We advocate developing a formal model of the complete pipeline of voting events, including ballot creation, vote marking, ballot recording or scanning, ballot aggregation and counting, and final certification. If described appropriately, in a fully-executable language, portions of this formal model can be used directly in a software implementation. This method of software development also makes feasible a wide variety of techniques to gain confidence in the correctness of the software, potentially including a complete formal proof of correctness for key components. It has the additional benefit of allowing us to make confident statements about the security and reliability of the non-computerized stages of the process.The Voluntary Voting System Guidelines recommendation released in 2007 by the National Institute of Standards and Technology makes significant steps toward a formal definition of voting, going as far as including UML process diagrams and mathematical descriptions of a few important properties. We advocate taking this work a step farther, and describing as much of the process as possible in a precise, formal, and machine-readable language.
High-Assurance Cryptography
Voting protocols that provide simultaneous guarantees of integrity and privacy typically depend heavily on the properties of cryptographic algorithms. While, in theory, these algorithms transform data in ways that achieve the properties necessary for trustworthy voting, it is absolutely critical that the algorithms be implemented properly. Recent work has made significant progress toward high-assurance cryptography. Researchers at Stanford have done work to formally verify that Java code implementing a cryptographic algorithm matches a specification written in a functional language. Galois’ own programming language, Cryptol, is also a functional language, designed specifically for implementation of cryptographic algorithms at a high level of abstraction, and also allows the high-level specification to be proven equivalent to code generated in C or VHDL. The use of a functional language in both approaches allows developers to describe cryptographic algorithms in a form that closely resembles their mathematical specification, making it significantly easier to gain confidence in their correctness.The existence of these approaches demonstrates the feasibility of high-assurance implementations of cryptographic algorithms. These specific technologies may or may not be the most appropriate solutions for a standard, highly trustworthy voting system, but they show that such a system can be built.
Guaranteed Privacy
Secure voting protocols often depend on the secrecy of certain pieces of information to protect voter privacy. To prevent vote buying and voter intimidation, it must be infeasible to prove that a specific voter cast a particular vote. Technology exists to provide this guarantee, as well. Work on cross domain solutions has resulted in a number of highly trustworthy systems. As an example, Galois’ Trusted Services Engine (TSE) includes a software component that enforces strong separation between different information domains. A formal proof of correctness, designed for evaluation at EAL6, guarantees that private information can never be accessed by unauthorized parties. General Dynamics also has a whole suite of products aimed at this market.In the context of voting systems, a cross domain component could be used to protect the database used to generate ballots. This database could be inaccessible to any human user, while still allowing auditors, and even the general public, to view the data necessary to tally votes, and verify that any particular vote was recorded correctly. Though these existing systems, as they stand, may not be entirely appropriate for use in a voting system (none of them are available to the general public, for instance) they do show that it is feasible to gain a high degree of assurance in the separation of secret and public data.
Openness
Because of the importance of voting to an effective democracy, and the temptations to subvert the process, we believe that transparency is essential. Therefore, we advocate that all software source code, design documents, and assurance artifacts involved in a voting system be made freely available to the public (either in the public domain or under an OSI-approved open source license). In particular, any interested party should be able to obtain the source code and use it to build executable software identical to that stored in the voting systems in use.
Conclusion
We argue that a key component of a secure voting system is trustworthy software that is developed using the best known assurance techniques and completely open to public inspection. In addition, the essence of the voting process should remain software independent, in that a manual recount should always be possible. Higher software reliability should make the necessity of a hand recount less common, but software should never be designed in such a way that a hand recount is impossible, or even more difficult than it would be in a completely manual election.