Invited Talks

We constantly hear about new vulnerabilities in information systems. Beyond the direct harm caused by each vulnerability and exploit, the constant stream of exposed flaws, which range from small programming bugs to large-scale design errors, undermine our general trust in information systems. This lack of trust, in turn, undermines our ability to fully realize the potential societal benefits that information systems carry --- in particular their ability to preserve the privacy of sensitive data, while allowing controlled use of this data along with accountability for such use.

This talk will argue that this unfortunate state of affairs is far from being inherent, and that if we combine technology and thinking from a number of communities, most prominently Programming Languages, Cryptography, and System design, it will indeed be possible to build large scale information systems that truly satisfy even intricate security and functionality requirements.

We will survey some of the work done in this direction and will outline a potential road ahead. Key tools include: (a) developing techniques for using PL methodology and techniques to specify and assert higher-level security properties of multi-component systems, and (b) enabling security-preserving modular design and analysis of complex systems from simple building blocks. Key application areas will also be discussed.

Electronic voting is now used in many countries and in many elections, from small elections such as parents representatives in schools, to politically binding elections. Electronic voting facilitates counting and enables a wide variety of elections, such as preferential voting where voters rank their candidates by order of preference. In such a case, counting the votes by hand can be a very complex task that can, in contrast, easily be handled by a computer. Another advantage of electronic voting is that voters may vote from anywhere and it can last several weeks if needed. It is often used at least as a replacement of postal voting.

However, electronic voting also comes with security threats and has been subject to severe attacks. For example, the Washington, D.C., Internet voting system has been attacked (Wolchok et al., 2012), during a trial just before the election. Recently, Switzerland has stopped temporarily using electronic voting after a public penetration test that has revealed severe weaknesses (Lewis et al., 2019).

Ideally, electronic voting should offer the same guarantees that traditional paper-based election. In particular, it should guarantee vote privacy (no one should know how I voted) and verifiability: anyone should be able to check that the votes are accurately counted and correspond to the voters intent.

In this talk, we will present the Belenios voting protocol (Cortier et al., 2019) that has been used in more than 500 elections in 2020, through its voting platform. We will discuss its security properties as well as its limitations.

As for security protocols in general, the design of electronic voting systems is error-prone and it is hard to assess whether a protocol ensures the required security properties. For these reasons, a common good practice is to design a protocol together with a formal security analysis, as it has been done in the context of TLS1.3 (Delignat-Lavaud et al., 2017) for example. The Swiss Chancellerie requires both computational and formal proofs of security before the deployment of an electronic voting system. We will explain how the tools developed for the automated analysis of security protocols, like ProVerif (Blanchet et al., 2013), can help gaining a better confidence in e-voting protocols. One particular issue in the context of voting is that the formalization of security properties is still an on-going work, even for crucial properties like vote secrecy (Bernhard et al., 2015). Hence electronic voting still raises many challenges for our research community.

A key measure to mitigate and slow down virical disease is contact tracing. Contact tracers traditionally relies on time-consuming activities performed by human contact tracers: interview positive patients to identify potential infected contacts, and communicate with those contacts to ensure they take precautions (e.g., self-isolate or take a test). As the number of cases increases, human contact tracers cannot timely perform their activities, decreasing their effectiveness at breaking transmission chains and hence at slowing down the virus spread. This situation prompted institutions and governments to seek help from technology to be able to scale mitigation measures.

During 2020 we have witnessed the appearance of a number of Digital Proximity Tracing proposals which have three main goals: notifying contacts in a timely manner, notifying close contacts that may not be identified by manual contact tracing, and operating even when manual contact tracers cannot scale to the number of positive cases. These proposals typically rely on smartphones to gather proximity information that serves to identify contacts.

In this talk we will present the Decentralized Privacy-Preserving Proximity Tracing protocol (DP3T) (Troncoso et al., 2020), that inspired Google and Apple's Exposure Notification and is now the basis of dozens of proximity tracing mobile apps around the world. We will discuss the requirements and constraints that drove the protocol design, and the security and privacy trade-offs that we had to confront.

The protocol, however, is only a small part of a Digital Proximity tracing system which includes communication with the server and integration with health services. This talk will also summarize our experience designing and implementing these mechanisms under time pressure and continuous changes in the underlying libraries.