« Galois Tech Talk: Specializing Generators for High-Performance Monte-Carlo Simulation in Haskell | Main | Equivalence and Safety Checking in Cryptol »
Monday
Mar022009

Trustworthy Voting Systems

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.

Reader Comments (7)

I wish that folks writing about voting systems would stop using the word "privacy" when it comes to securing secret ballots. The characteristic of a secret ballot is SECRECY, not privacy, and they are not the same thing. Basically a secret ballot system has to be receipt-free while a private ballot system does not.

All this cryptographic stuff seems like a waste of time too, unless a way is provided to verify that the code running inside the counting machine is the same as the code that has been certified. Part of the regulatory structure of the Las Vegas casino gambling industry includes that 1) ROM code is submitted as part of the certification process for a given new model of slot machine; and 2) inspectors from the gambling commission can come into a casino at any time, pull slot machines out of service, yank the roms out, and verify that the machine isn't running rigged code. Unfortunately it's a lot easier to technologically defeat such inspections now than it was decades ago when those rules were written.

Fortunately there's a much simpler way to verify optically scanned ballots. The election commission runs a scanning machine that scans all the ballots and creates the official scans, which are uploaded to the internet so anyone can download them and run their own counting software. Also, representatives of the major candidates are invited to bring their own scanning equipment, so the stack of ballots is scanned 3 times (once by the election commission, once by the democrats, and once by the republicans). All three sets of scans go up on the web. Any significant discrepancies are resolved with a hand recount. Done.

March 2, 2009 | Unregistered Commenterpaul

I agree with all the major points in this article and look forward to seeing complete formal specifications for voting systems.

In response to the previous comment, publishing the unencrypted ballots is not an option. In particular with PRSTV/IRV there are enough preferences on each ballot paper to allow for the possibility of vote signing (a.k.a. 'The Italian Attack'. There has been recent work (see EVT08) which shows how to count ballots cryptographically.

March 3, 2009 | Unregistered CommenterDermot Cochran

I easily grant that galois has a lot of awesome technology (and I would consider working there if they weren't in the US), but basically they all guard against threats that aren't relevant or applicable in voting systems.

Formal verification is a way to guard against accidental malfunction. Airplanes need working software to not crash. But: The easiest way to bring down an airplane is not to maliciously modify its operating software, but to get a stinger. The easiest way to make an election malfunction in a tiny way *is* to modify the election software.

Likewise does the trusted services engine provedly guard against accesses from the wrong side, but it does not guard against physical attack on the machine.

Where I'm voting now, I can just volunteer to work in the election office or even stay after the election closes and watch how the ballot boxes are opened and the contents counted. Those numbers must appear on the official lists for the election.

When there is a machine doing the tallying, I need a degree in formal methods to verify the proof for the software as well as the proover itself - in short: *all* the software that was used to build the voting engine. How many voters are going to do that? Or even are able to do so: in germany the operating software of some election machines is under a trade secret of the vendor, and only some government agencies are even allowed to look at the code.

And finally: How am I supposed to find out whether the engine is actually running the verified and licensed version of the software (and of the setup of the current election)?

The simultaneous requirements for openness of the voting in total and the anonymity of the individual ballot are ridiculously simply implemented with a ballot box and equally ridiculously complicated to do with machinery.

March 3, 2009 | Unregistered CommenterAndreas Krey

In response to the comments I've received on this post, I'd like to make a few clarifications.

First, the distinction between secrecy and privacy is indeed a good one, and one I didn't give it sufficient thought. Thanks for pointing it out.

Second, I'd like to say that I don't make any claims that the approach proposed in this posting is complete. A practical, trustworthy system will certainly depend on mechanisms beyond software. Physical security is important for some of the computer systems that this approach would use, and the existing safeguards in place to protect the integrity of manual, paper-only elections are still important.

However, it's important to also point out that the number of computers that need to be trusted for this system to work is fairly small. The posting does not, in any way, advocate touch-screen voting machines, or any similar technology. The methods cited work with pen-marked paper ballots and unmodified optical scanners. The scanners need not be trusted, as any malfunction can be detected by the public. The onlycomputer system that needs to be trusted is the one that creates ballots. There may be one of these machines in each precinct, or each county, but probably no more. It is certainly important to verify that this machine is running the intended software, and is protected from tampering.

Third, there's a key property that I didn't adequately emphasize in the original posting that systems like Scantegrity have, and that no voting system in widespread use can claim. This property is the ability to check that an individual vote was recorded correctly (not just that the total is correct) without allowing a voter to prove that he or she cast a particular vote. It would certainly be much less appealing to implement an electronic system that has no benefits over a purely paper-based process.

The alternative option of posting a scanned image of each ballot in a public place has two problems: a) it allows voters to make distinguishing marks on their ballots (though policy could dictate that such ballots always be rejected, as I believe they already are), and b) there is still no way to verify an individual vote. Schemes based on cryptography, while certainly more complex, can provide a high degree of confidence that all cast votes are included. Only a tiny percentage of the voting population need check their votes in order to make the probability of fraud effectively zero. The same mechanism also makes it very difficult to inject fraudulent votes, because each vote needs to be verifiable against a secret key.

