TRUST Security Seminar Series: On Voting Machine Design for Verification and Testability

Seminar | November 19 | 1-2 p.m. | Soda Hall, Wozniak Lounge

Speaker/Performer: Cynthia Sturton, University of California, Berkeley

Sponsor: Team for Research in Ubiquitous Secure Technology

We present an approach for the design and analysis of an electronic voting machine based on a novel combination of formal verification and systematic testing. The system was designed specifically to enable verification and testing. In our architecture, the voting machine is a finite-state transducer that implements the bare essentials required for an election. We formally specify how each component of the machine is intended to work and formally verify that a Verilog implementation of our design meets this specification. However, it is more challenging to verify that the composition of these components will behave as a voter would expect, because formalizing human expectations is difficult. We show how systematic testing can be used to address this issue, and in particular to verify that the machine will behave correctly on election day. This presentation is based on joint work with Susmit Jha, Sanjit A. Seshia, and David Wagner

Event Contact: 510-643-5105