Verifying Elections

Abstract:

Free & Fair is a new elections company that is bringing formal methods to US elections. In this talk we will describe the range of techniques that we apply to make end-to-end guarantees of the systems that we sell to jurisdictions across the country. In the process of our work, we have researched:

• cryptographic protocols for verifying the correctness of elections,
• formalized proofs of correctness for elections algorithms, and
• techniques for trusting commercial off the shelf hardware with critical software.

This poster addresses industrialization of formal methods. Free & Fair is a company that is breaking into an established market using formal methods to create high assurance software. Formal methods is critical in every way to our business plans. We use our confidence in our software to offer warranties that no existing vendor will be able to compete with. We are also actively working to help create federal certification requirements that can be met by evidence generated from formal methods approaches. By combining these requirements with our rigorous software engineering techniques, we will create a product that can make it through certification faster than any current elections software. This will not only help us get our products to market quickly, but it will free both us and jurisdictions to update their elections systems not just when certification allows, but as upgrades are necessary.

We have written a number of proposals and other responses to jurisdictions that wish to buy elections software. In doing so, and by working closely with elections officials, we have continuously tuned our approach to presenting our formal methods techniques to an audience that may not have heard of our approaches but that can appreciate what formal method can do for them. We will discuss what we have learned in this process.

--

Joseph Kiniry is the CEO and Chief Scientist of Free & Fair, a Galois spin-out focusing on high-assurance elections technologies and services. He is also the Research Lead at Galois of several programs: Rigorous Software Engineering, Verifiable Elections, High-assurance Cryptography, and Audits-for-Good.

Prior to joining Galois in 2014, Dr. Kiniry was a Full Professor at the Technical University of Denmark (DTU). There, he was the Head of DTU's Software Engineering section. Dr. Kiniry also held a guest appointment at the IT University of Copenhagen. Over the past decade, he has held permanent positions at four universities in Denmark, Ireland, and The Netherlands.

Dr. Kiniry has around fifteen years experience in the design, development, support, and auditing of supervised and internet/remote electronic voting systems while he was a professor at various universities in Europe. He co-led the DemTech research group at the IT University of Copenhagen and has served as an adviser to the Dutch, Irish, and Danish governments in matters relating to electronic voting. He now advises the U.S. government on these matters via his participation in the EAC-NIST VVSG public working groups.

His primary research interest is in applying formal methods to software development, especially in the areas of system correctness and security. Notable achievements include leading the network and external security evaluation team for the Dutch national internet voting system (KOA) and the Danish national single sign-on system; participating in, or leading the development of, verified voting systems for the American, Danish, Dutch, and Irish electoral systems; leading the development of the EU FP6-funded Mobius Program Verification Environment, the ESC/Java2 platform for extended static checking, and a number of other widely-used software platforms including AutoGrader, BONc, Beetlz, CLOPS, DiVS, FreeBoogie, IDebug, KOA, OBJ3, RCC, SATConfig, Simplify, Uilioch, Votail, and others.

Before starting at Galois in 2015, Joey Dodds was a Ph.D. candidate at Princeton University, working mainly on the VST project doing research around verifying C programs. At Princeton, Joey also researched a logic for conditional information flow, as a candidate method for analyzing information flow in the SPARK Ada toolkit.

During his work as a Master's student at KSU, Joey worked on Guardol, a programming language for configuring guards, a hardware solution to cross domain security. Specifically, he worked on various analyses for checking the validity of Guardol programs. Joey also contributed to the Kiasan bounded symbolic execution engine, as part of the Sireum project.