Trust through software independence and program verification

Here are four considerations that explain the unmet needs of this proposed project.

1. Voting protocols have become increasingly popular and will be more widely deployed in the future as a result of an ongoing digitalization effort of democratic processes.
2. Elections are based on trust, which means that election systems ideally should be based on algorithms and data structures that are trusted.
3. Program verification techniques are believed to strengthen this trust.
4. Greenland laws were recently changed to allow for Internet Voting.

The integrity of an election result is best captured through software-independence in the sense of Rivest and Wack’s definition “A voting system is software-independent if an undetected change or error in its software cannot cause an undetectable change or error in an election outcome.” Software independence is widely considered a precondition for trust. The assumption that program verification increases trust arises from the fact that those doing the verification are becoming convinced that the system implements its specification. However, the question is if these arguments also convince others not involved in the verification process that the verified system can be trusted, and if not, under which additional assumptions will they trust?

Thus, the topic of this project is to study the effects of program verification on public trust in the context of election technologies. Therefore, this project is structured into two parts. First, can we formally verify software dependence using modern program verification techniques and second, is software-independence sufficient to generate trust.

The research project aims to shed more light on the overall research question, if formal verification of software-independence can strengthen public confidence. Affirming this research question in the positive would lead to a novel understanding of what it means for voting protocols to be trustworthy, it would lead to an understanding how to increase public confidence in Internet Voting, which may be useful for countries that lack trust in the security of paper records.

(RO1) Explore the requirement of software-independence in the context of formal verification of existing Internet voting protocols.

(RO2) Study the public confidence in Greenland with respect to software-independence and formally verified Internet Voting protocols and systems.

Software Independence

In order to achieve (RO1), we will consider two theories of what constitutes software-independence. There is the game-theoretic view, which, similar to proof by reduction and simulation in cryptography, reduces software-independence of one protocol to another. The statistical view gives precise bounds on the likelihood of the election technology to produce an incorrect result. We plan to understand how to capture formally the requirement of software-independence by selecting existing or newly developed voting protocols and generate formally verified implementations. For all voting protocols that we design within this project, we will use proof assistants to derive mechanized proofs of software independence.

User Studies

To achieve (RO2), we will, together with the Domestic Affairs Division, Govern-ment of Greenland study the effects of formal verification of software independence on public confidence. The core hypothesis of these studies is that strategic communication of concepts, such as software inde-pendence, can be applied in such a way that it strengthens public confidence. We will invite Greenland voters to participate in pilot demonstrations and user studies and will evaluate answers qualitatively and quantitatively.

Scientific value
Internet voting provides a unique collection of challenges, such as election integrity, vote privacy, receipt-freeness, coercion resistance, and dispute resolution. Here we aim to focus on election integrity, and show that if we were to verify formally the property of software-independence of a voting system that would increase the public confidence of the voters in the accuracy of the election result.

Capacity building
The proposed project pursues two kinds of capacity building. First, by training the PhD student and university students affiliated with the project, making Denmark a leading place for secure Internet voting. Second, if successful, the results of the project will contribute to the Greenland voting project and to international capacity building in the sense that they will strengthen democratic institutions.

Societal value
Some nations are rethinking their respective electoral processes and the ways they hold elections. Since the start of the Covid-19 pandemic, approximately a third of all nations scheduled to hold a national election, have postponed them. It is therefore not surprising that countries are exploring Internet Voting as an additional voting channel. The result of this project would contribute to making Internet election more credible, and therefore strengthen developing and post-conflict democracies around the world.