On Voting Machine Design for Verification and Testability

Cynthia Sturton, Susmit Jha, Sanjit A. Seshia, and David Wagner. On Voting Machine Design for Verification and Testability. In Proceedings of the ACM Conference on Computer and Communications Security (CCS), pp. 463–476, November 2009.

Download

[pdf] 

Abstract

We present an approach for the design and analysis of an electronicvoting machine based on a novel combination of formal verificationand systematic testing. The system was designed specificallyto enable verification and testing. In our architecture, the votingmachine is a finite-state transducer that implements the bare essentialsrequired for an election. We formally specify how eachcomponent of the machine is intended to work and formally verifythat a Verilog implementation of our design meets this specification.However, it is more challenging to verify that the compositionof these components will behave as a voter would expect, becauseformalizing human expectations is difficult. We show how systematictesting can be used to address this issue, and in particular toverify that the machine will behave correctly on election day.

BibTeX

@InProceedings{sturton-ccs09,
  author = 	 {Cynthia Sturton and Susmit Jha and Sanjit A. Seshia and David Wagner},
  title = 	 {On Voting Machine Design for Verification and Testability},
  booktitle = 	 {Proceedings of the ACM Conference on Computer and Communications Security (CCS)},
  month = nov,
  year = 	 {2009},
  pages = "463--476",
  abstract = {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.
  },
}