Dominique Cansell
email: cansell@loria.fr

J Paul Gibson

Dominique Méry
email: mery@loria.fr

Formal verification of tamper-evident storage for e-voting

The storage of votes is a critical component of any voting system. In traditional systems there is a high level of transparency in the mechanisms used to store votes, and thus a reasonable degree of trustworthiness in the security of the votes in storage. This degree of transparency is much more difficult to attain in electronic voting systems, and so the specific mechanisms put in place to ensure the security of stored votes require much stronger verification in order for them to be trusted by the public. There are many desirable properties that one could reasonably expect a vote store to exhibit. From the point of view of security, we argue that tamper-evident storage is one of the most important requirements: the changing, or deletion of already validated and stored votes should be detectable; as should the addition of unauthorised votes after the election is concluded. We propose the application of formal methods (in this paper, event-B) for guaranteeing, through construction, the correctness of a vote store with respect to the requirement for tamperevident storage. We illustrate the utility of our refinementbased approach by verifying -through the application of a reusable formal design pattern -a store design that uses a specific PROM technology and applies a specific encoding mechanism.

Introduction

Motivation: the e-voting problem

Computer technology has the potential to modernise the voting process and to improve upon existing systems; but it also introduces new concerns with respect to secrecy, accuracy, trust and security [START_REF] Gritzalis | Secure Electronic Voting[END_REF]. The debate over e-voting is not a new one -recent use of such systems in actual elections has led to their analysis from a number of different viewpoints: usability [START_REF] Herrnson | Early appraisals of electronic voting[END_REF], trustworthiness and safety criticality [START_REF] Mcgaley | E-Voting: A Safety Critical System[END_REF], transparency and openness [START_REF] Mcgaley | Transparency and e-Voting: Democratic vs. Commercial Interests[END_REF], and risks and threats [START_REF] Neumann | Inside risks: risks in computerized elections[END_REF].

The potential advantages are generally accepted, for example: faster result tabulation, elimination of human error which occurs in manual vote tabulation, assistance to voters with "special" needs, defence against fraudulent practices (e.g. with postal votes [START_REF] Brown | Who is enfranchised by remote voting?[END_REF]), and improving the "fairness" of count systems that incorporate "unfair" non-deterministic procedures [START_REF] Tideman | Better voting methods through technology: The refinement-manageability trade-off in the single transferable vote[END_REF].

Despite ever-increasing uncertainty over the trustworthiness of these systems -which is one of the major disadvantage associated with them -many countries (particularly in Europe [START_REF] Svensson | E-voting in europe: Divergent democratic practice[END_REF]) have recently chosen to adopt e-voting. The main risks that have been clearly identified seem not to concern those responsible for procuring the systems. In fact, it appears that e-voting is just one, well-publicised, example of governments wishing to adopt new technologies [START_REF] Scherlis | IT research, innovation, and e-government[END_REF] before the risks and benefits, as perceived by the public [START_REF] Horst | Perceived usefulness, personal experiences, risk perception and trust as determinants of adoption of e-government services in The Netherlands[END_REF], have been properly analysed and debated.

This paper contributes to answering two important questions: firstly, whether the public's mistrust in the security of e-voting systems is well-founded; and secondly, whether formal methods have a role to play in addressing the problem of mistrust. With respect to the first aspect, Kocher and Schneier [START_REF] Kocher | Insider risks in elections[END_REF] state: "The threats are real, making openness and verifiability critical to election security." As to the second aspect, expecting the public to trust the adoption of such new technology is only possible if they can be convinced that it rests on firm trustworthy foundations. The formal methods community have an important role to play in this respect: the use of formal notations provides a fundamental foundation upon which the complexities of everchanging technologies can be managed [START_REF] Ghezzi | Fundamentals of software engineering[END_REF]. We argue that without the adoption and promotion of formal methods as the foundations of software engineering, developing trustworthy e-voting systems will not necessarily guarantee that they will be trusted.

This paper proposes that, in general, already existing formal techniques can help to alleviate many of the verification problems that the adoption of new e-voting technologies can introduce. For the specific modelling and verification in our study we use the event-B method [START_REF] Méry | B # : Toward a synthesis between Z and B[END_REF], based on the B notation. We argue that it is unreasonable to expect the public to trust a system (or part of a system) to behave correctly just because it is developed using a formal method (like event-B) 1 . Instead, we propose that we must first establish a set of quality standards for reliable, re-usable, trustworthy tools and techniques that have proven themselves in the formal development of correct systems. Then, provided the public are properly informed, it is not unreasonable to expect systems built in this way to be both more trustworthy and more trusted. The correct-by-construction approach in this paper illustrates the type of standard process to which we are alluding.

