Formal Verification of Voting Schemes

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
... mehr
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.