Full Verification of the KOA Tally System

Note: This project was accomplished as a 2004-2005 Final Year Project by Fintan Fairmichael (report).

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Software Engineering
  • Pre-requisites Good knowledge of Java, basic knowledge of encryption and security
  • Co-requisites (things you must learn along the way) Knowledge of JML, ESC/Java2, and program verification will be obtained during the course of this project
  • Subject Coverage Electronic and Internet Voting Systems, Formal Specifications, Extended Static Checking, Verification
  • Project Type Applied Research
  • Hardware/Software Machine running anything but Windows

Description

The Kiezen op Afstand (KOA) system is the world's first Open Source Internet Voting System. The KOA system was designed, developed, tested, and deployed by LogicaCMG, a Dutch consulting firm, under contract with the Dutch Government. The KOA system was Open Sourced by the Dutch Government under the GPL license in July of 2004, partially due to the influence of my previous research group (the Security of Systems [SoS] Group at the University of Nijmegen).

Early in 2004 the SoS group, under contract with the Dutch Government, implemented a vote tally application. This application was used to count the votes cast by Dutch expatriates in the recent EU elections.

The tally application was designed, formally specified, implemented, and tested by three Ph.D.s in six weeks. The core of the system was best-effort verified with ESC/Java2, and the rest of the system was tested using a combination of the JML runtime assertion checker and the JML unit test generator.

The purpose of this project is to complete the formal specification and verification of the KOA vote tally application.

Mandatory Goals

  1. Gain familiarity with JML, ESC/Java2, and the KOA system.
  2. Perform a code review of the KOA vote tally application.
  3. Measure specification and unit test coverage.
  4. Determine an appropriate approach for completing extra-core specifications.
  5. Determine appropriate (pseudo-)verification goals. How much of the architecture should have 100% ESC/Java2 coverage? How much only need complete JML unit test generation and coverage?
  6. Perform verification and testing. Correct problems with KOA code and specs and report bugs for problems and limitations of ESC/Java2 and JML tools.
  7. Post new version of KOA tally application to the world. Fame and fortune follow.
  8. Write, submit, and publish a paper on the results.

Discretionary Goals

  1. Some classes on which the KOA tally application depends do not yet have specifications. In particular, pieces of the java.security, javax.crypto, org.w3c.dom, and org.xml.sax packages need more specification. Any specifications written for classes in these packages is of great benefit to the Java community and your name goes up in lights for all time, as specifications are written once and kept forever.

Exceptional Goals

  1. If we get 100% verification coverage of the KOA tally application you win an M.S. degree. :)

Sources of Information and Preparatory Reading

  1. Formally Counting Electronic Votes (But Still Only Trusting Paper)
  2. The JML web site
  3. The ESC/Java2 web site
  4. Read the two recent papers available via the JML web page: "An overview of JML tools and applications" and "JML: notations and tools supporting detailed design in Java".
  5. Read introduction to J2EE technologies.
  6. Read about Open Source J2EE and web services like JBoss, Tomcat, etc.
  7. Download, install, and play around with the JML tool suite and ESC/Java2 to get a feel for the technology.
  8. Download, install, run, play around with the full KOA system and the JML annotated vote counting software available from UCD's KOA web pages