Formal Verification of an Electronic Voting System

Technical Report

Author(s):Daniel Bruns
Institution:Department of Informatics, Karlsruhe Institute of Technology
Series:Karlsruhe Reports in Informatics
Number:2014-11
Year:2014
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000042284

Abstract

Electronic voting (e-voting) systems that are used in public elections need to fulfil a broad range of strong requirements concerning both safety and security. Among these requirements are reliability, robustness, privacy of votes, coercion resistance and universal verifiability. Bugs in or manipulations of an e-voting system may have considerable influence on the life of the humans living in a country where such a system is used. Hence, e-voting systems are an obvious target for software verification. In this paper, we report on an implementation of such a system in Java and the formal verification of functional properties thereof in the KeY verification system. Even though the actual components are clearly modularized, the challenge lies in the fact that we need to prove a highly nonlocal property: After all voters have cast their votes, the server calculates the correct votes for each candidate w.r.t. the original ballots. This kind of trace property is difficult to prove with static techniques like verification and typically yields a large specification overhead.

BibTeX

@TechReport{Bruns14,
  author	= {Daniel Bruns},
  title		= {Formal Verification of an Electronic Voting System},
  year		= 2014,
  month		= aug,
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  language	= {english},
  number	= {2014-11},
  series	= {Karlsruhe Reports in Informatics},
  url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000042284},
  urn		= {urn:nbn:de:swb:90-422842},
  issn		= {2190-4782},
  license	= {http://creativecommons.org/licenses/by-nc-nd/3.0/},
  abstract	= {Electronic voting (e-voting) systems that are used in
		   public elections need to fulfil a broad range of strong
		   requirements concerning both safety and security. Among
		   these requirements are reliability, robustness, privacy of
		   votes, coercion resistance and universal verifiability.
		   Bugs in or manipulations of an e-voting system may have
		   considerable influence on the life of the humans living in
		   a country where such a system is used. Hence, e-voting
		   systems are an obvious target for software verification.
		   
		   In this paper, we report on an implementation of such a
		   system in Java and the formal verification of functional
		   properties thereof in the {\KeY} verification system. Even
		   though the actual components are clearly modularized, the
		   challenge lies in the fact that we need to prove a highly
		   nonlocal property: After all voters have cast their votes,
		   the server calculates the correct votes for each candidate
		   w.r.t.\ the original ballots. This kind of trace property
		   is difficult to prove with static techniques like
		   verification and typically yields a large specification
		   overhead.}
}