Search
Close this search box.

DIREC project

Trust through software independence and program verification

Summary

There is constant interest for Internet Voting by election commissions around the world. This is illustrated well by Greenland – their election law was changed in 2020 and now permits the use of Internet Voting. However, building an Internet Voting system is not easy: The design of new cryptographic protocols is error-prone and public trust in the elected body is easily threatened. 

A software-independent voting protocol is one where an undetected change or error in software cannot cause an undetectable change or error in an election outcome. Program verification techniques have come a long way and promise to improve the reliability and the cybersecurity of election technologies but it is, by no means, clear if formally-verified software-independent voting systems also increase public confidence in elections.

Together with the authorities in Greenland, this project will investigate the effects of program verification on public trust in election technologies. The project aims to contribute to making internet elections more credible, which can strengthen developing and post-conflict democracies around the world.

Project period: 2023-2026
Budget: DKK 4,6 million

Project Manager

  • Professor Carsten Schürmann
  • Department of Computer Science, ITU
  • carsten@itu.dk

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.

Impact

The project creates value by enhancing the credibility of Internet voting systems, thereby strengthening developing and post-conflict democracies worldwide, especially in the context of nations reevaluating their electoral processes amidst challenges such as the Covid-19 pandemic. 

Insights

Partners