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

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.