Security in E-Voting

Motivation

E-voting systems are used in many countries for national or municipal elections as well as for elections within associations, societies, and companies. There are two main categories of such systems:

1. Electronic Voting machines: usually installed in polling stations, they include, among others, recording electronic votingsystems and scanners.
2. Remote Electronic Voting: used by voters to vote over the Internet through their own devices (e.g., desktop computers or smartphones).

E-voting systems are complex hardware/software systems and as in all such systems programming errors can hardly be avoided. Verification techniques and procedures are therefore used to ensure that these systems enjoy particular security properties, such as privacy (i.e., voters' choices remain confidential) and verifiability (i.e., checking that voters' choices have been properly counted).

In this reference scenario, we consider the verification of privacy properties of Java programs that use cryptographic operations, where the final aim is to provide strong cryptographic guarantees on the code of a fully fledged remote e-voting system which is designed to provide confidentiality of the votes.

Approach

While tools for verification of Java programs are available, including tools for checking noninterference properties, they cannot deal with cryptography.

A new framework has hence been developed to reduce the problem of checking cryptographic indistinguishability properties to check non-interference properties of Java programs. Using existing tools to prove noninterference properties, several case studies have been proved to enjoy cryptographic indistinguishability properties.

Moreover, the integration of these tools in our framework led to the development and the further improvement of the existing techniques for proving noninterference.

Solution

The CVJ framework

As already mentioned above, a framework (the CVJ framework) has been developed for the cryptographic analysis of Java programs which use cryptographic code [6, 7]. This framework enables existing tools that can check noninterference properties for Java programs, but a priori cannot deal with cryptography, to establish cryptographic indistinguishability properties at the code level.

The CVJ framework combines techniques from program analysis and universal composability, a well-established concept in cryptography. The idea is to first check noninterference properties for the Java program to be analyzedwhere cryptographic operations (such as encryption) are performed within so-called ideal functionalities (Figure 1b). Such functionalities typically provide guarantees even in the face of unbounded adversaries and can often be formulated without probabilistic operations and, therefore, they can be carried out by tools that a priori cannot deal with cryptography (probabilities, polynomially bounded adversaries). The results of the framework now imply that the original Java program (using actual cryptographic operations) enjoys strong cryptographic indistinguishability (Figure 1a).

As to checking non-interference, many program analysis tools can only deal with closed Java programs. The systems to be analyzed are, however, often open: they interact, for example, with an untrusted (and unspecified) network. Therefore, as part of the framework, we have proposed a proof technique that enables program analysis tools to verify noninterference properties of open systems (Figure 1c).

Hybrid Approach

Fully automated tools are often preferable over interactive, because with such tools program analysis is typically less time-consuming and requires less expertise. However, if automated tools fail due to false positives, the only option for proving noninterference is to drop the automated tools altogether and instead turn to fine-grained but interactive, and hence, more time-consuming approaches, such as theorem proving.

The hybrid approach [4] aims to overcome this unsatisfying "all or nothing" approach by combining the automatic nature of static information flow control tools with the ultimate precision of interactive theorem provers. The idea underlying this approach, as shown in Figure 2, is as follow:

1. If the verification of noninterference of a program using an automated tool fails due to (what we think are) false positives, then, following the rules of our approach, additional code is added to the program in order to make it more explicit and more clear for the automated tool that there is no illegal information flow, and by this, avoid false positives.
2. If the automated tool now establishes that the extended program enjoys the desired noninterference property, it remains to show that the extended program is a conservative extension of the original program. Intuitively, this means that the additional code did not change the behavior of the original program in an essential way, including, importantly, noninterference properties.
3. Proving that an extension is conservative requires to prove functional properties of (parts of) the program and will typically be carried out by an (interactive) theorem prover.

sElect: A Lightweight Verifiable E-Voting System

We have designed a new practical voting system called sElect (secure/simple elections) [5]. This system, which is implemented as a platform independent web-based application, is meant for low-risk elections and is designed to be particularly simple and lightweight in terms of its structure, the cryptography it uses, and the user experience. One of the unique features of sElect is that it supports fully automated verification, which does not require any user interaction and is triggered as soon as a voter looks at the election result.

