PhD%20Project%20Topics

= PhD Project Topics = Here you can see a rough description of potential PhD topics that you can apply for. The PhD projects will be conducted in collaboration with the ETH Zurich, and the University of Luxembourg. Be prepared to spend some time in either of the two places if you are admitted in ITU's PhD programme. The topics are kind of general. If you apply to one of our calls, please make your interests more precise in your research statement.

== Epistemic Logical Frameworks == Building on methods developed within the area of proof carrying code, we propose to investigate a novel idea of trace-emitting computation that forces a computing machine to create a certificate that will be used to hold the machine accountable for its actions and therefore the results it computes. The idea works as follows: while the electronic voting machine is running, it constructs a certificate by recording every step it took. Here, a step refers to a well-specified and se- mantically well-understood elementary operation in an election specific programming language that may include justifications for security and access conditions. These justifications should be thought of as propositions derived in an election specific authorization logic that we will developed within this proposed project. As the following example shows, the logic is likely to include epistemic modalities that correspond to principal p knows A (written as [p]A), principal p has A (written as [p]A) and prin- cipal p says A (written as ⟨p⟩A). The following three sample rules are expressed in the hypothetical epistemic logical framework that we propose to develop within this project. They illustrate the flavor of how specify operations of the electronic voting machine. va represents the voting authority.

'''Vote Casting'''

[K]⟨K⟩vote-for L ⊗ ⟨va⟩is-registered K ⊗ [va]voting ⊗ !⟨va⟩is candidate L -o {[va]vote L ⊗ [va]voting}

'''Election Closing'''

[K]⟨K⟩close ⊗ ⟨va⟩may-close K ⊗ [va]voting -o {[va]close}

'''Counting'''

[K] count L N ⊗ [va]may-count K ⊗ [va]close ⊗ [va]vote L -o {[va]close ⊗ [K]count L (N + 1)}

The proposition “[K]⟨K⟩vote-for L” in the Vote Casting rule refers to the fact that K knows that he or she wants vote for L. If the voting authority has the (one time) consumable information that K is a registered voter, some evidence that the election is on, and is sure that L is really a candidate, then (formally expressed by the connective -o) a vote was cast for L, and the election is still on. The Election Closing rule lets K close the election by consuming the [va]voting token, and finally the Counting illustrates how to tally the (now anonymized) votes for candidate L.

Combining the ideas from the areas of proof carrying authorization and logical frameworks we then plan to use our concurrent logical framework Celf developed in Schu ̈rmann’s group at the IT University of Copenhagen, to design, experiment, deploy and test an election specific programming language and authorization logic. During an electronic elec- tion, the certificate is then chopped into fragments and given to each voter as a piece of physical evidence representing the part of the computation trace that pertains to counting the vote. As in a conventional election, the evidence is then cast into a ballot box. Once the election has closed, we reconstruct the certificate from all of the fragments, and validate it using the small trusted implemen- tation of Celf’s type checker (which can be written in the aforementioned thousand lines of code). This way we detect attacks that alter the outcome of an election, for example by spyware or malware tampering with counters. The semantic meaning of a single ballot, sometimes referred to as a “frog”, is logically uniquely determined.

== Homomorphic Encryption == Besides outcome-altering attacks from within a voting machine, there are also attacks that threaten the secrecy of the vote. Attacks of this kind may happen at the interface between the physical machine, the machine that may be located in a polling station and the abstract machine, running on the physical machine, whose steps need to be recorded. For example, the physical machine has access to the memory of the abstract machine and may enable viruses or spyware to listen in on the voting process, for example on internal counters but also the certificates that may contain sensitive information. The challenge of this research focus is to secure the abstract machine by preventing the host machine from accessing sensitive data.

Certificates are built incrementally during the course of an election day. Let us assume that starting from an initial certificate C0 the voting machine terminates returning certificate Cn.

C0 −→ C1 −→...−→ Cn−1 −→ Cn

We propose to apply homomorphic encryption and allow the electronic election to work with encrypted certificates only. Let pk be a public key. We write ci for the ciphertext that corresponds to certificate Ci encrypted by pk. Gentry’s PhD thesis work guarantees that we can construct new certificates without decrypting the old ones (as indicated by ⇒). c0 ⇒ c1 ⇒... ⇒ cn−1 ⇒ cn

== Trust-by-design == In a conventional elections, we trust all parts of the process, from voter registrations to the announcement of the official final result. In this research focus, we study therefore the role of the voter’s trust as part of the entire conventional process, and distill a list of critical elements of why people trust and what makes the process trustworthy. Based on the results from Research Focus 4 below, we are certain that we are able to locate the majority of critical elements within, for example, voter registration, distribution of registry data to polling stations, communication of partial results to municipalities, aggregation of vote counts at the municipalities or the interior ministry, and finally even how to map of vote totals to seat distribution. We propose to proceed as follows.

We develop a software engineering principle that we refer to as trust by design. The principle will consist of one part toolbox full of data structures and algorithms and another part best practice recommendations on how to work with critical elements. We expect software and hardware designers to follow this principle, in a way that they use the tools to mirror the critical elements in form of technology that users can see, touch, validate, and most importantly trust. We are certain that together with the data structures, algorithms, and other techniques developed in this research project, we can provide a complete set of tools to implement electronic election software. We will gain first-hand experience with the principle during the development of our prototype voting machine.

Time permitting, we propose to broaden the context of electronic elections to the internet. Crucial for this endeavor is that we are able to recreate the critical elements in a distributed setting while keeping the trusted base of computing small. If this is possible is an open question. In the distributed setting we are faced with cross-cutting challenges concerning privacy, security, and availability, prompting us to refine the election specific programming language and authorization logic for voting systems.

== Ethnographic Studies == The social, political and cultural impacts and effects in implementing the trust by design idea. The trust by design idea implicates a redistribution of social and technical agencies and competencies in the election process. In particular, the highly complex nature of trust in democratic elections constituted by various legal regulations and well-established informal practices must be addressed . This raises questions of the legitimacy and transparency of the election. Those issues are often addressed from a cognitive and psychological perspective with their emphasis on the rationality of the technology on the one hand and the cognitive and emotional faculties of the individual on the other. Our perspective differs radically from this.

Based on a social science approach informed by STS we will examine the election process and the development and application of the new technology in a multi-spectered view. Our approach is unique in focusing on the organizational practices, control mechanisms and agencies as well as the accountabilities involved in performing trust by design.

First, by doing ethnographies of election processes, including both conventional practices and pilot projects in the next upcoming elections in Frederiksberg and Aarhus municipalities.

Second, we will explore issues of trust, election technologies and democracy from a historical and comparative perspective in order to better understand the role of tradition and familiarity and how specific technologies, legality and legitimacy are accounted for in various situations. The findings will serve as an analytical framework for examining impacts on trust when introducing new technology in the election process.

Third, we will focus on trust by design as a voting technology in the making: How do the computer scientists inscribe specific values of trust and ideas about democracy and society into the technology. All three investigations, and especially the third, aim at making trust by design and its implications as transparent as possible. Particularly the third focus is distinct in addressing the scientific practices in addition to the practices that take place within the local authorities.