KOA is a free electronic voting software created for the Netherlands government in 2003. The software enables remote and internet voting.
The Security of Systems (SoS) Group at Radboud University Nijmegen developed an independent tally application that was formally specified and partially verified using the Java Modeling Language (JML) and the Extended Static Checker for Java as part of KOA. With this application, users can be assured of secure and accurate vote tallying.
However, the version of KOA released by the Dutch government under the GPL was not complete as certain pieces of functionality, constituting roughly 10% of the deployed KOA system, were proprietary and owned by the authors, LogicaCMG. Despite this, reverse engineering was done, and the entire system was ported to an entirely open-source foundation.
Presently, KOA is being extended to support the Irish electoral system through the development of a plugin named Votáil. 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.
As an experimental platform for electronic and remote voting, other work on KOA is continuing. For instance, the core security properties of electronic and remote voting must be formally specified at a high-level in a domain-specific language. At the same time, a methodology, theoretical and practical, for translating such high-level specifications into concrete, low-level specifications and type-annotations will be provided to ensure that these properties are formally verified in KOA.
Additionally, a MIDP-based remote voting applet has been developed at UCD, and it is currently being evaluated for possible incorporation into KOA, using the same verification-centric approach used in the rest of the KOA work. Overall, KOA is an important software application for safe and secure remote voting, and its potential is still being harnessed.
Version 2.0.0: N/A