Formal methods and vote storage

Public opinion, arising from detailed debate of the issues, would suggest that for e-voting machines to be acceptable they should be developed following best practice with regards to the engineering of critical systems. Media reports would also suggest that the secure storage of votes is one of the issues that is most mistrusted by the public.

We propose the use of formal methods as a means of ensuring that a machine securely stores votes, and we propose to demonstrate the utility of formal methods through guaranteeing simple safety properties of a voting machine store. The main property that we examine is concerned with the need for tamper-evident storage, which addresses the risk of unauthorised tampering of vote data after it has been correctly registered and stored. In Analysis of an electronic voting system [START_REF] Kohno | Analysis of an electronic voting system[END_REF], we see that such a security weakness already exists in one of the most widely procured voting systems: ". . . an adversary could alter election results by modifying ballot definition files, and . . . it leaves no evidence that an attack was ever mounted" Here, the "adversary" is most likely to be a single insider (election official) with access to the storage device. We argue that it is the responsibility of the storage designers to guarantee the security of the votes stored without having to make an assumption about the behaviour or intent of such officials.

In order to illustrate how a guarantee could be made, we use event-B and apply an incremental refinement approach to verifying a sequence of designs for the storage of votes, which we prove to be correct-through-construction with respect to the simple requirement that the vote storage is tamper-evident.

Refinement and genericity: a formal design pattern

>From a technological viewpoint we know that system design has an important role in security assurance. Mercuri [START_REF] Mercuri | Computer security: quality rather than quantity[END_REF] addresses the theme of quality in the process of engineering security: "By encouraging artistry and applying craftsmanship to our security problems, viable solutions will emerge." This supports our view that one must start with a simple model of the vote store requirements and refine that model, during design, towards a correct implementation. For this reason we chose a simple security requirement -that only valid votes can be found in the vote store and that these cannot be tampered with without detection -and start our formal development from there. The use of formal methods to guarantee that only valid votes are passed from the machine interface to the store has already been presented [START_REF] Cansell | Refinement: a constructive approach to formal software design for a secure e-voting interface[END_REF]. The work presented in this paper, which addresses the tamperevident requirement, is complementary in nature: event-B is the common modelling language, and correctness through construction is the common formal design approach.

As one of the long-term goals of the formal methods community is to simplify the verification process for engineers [START_REF] Caldwell | Formal methods technology-transfer: a view from NASA[END_REF][START_REF] Gibson | Formal requirements engineering: Learning from the students[END_REF], we support the view that re-usable verification design patterns, similar in nature to the work by Mehlitz and Penix [START_REF] Mehlitz | Design for verification -using design patterns to build reliable systems[END_REF], as a potential solution to this problem. This paper identifies a good candidate for such a reusable pattern, combining genericity and refinement to provide a correct-by-construction pattern (see Section 4).

Manchester Encoding: formalising the design of a secure vote PROM

The main design that is modelled and verified in this paper is taken directly from the work by Molnar, Kohno, Sastry and Wagner [START_REF] Molnar | Tamperevident, history-independent, subliminal-free data structures on PROM storage -or-how to store ballots on a voting machine[END_REF]. Their proposed solution to providing tamper-evident storage involves the application of Manchester codes [START_REF] Stallings | Data and computer communications[END_REF] and a write-once data PROM store. The encoding simply represents a 0 as a 01 and a 1 as a 10. Thus, when validating votes stored as pairs of bits there are 2 additional pair cases to be considered, where (because our memory allows only 1s to be overwritten as 0s): 11 corresponds to unwritten memory and 00 corresponds to an invalid memory that has been tampered with.

Before we formally specify and verify the proposed solution, we briefly note that there is a real pragmatic need for tamper-evident rather than tamper-proof writeable storage. The tamper-proof requirement can be met only by some security mechanism ensuring authorised-only update of the vote store. This security mechanism would probably be implemented as some combination of physical constraints, together with hardware and software checks. It would most likely involve some complex encryption technique and it is not clear whether one could, or should, expect voters to trust such a complex system. Contrastingly, guaranteeing the tamper-evident requirement is a much simpler problem that -if done well -could be both trustworthy and trusted.

