KOA: A Platform for e-Voting Experimentation
Kiezen op Afstand (KOA) is a Free Software Electronic/Remote/Internet Voting System developed for the Dutch government in 2003. "Kiezen op Afstand" is literally translated from Dutch as "Remote Voting." A version of this system was used in the European Parliamentary election of June 2004 and was subsequently released under the GNU General Public License.
As part of this work, the Security of Systems (SoS) Group at Radboud University Nijmegen wrote an independent tally application that was formally specified and (partially) verified using the Java Modeling Language (JML) and the Extended Static Checker for Java, ESC/Java2.
The version of KOA released by the Dutch government under the GPL was not complete. A number of pieces of functionality, constituting roughly 10% of the deployed KOA system, were proprietary and owned by the authors, LogicaCMG. Moreover, certain other changes were made for publication purposes (e.g., the length of public/private Key pairs was elided). This 10% has been reverse engineered and the entire system has been ported to an entirely Open Source foundation.
KOA is also being extended to support the Irish electoral system. This work is being carried out through the development of a plugin called Votáil. A Votáil's core is a full JML specification of the Irish vote counting system. This formal specification is derived from the complete functional specification for the election count algorithm as set out in Irish law. An implementation of this specification is being written at the moment using our verification-centric design by contract methodology.
Other work on KOA, as an experimental platform for electronic and remote voting, is continuing. First, we are identifying the core security properties of electronic and remote voting that must be formally specified at a high-level in a domain specific language, and verified by providing a methodology, both theoretical and practical, for translating such high-level specifications into concrete, low-level specifications and type-annotations with the intention of formally verifying these properties in KOA. Additionally, a MIDP-based remote voting applet has been developed at UCD. This application is being reviewed for possible incorporation into KOA, using the same verification-centric approach used in the rest of the KOA work.