- Wolfgang Thomas, RWTH Aachen University
“Synthesis and Some of Its Challenges”
- David Dill, Stanford University
“Model Checking Cell Biology”
- Alex Haldermann, University of Michigan
"Verifiably Insecure: Perils and Prospects of Electronic Voting"
The advent of a methodology of automatic synthesis (of state-based systems) adds a number of interesting facets to the setting of model-checking. In this talk we focus on some conceptual aspects arising from the basic scenario of strategy synthesis in infinite-duration two-player games, as a natural extension of model-checking. The starting point is the simple observation that model-checking asks about the (non-) emptiness of sets while synthesis asks for a certain kind of uniformization of relations by functions. This raises a large number of questions on the classification of (word-) functions (which serve as strategies in games). We discuss basic results and recent progress, emphasizing two aspects: the definability of strategies and their ”complexity” in various dimensions. These results are as yet preliminary, and we end by listing unresolved problems, for example on the logic-representation of strategies.
Mathematical models of real biological systems have predominantly been deterministic or stochastic continuous models. However, there are reasons to believe that at least some processes can be modeled in a “digital" way. Once we do that, we enter the domain of concurrent and reactive systems, where model checking has been an important tool. Perhaps techniques from the verification community could lead to insights about the systems principles that allow biological systems using very low energy (and high noise) components to function dynamic environments. I will explore some past and future research directions in this area, as well as some of the non-computational challenges that arise in this kind of research.
Electronic voting presents deep security challenges due to the simultaneous requirements of ensuring correct election outcomes and preserving the secret ballot. These difficulties are compounded by the political realities and logistical constraints of conducting national elections, which inevitably lead to technical compromises. Over the past eight years, I have worked to illuminate the contours of this problem through studies of e-voting systems used in the U.S. and abroad. These (often uninvited) security evaluations culminated in the production of "proofs of incorrectness" that established the feasibility of attacks, including the first voting machine virus and the first malicious election hardware, and they have helped catalyze policy reforms affecting the voting technology used by almost a billion people.
In this talk, I will discuss how practical obstacles exposed in my empirical work suggest limitations to what formal verification of the correctness of voting systems can achieve. At the same time, practice presents opportunities for technology---designed correctly and applied intelligently---to make elections more secure and efficient than ever. Along the way, I’ll share adventures from my work at the intersection of technology and political power. We will travel from Manhattan alleyways to Mumbai jail cells to the august halls of Washington, D.C., be accused of being a "foreign conspiracy" to destabilize a major democracy, and narrowly escape deportation.