Formal Verification of Voting Schemes

@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}
}