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.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 183, pp.39-55. 〈10.1016/j.entcs.2007.01.060〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00594892
Contributeur : Dominique Méry <>
Soumis le : samedi 21 mai 2011 - 18:03:36
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Lien texte intégral

Identifiants

Collections

Citation

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, Elsevier, 2008, 183, pp.39-55. 〈10.1016/j.entcs.2007.01.060〉. 〈inria-00594892〉

Partager

Métriques

Consultations de la notice

204