Implementing storage using a write-once data store has many obvious advantages when we consider tampering: obviously, any vote that has already been written cannot be overwritten? In fact, without a more formal model of the store, this is not guaranteed to be true. For example, one form of write-once storage could allow the flipping of an initial bit state to be done once and once only. This does not necessarily guarantee that a recorded vote cannot be overwritten as individual bits of a vote will not have been flipped when a vote is recorded. In fact, as with all storage mechanisms, the (encoding) protocol used for writing information to such a store will be the deciding factor in whether the tampering requirements are met. Furthermore, there are many reasonable variations of the tampering requirement. Without a precise statement, it is not clear whether we will be able to verify whether a given system (the store properties, together with the encoding protocol) is correct.

The key property of the encoding that we shall model is that if any (sub)set of 1 bits in a stored codeword are flipped to 0s then the result is no longer a valid code word. We then wish to establish that anyone with read access to the voting store can detect an invalid memory state, where at least one codeword is invalid, and consequently any tampering after2 the election has been completed. The verification of this safety property requires modelling of the write-once behaviour in the chosen PROM implementation (checking that 1s can be re-written as 0s but that 0s cannot be changed) in conjunction with the encoding mechanism. It also requires the use of a special election over bit (bit pair in PROM) to signify that the election is over, and which must be unset and untampered with for new votes to be recorded (otherwise anyone with access to the voting machine could add unauthorised votes after the election, an attack known as ballot stuffing). We chose not to include the election-over behaviour in the model presented in this paper.

We note that this system is not tamper proof: attackers with write access to the vote store can still invalidate the election by overwriting vote data. However, this attacks would be easily identified by procedures for validating the storage state during and after the vote.

The main advantages of doing this design formally, in event-B, are development oriented:

• an abstract model can be easily validated as correctly expressing the requirement,

• the actual design model can be constructed incrementally through refinement of the abstraction,

• the refinement process can continue through to modelling at very fine grain levels of detail that correspond to the chosen low-level implementation architecture,

• we can more easily reason about different variations and combinations of encodings and storage media, and

• we can analyse possible problems of integrating this requirement with other requirements of the e-voting system, in general, and the vote storage, in particular.

Thus, we are more likely to develop a trustworthy storage.

A secondary benefit arises when we consider the issue of how to build public trust in our formally developed trustworthy system. We argue that the correct-by-construction technique, embodied in a reusable design pattern, will become more and more trusted as it is used to develop more and more systems that prove themselves to be trustworthy. As a consequence, using such a standard technique (and associated tools) in constructing critical systems will increase confidence in the systems' correctness, from both the developers and the public users.

With tool support for automatically checking our verification proof we have another advantage: if our proof tool is trustworthy then the design is sure to be correct provided the property that we have established, in the initial abstract model, is an accurate statement of the high level requirement. To make this transparent to the users (voters) it is essential that an initial abstract model is easy to understand and validate, and that they have good reason not to mistrust our proof tool and techniques. Our design approach facilitates this type of openness and transparency.

Overview of event-B development by stepwise refinement

Event-based modelling

Our event-driven approach [START_REF] Méry | B # : Toward a synthesis between Z and B[END_REF] is based on the B notation. It extends the methodological scope of basic concepts in or-der to take into account the idea of formal models. Roughly speaking, a formal model is characterized by a (finite) list x of state variables possibly modified by a (finite) list of events; an invariant I(x) states properties that must always be satisfied by the variables x and maintained by the activation of the events. In the following, we briefly recall definitions and principles of formal models and explain how they can be managed by tools [START_REF] Abrial | Click'n'prove: Interactive proofs within set theory[END_REF][START_REF] Clearsy | Aix-en-Provence[END_REF].

Generalized substitutions are borrowed from the B notation. They provide a means to express changes to state variable values. In its simple form, x := E(x), a generalized substitution looks like an assignment statement. In this construct, x denotes a vector built on the set of state variables of the model, and E(x) a vector of expressions. The interpretation we shall give here to this statement is not however that of an assignment statement. We interpret it as a logical simultaneous substitution of each variable of the vector x by the corresponding expression of the vector E(x). There exists a more general normal form of this, denoted by the construct x : P (x 0 , x). This should be read: "x is modified in such a way that the predicate P (x 0 , x) holds", where x denotes the new value of the vector and x 0 denotes its old value. This is clearly non-deterministic in general.

In the following, the so-called before-after predicate BA(x, x ′ ) describes an event as a logical predicate expressing the relationship linking the values of the state variables just before (x) and just after (x ′ ) the "execution" of event evt 3 . Each event has two main parts: a guard, which is a predicate built on the state variables, and an action, which is a generalized substitution.

Proof obligations are produced from events in order to state that an invariant condition I(x) is preserved. Their general form follows immediately from the definition of the before-after predicate, BA(x, x ′ ), of each event:

