Project Background
Electronic voting systems (e-voting) have the purpose of collecting and counting votes in elections. For this, e-voting systems implement electoral systems such as Single Transferable Vote (STV) [1] or Condorcet methods [2], which are algorithms to determine the winner (or winners) of an election based on some set of submitted votes. E-voting systems are widely applied on all levels, including national elections in various countries.
Because elections matter, it is important that e-voting systems handle and count votes correctly. Implementations of e-voting therefore have to be validated extremely carefully, in particular to ensure that there are no corner cases in which voters might trick the voting systems into counting wrongly. This project (external link, opens in a new window) is about creating a simple e-voting system that is formally verified, establishing the correctness of the e-voting system on the highest level of confidence possible.
The project will go through the typical phases of creating verified software:
- Analysis:
- Familiarising with the algorithm to be implemented, in this case electoral systems.
- Development of a prototype to fully understand the electoral system. The prototype can be implemented in any programming language.
- Collection of requirements.
- Design:
- Architectural and detailed design of the implementation.
- Translation of requirements to formal specifications, capturing relevant correctness properties.
- Implementation:
- Implementation of the electoral system in a verification-oriented programming language.
- Verification:
- Careful testing of the implementation, comparison with the prototype.
- Formal verification of the different parts of the implementation, with respect to the formal specification established.
- Extraction of an executable software program.
The project is iterative and open-ended. The plan is to start with a very simple electoral system (e.g., simple majority voting), moving on to more sophisticated electoral systems as the group gets more experienced.
The main programming language to be used in the project is Dafny [3,5], a verification-oriented language that is widely used in industry. For inspiration, you may watch the presentation [4] explaining how the Amazon Web Services authentication engine, a software program that is called and executed by the Amazon cloud more than 1 billion times per second, was redeveloped and verified using Dafny.
It is recommended to take this programming project in parallel with the course “Logic and Formal Methods”, which will provide the right background in logic, formal specification, formal verification, and also introduce the Dafny language.
[1] https://en.wikipedia.org/wiki/Single_transferable_vote (external link, opens in a new window)
[2] https://en.wikipedia.org/wiki/Condorcet_method (external link, opens in a new window)
[3] https://dafny.org (external link, opens in a new window)
[4] https://youtu.be/oshxAJGrwMU?si=RYlNKVufXE63AiJj (external link, opens in a new window)
[5] Program proofs. K. Rustan M. Leino. The MIT Press, 2023.
Organization
- Number of participants: 3-6
- Kick-off meeting: in the week from April 28
- Submission deadline: end of August