Formal Verification of Voting Schemes

Diplomarbeit

Autor(en):Michael Kirsten
Hochschule:ITI Beckert, Karlsruhe Institute of Technology
Jahr:2014
PDF:

Abstract

Fundamental trust and credibility in democratic systems is commonly established through the existence and execution of democratic elections. The vote-counting of an election, usually formalised by a voting scheme, essentially boils down to a mechanism that aggregates individual preferences of the voters to reach a decision. For this matter, there are various differing voting schemes in use throughout the world, commonly based on high expectations and means to ensure a sensible democratic process. However, incidents such as the ruling by the German federal constitutional court which led to a change of the German legislation in 2013 manifest that it is difficult for a voting scheme to meet these legitimate expectations. In fact, there is no general notion of correctness for a voting scheme and thus no universal mechanism as shown in Kenneth J. Arrow’s Impossibility Theorem in 1951. As a consequence, designing a real-world voting scheme without flaws, which still gives significant democratic guarantees, is a difficult task as a trade-off between desirable properties is non-trivial and error-prone.
The approach in this thesis is based on the idea to tackle this issue by proposing an incremental and iterative development process for voting schemes based on automated formal reasoning methods using program verification. We analyse two different forms of verification considering their role in this development process in order to achieve formal correctness of voting schemes. We perform a comprehensive set of case studies by applying "medium-weight" and "light-weight" verification techniques. The "medium-weight" approach uses the annotation-based deductive verification tool VCC based on an auto-active methodology and the "light-weight" technique is performed with the bounded model checking tool LLBMC. Our analysis covers a set of well-known voting schemes combined with a set of prominent voting scheme criteria. In addition to giving precise formalisations for these criteria adapted to the specific voting schemes and tools used, we advance the efficiency of the "light-weight" approach by exploiting fundamental symmetric properties. Furthermore, we investigate on encountered challenges posed by the auto-active verification methodology, which lies in-between automatic and interactive verification methodologies, with respect to specific characteristics in voting schemes and also explore the potential of bounded verification techniques to produce precise counterexamples in order to enhance the capability of our envisioned development process to give early feedback. This thesis gives fundamental insights in general challenges and the potential of automated formal reasoning with the goal of correct voting schemes.

BibTeX

@MastersThesis{KirstenDA2014,
  author	= {Michael Kirsten},
  title		= {Formal Verification of Voting Schemes},
  school	= {ITI Beckert, Karlsruhe Institute of Technology},
  month		= dec,
  year		= {2014},
  location      = {Karlsruhe, Germany},
  abstract	= {Fundamental trust and credibility in democratic systems is commonly established 
  		   through the existence and execution of democratic elections. The vote-counting 
  		   of an election, usually formalised by a \emph{voting scheme}, essentially boils 
  		   down to a mechanism that aggregates individual preferences of the voters to 
  		   reach a decision.
  		   For this matter, there are various differing voting schemes in use throughout 
  		   the world, commonly based on high expectations and means to ensure a sensible 
  		   democratic process.
  		   However, incidents such as the ruling by the German federal constitutional court 
  		   which led to a change of the German legislation in 2013 manifest that it is 
  		   difficult for a voting scheme to meet these legitimate expectations.
  		   In fact, there is no general notion of correctness for a voting scheme and thus 
  		   no universal mechanism as shown in Kenneth J. Arrow’s \emph{Impossibility Theorem} 
  		   in 1951.
  		   As a consequence, designing a real-world voting scheme without flaws, which still 
  		   gives significant democratic guarantees, is a difficult task as a trade-off 
  		   between desirable properties is non-trivial and error-prone.
  		   \newline

  		   The approach in this thesis is based on the idea to tackle this issue by proposing 
  		   an incremental and iterative development process for voting schemes based on 
  		   automated formal reasoning methods using program verification.
  		   We analyse two different forms of verification considering their role in this 
  		   development process in order to achieve formal correctness of voting schemes.
  		   We perform a comprehensive set of case studies by applying ``medium-weight'' and 
  		   ``light-weight'' verification techniques.
  		   The ``medium-weight'' approach uses the annotation-based deductive verification 
  		   tool VCC based on an \emph{auto-active} methodology and the ``light-weight'' 
  		   technique is performed with the bounded model checking tool LLBMC.
  		   Our analysis covers a set of well-known voting schemes combined with a set of 
  		   prominent voting scheme criteria.
  		   In addition to giving precise formalisations for these criteria adapted to the 
  		   specific voting schemes and tools used, we advance the efficiency of the 
  		   ``light-weight'' approach by exploiting fundamental symmetric properties.
  		   Furthermore, we investigate on encountered challenges posed by the 
  		   \emph{auto-active} verification methodology, which lies in-between automatic 
  		   and interactive verification methodologies, with respect to specific 
  		   characteristics in voting schemes and also explore the potential of bounded 
  		   verification techniques to produce precise counterexamples in order to enhance 
  		   the capability of our envisioned development process to give early feedback.
  		   This thesis gives fundamental insights in general challenges and the potential 
  		   of automated formal reasoning with the goal of correct voting schemes.},
  language	= {english},
  type		= {Diplomarbeit}
}