I(x) ∧ BA(x, x ′ ) ⇒ I(x ′ )
Note that it follows from the two guarded forms of the events that this obligation is trivially discharged when the guard of the event is false.

Model Refinement

The refinement of a formal model allows us to enrich a model in a step-by-step approach, and is the foundation of our correct-by-construction approach. Refinement provides a way to strengthen invariants and to add details to a model. It is also used to transform an abstract model into a more concrete version by modifying the state description. This is done by extending the list of state variables, by refining each abstract event into a corresponding concrete version, and by adding new events. The abstract state variables, x, and the concrete ones, y, are linked together by means of a, so-called, gluing invariant J(x, y). A number of proof obligations ensure that (1) each abstract event is correctly refined by its corresponding concrete version, (2) each new event refines skip, (3) no new event takes control for ever, and (4) relative deadlock-freeness is preserved. Details of the formulation of these proofs follows.

We suppose that an abstract model AM with variables x and invariant I(x) is refined by a concrete model CM with variables y and gluing invariant J(x, y). If BAA(x, x ′ ) and BAC(y, y ′ ) are respectively the abstract and concrete before-after predicates of the same event, we have to prove the following statement, corresponding to proof obligation (1):

I(x) ∧ J(x, y) ∧ BAC(y, y ′ ) ⇒ ∃x ′ • (BAA(x, x ′ ) ∧ J(x ′ , y ′ ))
Now, proof obligation (2) states that BA(y, y ′ ) must refine skip (x ′ = x), generating the following simple statement to prove (2):

I(x) ∧ J(x, y) ∧ BA(y, y ′ ) ⇒ J(x, y ′ )
For the third proof obligation, we formalise the notion of the system advancing in its execution; a standard technique is to introduce a variant V (y) that is decreased by each new event (to guarantee that an abstract step may occur). This leads to the following statement to prove (3):

I(x) ∧ J(x, y) ∧ BA(y, y ′ ) ⇒ V (y ′ ) < V (y)
Finally, to prove that the concrete model does not introduce additional deadlocks, we give formalisms for reasoning about the event guards in the concrete and abstract models: grds(AM ) represents the disjunction of the guards of the events of the abstract model, and grds(CM ) represents the disjunction of the guards of the events of the concrete model. Relative deadlock freeness is now easily formalised as the following proof obligation (4):

I(x) ∧ J(x, y) ∧ grds(AM ) ⇒ grds(CM )
To review, refinement guarantees that the set of traces of the refined model contains (modulo stuttering) the traces of the resulting model.

Genericity and refinement in event-B: a formal design pattern

The event-B method provides a framework for developing generic models of systems, where a problem can be defined using parameters to be instantiated. Intuitively, this means that we are able to relate the current problem to be solved to an abstract problem solved by an already existing generic B development (theory). Following our approcah, in the existing generic solution we must find the mathematical framework that is common to both problems, together with some constants which need to be instantiated. Consequently, in formulating the solution to the new problem the main work is to check that the instantiated parameters satisfy the constraints of the generic problem theory.

Projects

The development of a fully formal generic modelling mechanism for the B event-based method is work in progress. In the following, we indicate how the current framework can be used for implementing the instantiation.

The key concept is that of a validated project: a collection of models, either machine or refinement or implementation, which are completely verified through type checking and theorem proving. For simplicity, and without loss of generality, we assume that there is only one machine in the current project, allowing us to focus on the re-usability of developed models. Hence, a project G is roughly speaking an acyclic directed graph of models related by the refinement relationship: G = ({G, ..., G n }, -→).

The General Model

In the following, in order to avoid confusion among names, we use different fonts for designating problems, models and projects. The creation and the development of the project G follows the event B methodology. We assume that G is an existing project corresponding to a given generic problem, denoted G. The model G (see the template specification on the left of figure 1) is, in fact, the formal statement of the generic problem: it incorporates relevant aspects of the generic problem -at a high level of abstraction -in an initial model. This initial abstraction can be thought of as defining the scope of the problem and the behavioural properties that require validation.

The model G provides a general framework for the current problem; the problem is characterized by a theory defined by the clauses SETS, CONSTANTS and PROPERTIES. The unique event helps in solving the problem by defining the problem in an abstract form: saying what is required rather than how the solution is to be implemented. Intuitively this corresponds to the problem being viewed as pre/post-condition relation between an initial state and a final state which is arrived at after executing the single event. Of course, refinement permits us to move from this "magical" one-step functional view of the required system's behaviour to a richer multi-step view. The generic model G is the starting point of the development of the project G: it solves the problem G; and the project is formally checked by the theorem prover. Constants in G can be instantiated, but proof obligations must be established to ensure the validity of properties in the instantiated model, which correspond to theorems in an instantiation.

