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

Keywords (11)

Related Publications (2)

Academic

Publications

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

Edit

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


	BibTex \| RIS \| RefWorks Download

, ,

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.

Journal: Electronic Notes in Theoretical Computer Science - ENTCS , vol. 183, pp. 39-55, 2007

DOI: 10.1016/j.entcs.2007.01.060

Cumulative Annual

View Publication

( www.sciencedirect.com )

( www.informatik.uni-trier.de )

( www-public.int-evry.fr )

- ...Using formal modelling and verification to ensure that an interface cannot generate invalid votes is reported in Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface[20]...
J Paul Gibson, et al. Just like paper and the 3-colour protocol: A voting interface requirem...
- ...Another pattern called re-usability pattern, has been suggested by Abrial, Cansell and Méry [2] and applied to the development of voting systems [6]...
Nazim Benaïssa, et al. Proof-Based Design of Security Protocols
- ...A secondary objective is to demonstrate the application of formal methods — as in [5,6] — in the engineering of the software in the e-voting system, which we consider to be critical[24]...
- ...As votes are transformed from one representation to another it is possible that a bug could transform a valid vote into an invalid vote[6]...
J. Paul Gibson, et al. Engineering a Distributed eVoting System Architecture: Meeting Critica...
- ...There are obvious advantages with this framework when compared with that in figure 2. Firstly, verification of the correctness of refinements — a good example is the refinement of the voter interface[22] — can be done at the generic level (facilitating re-use)...
- ...Integrating SPL techniques with formal methods is a promising approach: refinement for re-use of trustworthy components has already been addressed with respect to e-voting machine interfaces [22] and storage [29]...
- ...Current research — based on the notion of a feature interaction algebra[31] — suggests that a correct-by-construction approach to guaranteeing the functionality of evoting systems[22,29] merits further investigation...
J. Paul Gibson, et al. Feature Interactions in a Software Product Line for Evoting
- ...• The parametric/generic pattern provides a way to instantiate Event B development and we apply it on two very different case studies: the design of greedy algorithms [27] and the design of e-voting algorithms [22, 21]...
Projet RIMEL. Livrable 3 Proof-based design patterns