The main components of the system are one (or several) voting booth(s), a collecting/ authentication server, a cascade of mix servers, and one (or several) bulletin board(s).

Casting phase.

As depicted in the figure at right, in the casting phase, every voter chooses a voting booth serving static HTML / CSS / Javascript to prepare her ballot. Each ballot contains the voter's choice (for example, the name of the candidate chosen by the voter) and an unique, randomly chosen verification code. To construct the ballot, the choice along with the verification code is encrypted several times with the public key of each mix server, from the last to the first. Such a (complete) ballot is then submitted to the collecting/authentication server which, if it accepts the ballot, replies by sending back a digitally signed receipt.

Tallying phase.
When the voting phase is over, the system enters the tallying phase (shown in the figure below). In this phase, the collecting/authentication server outputs the list of ciphertexts to the first mix server which decrypts the outer encryption layer, shuffles the inner ballots and sends the signed result both to the next mix server and to the bulletin board.

Next, the bulletin board reads the list of (unencrypted) ballots produced by the last mix server. It then publishes the resulting list containing the voters' choices along with verification codes, again in alphabetical order and digitally signed. This list constitutes the official result of the election process.

A demo version of the system is available at select.sec.uni-stuttgart.de.

Security Properties of sElect

Privacy. sElect provides confidentiality of the votes under the assumption that at least one of the mix servers is honest. The steps taken by an honest server, by design, hide the link between its input and output entries. Therefore, no one can link the ballot of a given voter to his/her choice-identifier-pair in the final output.

Verifiability. sElect provides two different ways through which each voter can make sure that her vote has been actually counted. A fully automated verification procedure is carried out by the voter's browser at the moment of looking the election result, checking whether her choice/verification code pair is in the list of choices/verification codes pairs produced by the last mix server.


Besides fully automated verification, sElect also supports a very easy to understand manual verification procedure: when visiting the bulletin board, a voter can check whether her verification code appears in the election result along with her choice.

Accountability. The automated verification procedure of sElect also performs certain cryptographic checks and, if a problem is discovered, it singles out a specific misbehaving party and produces binding evidence of the misbehavior. This provides a high level of accountability and deters potentially dishonest voting authorities.

Tools used for the verification of sElect

sElect is the first fully fledged remote voting system where cryptographic privacy of the votes has been proved at the code level. The core of each mix server, the component which is indeed designed to ensure privacy of the votes, is written in Java: Using the Hybrid Approach to prove noninterference and the CVJframework, it was possible to prove this code cryptographically secure. In particular, to check noninterference properties of this code, the following two tools have been used:

1. Joana [1] is a tool for the fully automatic analysis of non-interference properties of Java programs. It uses state-of-the art program analysis techniques to build a program dependence graph (PDG), a conservative approximation of all possible information flows inside a given program. The program has no illegal information flows if low sinks cannot be reached from high sources in the PDG. The absence of such paths can be checked by a program analysis technique called slicing. To maximize precision and reduce false alarms, Joana exploits flow-, field-, context-, object-sensitive program analyses. Moreover, it offers a wide variety of analysis options, e.g. to find sweet-spots between precision and scalability or to ignore flows with certain properties.
2. KeY [2, 3] is an interactive deductive verification tool of functional, relational and information flow properties of object-oriented software. The theorem prover is based on a sequent calculus for dynamic logic for Java (JavaDL), that precisely reflects the semantics of Java. Specifications can be given in the Java Modeling Language (JML) or RS3 Information Flow Langauge (RIFL).

Highlights

To outline the novelty and the contribution of the E-Voting reference scenario, we highlight the following three items:

• Establishing cryptographic properties at code level by checking non-interference [6, 7].
• Combining tools for proving non-interference [4].
• An e-voting system whose cryptographic component designed to provide privacy of the votes has been formally verified at the code level [5].

Publications