Before we introduce the instantiation and refinement steps in our design pattern, we motivate the need for such a pattern. In the general correct-by-construction refinementbased development process, working with concrete models often leads to refinements generating large numbers of proof obligations that cannot be discharged automatically. The main goal during development is to find a good refinement path: a short sequence of refinement steps where a small number of proof obligations are generated at each step and which are discharged automatically. Finding such a path usually requires reformulating or restructuring of invariants, together with changes to the degree of detail (abstraction) in the models, and is very challenging for nonexperts. Thus, we would like to package such expertise in a re-usable construct, which we call a formal design pattern.

In order to manage the complexity of the refinement path, one common approach (used by experts) is to find a more generic representation of their initial problem where details are hidden by constants requiring instantiation. Then, in general, the refinement path is much simpler to establish as it requires fewer interactive proofs and leads to a correct concrete generic solution. To prove that this generic solution can be re-used, through instantiation, to solve the initial concrete problem, two final steps are required. First, one must show that the initial problem model is a correct instantiation of the generic problem model; and secondly, one must show that the final solution model is a correct instantiation of the generic solution model.

In the best case, the generic refinement path has already been established and can be re-used directly. In the worst case, this path has to be developed from scratch. However, even in this worst case, developing the path at a higher level of abstraction (and proving 2 instantiations to be correct) is much easier 4 than developing the path at the lower level of abstraction.

Thus, our formal design pattern is a re-usable solution to a common design problem that can be exploited by formal developers who are not necessarily expert. This re-use requires only that the developers understand instantiation and refinement.

Instantiation

Consider a specific problem H in project H, say. We specify the specific requirements as a new model H (see the template specification on the right of figure 1). In order to exploit our design pattern, we wish to establish that an instantiation of the generic project G corresponds to the given problem H;

The instantiation of the generic project G for the generic problem G to solve the specific problem H consists of exhibiting a set term σ(t, d), defined in terms of the set t and constant of d, and also a similar constant term γ(t, d) for instantiating the constant c of G. Thus, the instantiation consists of repainting G with σ(t, d) and γ(t, d) and to invoke it as G (σ(t, d), γ(t, d)). We must also rename each variable (resp. event) of G by a unique variable (resp. event) of H5 . This instantiation must resolve the specific problem H and we propose to instantiate a development path through the refinement of H.

Proof Obligation of an Instantiation

Now, proof obligations of any subsequent refinement assume that the instantiated development solves the specific problem H. The next refinement step captures the semantics of how the specific problem H is solved in the same way as the problem G, after a suitable instantiation. When the instantiation is proved to be correct, we freely obtain a complete instantiated development for the new problem H.

An instantiation requires one only to prove that the properties of the system G are theorems with respect to the properties of H. We do this in two steps:

• (1) The properties of the system G, i.e. axioms defining the theory of G, are theorems in the new theory defined by the problem H:

Q(t, d) ⇒ P (σ(t, d), γ(t, d))
• (2) both models are solving the same problem and the event spec_event of H is refined by the instance of the event event of G for the problem H:

Q(t, d) ∧ P (σ(t, d), γ(t, d)) ∧ I(y) ∧ [s, c := σ(t, d), γ(t, d)]J(y1) ∧ y = y1 ∧ R(L)(y1, y1 ′ ) ⇒ ∃y ′ .(I(y ′ ) ∧ R(K)(y, y ′ ))
Once we establish these two steps, we have a formal verification of the correctness of our concrete solution with respect to the already existing generic project: Property 1 When the given (previous) proof obligations are proved, the new problem H is solved by the development of the problem G, up to renaming and instantiation.

A formal design pattern

When the refinement is proved, the new problem H is solved by the development of the problem G, upto renaming and instantiation. A new project H is created from the project G of the problem G: events are renamed, variables are renamed, instantiations are done. Parameters are not necessarily completely instantiated or renamed: if a parameter is not instantiated then it keeps properties stated in the general model and no new proof obligation is generated. We illustrate this formal design pattern in the following diagram:

H G ◮ H.G G1 ⊲ H.G1 ⊲ Gn ◮ H.Gn H.Gn+1
The diagram tells us where proof obligations must be proved: filled (triangular arrow) symbols show that new proof obligations are generated and require proving; nonfilled symbols show that proof obligations have been generated but their proofs are inherited from the previous project (G). Horizontal arrows represent instantiation. Vertical arrows represent refinement. The proof that model H.G n+1 is a correct solution to the problem H is simplified by re-use of the refinement path in project G.