A final point is that there is one major legal impediment to the adoption of such a voting system. Some states require that unmarked ballots be identical. In the Scantegrity system, each ballot contains a random code under each bubble, invisible at first but revealed by special in in the marking pen. In addition, each ballot is marked with a unique serial number. However, it may be sufficient that all unmarked ballots are visually indistinguishable, which is certainly achievable.

March 9, 2009 | Unregistered CommenterAaron Tomb

The remarks about publishing scanned ballots are well taken. The solution may have to be to not allow the voter to touch the ballot. The voter makes selections on a touch screen and hits "confirm". That generates a printed ballot that the voter can see through a glass window. The voter is advised that if there is a discrepancy between the on-screen vote and the printed ballot, s/he should summon the officials. On pressing "done" the ballot is (visibly) dropped into a ballot box.

Cryptographic verification that a particular vote was counted is practically useless. Imagine attempts to use it in the ongoing Minnesota senate election contest (the two candidates are separated by a few hundred votes out of millions) or the notorious Florida 2000 contest. Do you really expect millions of voters to all run a cryptographic verification on some bunch of weird numbers? Otherwise there's no way to detect a few thousand votes being added, or for that matter a few thousand being flipped or suppressed in areas where voters tend not to be computer literate. We already know that in every election, some votes are lost due to procedural errors or the like. Cryptography just doesn't sound like an effective way to tell when this is done maliciously. The old system of keeping paper ballots locked up under constant observation by representives of the candidates is a lot more effective if done without gaps.

March 11, 2009 | Unregistered Commenterpaul

While the system you describe is one of the most convincing I have seen, I still believe the problem is not a technological one. These are some toughts I had when my governement stated that since they used some quantum technology to transmit the ballots to a central database, the system was secure :

Apart from the laudable statement, I believe the biggest mistake was to remove the humans from the process. Given a big enough and generally well behaving crowd to count the votes, it has been verified that abuse could be limited and detected. This is possible because the process is simple enough that each person involved can verify what's going on.

By throwing cryptography and other technologies into the process, you effectively reduce the number of people who can be involved and thus increasing the risks of fraud, which I find kind of ironical because, if the system is secure, you will probably have less errors, but on the other hand if the system is corrupted, it may be completely.

All this may sound anti-technological but I am not. It's just that I believe enineers where given a problem and instead of improving the proven and existing one, they, as usual, decided to re-invent the whell (or voting in that case).

Hope this brings another interesting point of view.Cheers, zimbatm

March 25, 2009 | Unregistered Commenterzimbatm
This is really amazing to see schools and corporates updating to the latest information technology trends.
July 8, 2011 | Unregistered Commenterhand held clickers

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Post:
 
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>