Verifying security properties in electronic voting machines

Voting is the bridge between the governed and government. The last few years have brought a renewed focus onto the technology used in the voting process and a hunt for voting machines that engender confidence. Computerized voting systems bring improved usability and cost benefits but also the baggage of buggy and vulnerable software. When scrutinized, current voting systems are riddled with security holes, and it difficult to prove even simple security properties about them. A voting system that can be proven correct would alleviate many concerns. This dissertation argues that a property based approach is the best start towards a fully verified voting system. First, we look at specific techniques to reduce privacy vulnerabilities in a range of voting technologies. We implement our techniques in a prototype voting system. The componentised design of the voting system makes it amenable to easily validating security properties. Finally, we describe software analysis techniques that guarantee that ballots will only be stored if they can later be accurately reconstructed for counting. The analysis uses static analysis to enable dynamic checks in a fail-stop model. These successes provide strong evidence that it is possible to design voting systems with verifiable security properties, and the belief that in the future, voting technologies will be free of security problems.