The formal development in B

For conciseness, we choose to instantiate our formal design pattern in its simplest form, where the generic refinement path is a single refinement step.

Applying the design pattern

We have two generic models (m1 is a solution to problem m0) and a specific model (M CH) which is an instantiation from both generic models; then both specific model (M 0 and M 1) are obtained by this instantiation. Finally, we refine M 1 to a final implementation model M 2. This is illustrated in the diagram, below:

M CH m0 ◮ M 0 m1 ◮ M 1 M 2
In the following, we do not have space to include complete code for all models and so we include snippets of B code which illustrate the main aspects of the application of the design pattern to the e-voting tamper-evident storage requirement. (Complete code for these projects is available from the authors on request.)

Project G

The generic problem model m0

The most abstract generic model must capture the essence of the problem: a vote (v) in storage can be tampered with (be corrupted) but we can detect this as a bad vote. Storage that has not been tampered with contains only good votes. A bad vote cannot be tampered with in order for it to be made good. This suggests modelling a single abstract corrupt event. The invariant property specifies that good and bad are subsets of an abstract V OT E set and that they have no elements in common (so that a concrete vote cannot be both good and bad at the same time). We note that, in order to establish the invariant, m0 generated 5 simple proof obligations6 that were automatically discharged.

At this point, one may ask what happens when a vote that is corrupt is corrupted again. The implicit skip operation models the abstract event where the state of the model is not changed. This is precisely what we require: when we corrupt a vote that is bad we require that it stays bad. Thus, re-corruption may appear in more concrete refinements of m0 provided they refine skip of the abstract model m0. This is precisely what we intend to do in our next model m1.

The generic problem model m1

The refinement in model m1 introduces an abstract mechanism for encoding votes. Constants G_C (for GoodCode) and B_C (for BadCode) are two subsets of the set CODE. These sets are disjoint but don't neccessary cover the set CODE. The constant code is a bijection between V OT ES and G_C. The last constant chg is a relation between CODEs.

The most important property of the relation chg is that a good or bad code can only be changed to a bad one. In B we specify these as P ROP ERT IES of the model.

G_C ⊆ CODE B_C ⊆ CODE G_C ∩ B_C = ∅ code ∈ V OT E ։ G_C chg ∈ CODE ↔ CODE chg[G_C ∪ B_C] ⊆ B_C
We refine the corrupt event to ensure that any encoded vote that has been changed can be recognised as being bad. Furthermore, we refine the skip event to say that if we now allow encoded votes to be changed then a bad vote is guaranteed to stay bad.

corrupt = any v, c, b where v ∈ vt c ∈ G_C b ∈ CODE v → c ∈ Cv c → b ∈ chg then Cv(v) := b end corrupt_again = any v, c, b where v ∈ vt c ∈ B_C b ∈ CODE v → c ∈ Cv c → b ∈ chg then Cv(v) := b end 5.2.

m1 refines m0

There is some additional work in proving that m1 refines m0 as we need to "glue together" the abstract and concrete models using a gluing invariant.

Cv ∈ vt → G_C ∪ B_C good = dom(Cv G_C) bad = dom(Cv B_C)
To glue together the actual set of votes (vt) with the CODE we introduce Cv. Then, the abstract variables good and bad can be defined in the concrete model using Cv.

We note that m1 generated 11 proof obligations and all but one were automatically discharged, with the single remaining obligation easily discharged through interaction with the theorem prover.

Project H

In project G we have abstracted away from how a vote is represented. In project H we work with concrete representations of the votes (within the generic structure of project G) by instantiating parameters of the models in G.

The problem to be solved -M CH

In our pattern, the new problem to be solved is expressed by the model called M CH; which contains all specific constants, and with identical variables and identical event names as can be found in m0. M 0 (resp. M 1) is the model m0 (resp. m1) instantiated using the new constants of M CH and our new project is MCH. M CH is the basis for our iterative refinement development process. The main point of interest is that the refinement between the model M CH and the model M 0, an instance of m0, allows us to guarantee that our specific problem M CH is solved or refined by our intantiated model M 0. For convenience (and space) we present all specific constants in two steps when presenting M 0 and M 1.

M 0 refines M CH and instantiates m0

We start the development with an abstract model where a vote is represented by k bits. In fact, the abstract V OT E set in model m0 is replaced (instantiated) by our more concrete V OT ES:

k ∈ N V OT ES = 1..k → 0..1
We have nothing to prove to verify that this instantiation is correct (there are no additional properties on abstract set V OT E). The proof obligation that M 0 refines M CH is obvious (with the same abstract and concrete events) and done automatically.

