Skip to Main content Skip to Navigation
New interface
Journal articles

Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface

Dominique Cansell 1 Paul Gibson 2 Dominique Méry 1 
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Electronic voting machines have complex requirements. These machines should be developed following best practice with regards to the engineering of critical systems. The correctness and security of these systems is critical because an insecure system could be open to attack, potentially leading to an election returning an incorrect result or an election not being able to return any result. In the worst case scenario an incorrect result is returned -- perhaps due to malicious intent -- and this is not detected. We demonstrate that an incorrect interface is a major security threat and show the use of the formal method B in guaranteeing simple safety properties of the voting interface of a voting machine implementing a common variation of the single transferable vote (STV) election process. The interface properties we examine are concerned with the collection of only valid votes. Using the B-method, we apply an incremental refinement approach to verifying a sequence of designs of the interface for the collection and storage of votes, which we prove to be correct with respect to the simple requirement that only valid votes can be collected.
Document type :
Journal articles
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Saturday, May 21, 2011 - 6:03:36 PM
Last modification on : Friday, February 4, 2022 - 3:08:50 AM

Links full text




Dominique Cansell, Paul Gibson, Dominique Méry. Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface. Electronic Notes in Theoretical Computer Science, 2008, 183, pp.39-55. ⟨10.1016/j.entcs.2007.01.060⟩. ⟨inria-00594892⟩



Record views