Kiezen op Afstand 2004

See also RIES-KOA: 2006.

KOA stands for Kiezen Op Afstand and denotes an experiment in voting over the Internet conducted by the Dutch government. The experiment was specifically conducted for the European elections in June 2004.

The Security of Systems group was actively involved in this project. In 2003, a blackbox test was conducted to analyze the security of the voting system and its network connection. Furthermore, the group participated in an expert panel. One of the panel's recommendations was to hire an independent third party to verify the election outcome. This recommendation was adopted by the ministry and they issued a bid request to write the tallying software. The SoS group wrote a proposal to write the software, and in the bid the use of formal methods was emphasized. Somewhat to our own surprise, we won the bid. From communication with the ministry, we learned that they made a very conscious choice for the use of formal methods in order to increase the level of trust in the application.

The resulting tally application was written in Java. The specifications were written in JML, the Java Modeling Language. This language is gaining popularity in helping specify correct Java programs and verify their correctness. JML's popularity is partly due to the many available tools that support it. Tools are available for JML for every task from documentation generation to unit testing to runtime checking to full formal verification. Because of the limited time for this project, it was decided to only use fully automatic tools, including the runtime assertion checker JMLRAC and the static checker ESC/Java2.

Of course, these tools will not work without specifications. We have tried to stick with the principle of writing specifications first and then write an implementation. However, we have to admit that the desire to quickly write some code and test it (on example files) was sometimes too tempting. This was especially true for relatively "boring" parts of the program, such as user interface code. We have done our best to add specifications for such code afterwards.

The core parts of the systems though, including the key data structures, counting votes, and summarizing data, were all written in a specification-first Design by Contract fashion. In fact, much of this part of the KOA tally application were verified correct in a just-in-time fashion. I.e., all specs were written first and each new method was written and verified immediately, before proceeding on to the next method.

Download

Not ready yet...

• koa.zip: The version of the application being used during the official counting.
• jml_java.zip: JML annotations for java.lang and java.security.
• jml_javax.zip: JML annotations for javax.crypto, javax.swing and javax.xml.
• jml_org.zip: JML annotations for org.xml.
• ESC/Java2: Uniting ESC/Java and JML, which describes KOA as a case study.

The KOA source code is distributed by the Dutch government under a GPL license, and is available from the OsOss site. However, because this site is in Dutch, it might be difficult to find the actual source there. Therefore we have included a downloadable version here as well.

Documentation by the ministry

The ministry of the Interior and Kingdom Relations provides a lot of documents. Unfortunately they are all in Dutch.

• Voortgangsrapportage Kiezen op Afstand 2004
• Evaluatierapport stemmen per internet en per telefoon
• Kiezen op afstand in het buitenland
• Begeleidende brief commissie internet- en telefoonstemmen voor de kiezers in het buitenland

1. Verslag van de uitvoering van het experiment internet- en telefoonstemmen
2. • Mededeling locatie stembureau Staatscourant
   • Benoemingsbesluit leden evaluatiecommissie
   • Experimentenregeling
   • Aanwijzingsbesluit experimenten KOA
   • Aanwijzing deskundige stemmen via internet en telefoon
   • Benoemingsbesluit stembureauleden Staatscourant
   • Experimentenbesluit definitief
   • Experimentenwet Staatsblad
3. • Vragenlijst briefstemmers
   • Vragenlijst internetstemmers
4. Vragenlijst ten behoeve van de evaluatie van de leden van het internet- en telefoonstembureau
5. • Adresdrager
   • Overzicht kandidaten detailopname
   • Overzicht kandidaten voorzijde
   • Overzicht kandidaten achterzijde
   • Handleiding kiezer
6. Overzicht uitgevoerde testen
7. Specificatie functionele eisen

For more information, contact Engelbert Hubbers.