M 1 -an intermediate design step

For this step we enrich the representation of a vote by doubling the number of bits. Each bit in the original vote representation is paired with its inverse value. For example, a vote that was represented as 10010 will now be represented by (10010, 01101)

inv ∈ V OT ES → V OT ES ∀(v, i) •   v ∈ V OT ES ∧ i ∈ 1..k =⇒ inv(v)(i) = 1 -v(i)   CODE = V OT ES × V OT ES code ∈ V OT ES → CODE ∀v • (v ∈ V OT ES =⇒ code(v) = v → inv(v))
For the new model, we instantiate the constants of the generic model m0: GC instantiates G_C and BC instantiates B_C and chgv ∪ chgi instantiates chg.

GC and BC are specified as follows:

GC = {v → w|v → w ∈ CODE ∧ w = inv(v)} BC = {c|c ∈ CODE ∧ P C(c)} -GC
Note: in the definition of BC we use a predicate over codes, P C, that is defined to identify all "possible" codes. This predicate is true except in the case where a pair of bits in an encoded vote are both 1. This encoding is not possible because we allow only bits to change from 1 to 0 (and not from 0 to 1) and because all votes are initially coded as good codes (with pairs 01 or 10). P C is defined as follows:

P C(c) = ∃(v, w) • 0 B B B B @ c = v → w ∧ ∀i • 0 B B @ i ∈ 1..k ∧ v(i) = 1 =⇒ w(i) = 0 1 C C A 1 C C C C A
Now we wish to specify that when a change is made to a single bit of a vote's representation (in either of the pair elements) then only a bit 1 can change to the bit 0. We do this by defining chgv to specify how the vote part of the pair can change, and chgi to specify how (symmetrically) the inverse part of the pair can change. The specification of chgi is given below:

0 B B B B B B B B B B @ (v1 → w1) → (v2 → w2) ∈ chgi ⇔ v1 = v2 ∧ ∃i • 0 B B B B @ i ∈ 1..k ∧ w1(i) = 1 ∧ w2(i) = 0 ∧ ∀j • 0 @ j ∈ 1..k ∧ i = j =⇒ w1(j) = w2(j) 1 A 1 C C C C A 1 C C C C C C C C C C A
The specification of chgv is symmetrically defined.

M 1 instantiates m1

We have instantiated 7 our previous generic model replacing: G_C with GC, BC with BC and chg with chgv ∪ chgi. Then we need to prove the instantiation to be correct by establishing the following proof obligation (from the invariant of model m1).

GC ⊆ CODE BC ⊆ CODE GC ∩ BC = ∅ code ∈ V OT E ։ GC chgv ∪ chgi ∈ CODE ↔ CODE (chgv ∪ chgi)[GC ∪ BC] ⊆ BC
For convenience we structure the proof based on the two symmetric cases, depending on whether a change is made using chgi or chgv. To do this, we split both events corrupt and cor-rupt_again into corruptv and corruptv_again, and corrupti and corrupti_again.

For brevity, we give the definition of only one half of the symmetric pair, the chgv case:

corruptv b = any v, c, b where v ∈ vt c ∈ G_C b ∈ CODE v → c ∈ Cv c → b ∈ chgv then Cv(v) := b end corruptv_again b = any v, c, b where v ∈ vt c ∈ B_C b ∈ CODE v → c ∈ Cv c → b ∈ chgv then Cv(v) := b end
We note that for this step we had 7 proof obligations (for the instantiation), 3 of which required interactive proofs.

A final implementation model -M 2

A manchester code is a sequences of 2 × k bits where the oddly ranked bits give the representation of the original k bits of an unencoded vote, and the even rank gives the bit-wise inverse. This is defined by M N CH, below:

M N CH = 1..2 × k → 0..1 mcode ∈ V OT ES → M N CH ∀(v, i) • 0 B B @ v ∈ V OT ES ∧ i ∈ 1..k =⇒ mcode(v)(2 × i -1) = v(i) ∧ mcode(v)(2 × i) = 1 -v(i) 1 C C A
We also define two constants, mv and mi, to extract a vote and its inverse from the manchester encoded (2 × k) bits: 7 In our design pattern, M 1 is shown as simply an instantiation of m1. In fact, in this paper, M 1 is constructed as a refinement of the instantiation. For the sake of brevity, we have combined a horizontal instantiation with a vertical refinement in a single development step. In order to formally proof this, we establish that the invariant in M 1 is true in the refinement M 2. In order to do this, we replace (instantiate) Cv with M chv. Without going into details, we note that in this step there are 15 proof obligations, 5 of which required interactive proofs as they could not be discharged automatically by the tool.

