There are many aspects to electronic voting and each of these involves risks: voter identification, separation of voter identity from vote, transparent vote auditing, network security and correct counting of votes, to name a few. Electronic voting has recently become a contentious issue in the United Sates of America due to the discovery of serious flaws in existing systems in almost each and every one of these aspects: for example see slashdot and NYT. In response there have been numerous calls for the code from electronic voting systems to be made available for public scrutiny so that experts can identify the risks inherent in the code: for example see David Dill's verified voting website.
David Dill also advocates the production of a physical paper ballot to enable a manual audit of the whole election process at a later date. Though paper ballots are hard evidence of which votes were cast, hand-counting is notoriously error-prone and time-consuming, and these problems are magnified when complex counting methods are used. For this reason we advocate the use of a verified electronic vote counting program. The counting program could be used within an electronic voting system, but could also be used to calculate election results by entering the paper ballots by hand, as was done in the ACT elections in 2001. Not only can such programs can be examined and used by anyone, but the proofs of correctness can be checked by independent experts.
Members of the Logic and Computation Group (NICTA) and the Computer Science Laboratory (ANU) are investigating the correct formalisation of legislation in vote counting programs. More specifically, can it be shown by mathematical means that the process or algorithm used by a vote counting program faithfully implements the legislation? We are confining ourselves to the vote counting algorithm only -- the rest of the entire electronic voting process, for example vote casting and security, is beyond the scope of our current activities.
Contrary to what one might expect, vote counting is not trivial and a wide variety of complex voting systems exist. The Australian Capital Territory (ACT) uses the Hare-Clark system and the ACT Electoral commission has an excellent website containing much information about this system. The Hare-Clark system is more complicated than many other voting systems, which is why we have chosen it as a case-study for our formalisation and verification process.
We believe that electronic voting systems should be considered as "mission-critical" systems, and therefore developed to a much higher standard of rigour than is everyday software. It is patently clear that many of the commercial electronic voting systems available on the market do not meet such criteria. We believe that modern techniques from Formal Methods and Software Engineering can be used to guarantee some of the necessary rigour. These pages describe our initial attempts to apply such techniques to modern electronic voting systems.
More details of this investigation will appear soon. Currently we are:
Once these tasks are complete, we will be able to prove that the Standard ML code obeys sensible and desirable properties as captured by our specification. Empirical testing will allow us to compare the results from the existing C code against the results from the verified system. While it may be too difficult to prove absolute correctness of the C code, it is possible to prove something about an individual result since a result from the C code that agrees with the verified code implies that the C code's result is provably correct.
A mathematical specification (formalisation) of the ACT Hare-Clark legislation is underway. This will eventually be used to prove the correctness of an implementation of the vote counting algorithm with respect to this specification. The implementation will probably be in some high level language such as Standard ML which has nicer properties if you want to actually prove something about the code. Details of the formalisation and process can be found on a separate page.
This formal specification was created by a person with no previous involvement in eVACS (see below): he worked independently and started from the English specification of Hare-Clark found at the ACT Electoral Commission website.
In 2001 the ACT Electoral commission used an electronic voting and vote counting system called eVACS. Some of the source code for this system is publicly available: in particular, the code that implements vote counting according to Hare-Clark. As part of our investigation, we took this code and built the necessary extra infrastructure to run the vote counting code. Details of building and experimenting with the eVACS counting code can be found on a separate page.
To gain experience in developing vote counting programs from specifications written in natural language (English) and to better understand the ACT Hare-Clark legislation, we built our own in-house Hare-Clark vote counting program using the programming language C. In particular, this program was written by a trained lawyer who had no previous experience with eVACS. Details and experimental results. Disclaimer: this program was developed in a short period period of time by a single person. It is not intended to be a reference program, and is provided here simply for information purposes. We do not intend to develop this program further.
Jeremy Dawson developed a prototype Hare-Clark vote counting program using the programming language Standard ML during the conception of eVACS. Details and experimental results.
|
Site Map and Table of Contents |
Disclaimer |
Page content Copyright 2003 NICTA
|