mv ∈ M N CH → V OT ES mi ∈ M N CH → V OT ES ∀(c, i) • 0 B B @ c ∈ M N CH ∧ i ∈ 1..k =⇒ mv(c)(i) = c(2 × i) -1 ∧ mi(c)(i) = c(2 × i)) 1 C C A 5.
M chv ∈ vt → M CH ∀(v, m) • 0 B B B B @ v ∈ vt ∧ m ∈ M N CH ∧ v → m ∈ M chv =⇒ v → (mv(m) → mi(m) ∈ Cv

Conclusions

We have argued that without the adoption and promotion of formal methods, as the foundations of software engineering, developing trustworthy e-voting systems will not necessarily guarantee that they will be trusted. We have demonstrated the application of the formal methods event-B for guaranteeing, through construction, the correctness of a vote store with respect to the requirement for tamper-evident storage. We illustrated the utility of our refinement-based approach by verifying -through the application of a reusable formal design pattern -a store design that uses a specific PROM technology and applies a specific Manchester encoding mechanism. The formal design pattern is a reusable solution to a common design problem -of how genericity can help to structure the refinement proof process -that can be exploited by formal developers who are not necessarily expert.

Future work is mainly concerned with maintainability and extensibility, for example:

• Strongly tamper-evident storage -The design that we have presented in this paper guarantees that the store is weakly tamper evident. It is said to be weak because tampering can be detected once an election is complete. In fact, with minor modifications to the design we can meet the requirement for a store that is strongly tamper evident: so that tampering can be detected during the voting process.

• Election closed bit -There is a separate requirement that no more votes can be recorded once an election is closed.

Clearly, the implementation of this requirement will involve some extension to the storage of votes so that the store is protected against any further addition of votes after the voting process is terminated (known as vote stuffing). A proposed design is to add an election closed bit to the store and to check that this is not set as a guard for the writing of a vote to the store. Of course, with our encoding mechanism we can detect when this bit has been tampered with. However, without formal modelling it is difficult to reason about the consequences of such a design with respect to a potential denial of service attack where the bit is set before the election has really terminated.

• History independent storage -The requirement that the physical order of the votes recorded in the store cannot be used to deduce any information about the vote of a particular voter.

We will analyse the different structuring mechanisms in event-B and the ways in which they can be used to extend our storage requirements.

Figure 1 .

 1 Figure 1. Definition of models

  corrupt =any v where v ∈ good then good := good -{v} bad := bad ∪ {v} end

1 A

 1 Then we introduce two more constants:corruptx b = any v, c, a where v ∈ vt v → c ∈ M chv GD a ∈ 1..2 × k x(a) c(a) = 1 then M chv(v)(a) := 0 end corruptx_again b = any v, c, a where v ∈ vt v → c ∈ M chv ¬GD a ∈ 1..2 × k x(a) c(a) = 1 then M chv(v)(a) := 0 end where: GD = ∀i • 0 @ i ∈ 1..k =⇒ c(2 × i -1) = c(2 × i) ,and v(a) = odd(a) and i(a) = even(a).

  5.1 M 2 refines M 1 It should be obvious that the Manchester code is a correct implementation of our requirements since it is clearly a correct implementation of M 1. Intuitively, M 2 refines M 1 by changing the way in which the votes are encoded. In M 1 they are encoded as a pair of bitsequences; in M 2 they are single bit sequences where the original pair values have been interleaved. For example, the vote 101 is encoded as (101, 010) in M 1 but as 100110 in M 2.

This is analagous to the current common situation where the public have been asked to trust the e-voting machines because they have been independently tested by some appropriately accredited body. Experience now shows that such trust was misplaced.

It is trivial to extend our model to dynamically detect tampering during an election but for simplicity and conciseness we do not present details of this variation of tamper-evidence in this paper.

The prime notation, where we represent the value of a variable x, say, after an event by x ′ is a fundamental part of the modelling language and is used throughout all the models that follow.

We have no formal metric for the complexity of a refinement path; however, intuitively a path is simpler if there are fewer proof obligations that require interactive proof as they cannot be discharged automatically.

We can assume that H and G have no common parameters: x is different from y and events names are different.

An example proof obligation is v ∈ good ∧ good ∩ bad = ∅ =⇒ (good -{v}) ∩ (bad ∪ {v}) = ∅.

* Works of Dominique Cansell and Dominique Méry are supported by grant No. ANR-06-SETI-015-03 awarded by the Agence Nationale de la Recherche.