|
GC6: Dependable Systems Evolution
|
Mondex
The first VSR pilot project experiment took place during 2006, and involved the successful mechanisation of the verification of a commercially sanitised version of the first project to meet the high-assurance standard, ITSEC Level 6: the Mondex smart-card banking application. The original formal specification and design are publicly available. The mechanisation was accomplished by eight international research groups using different theories and tools, and the project remains open for other groups to contribute. The Mondex case studyThe Mondex case study was initially a year-long pilot project launched in January 2006. The objectives were to demonstrate how research groups can collaborate and compete in scientific experiments, and to generate artifacts to populate the Verified Software Repository. To do this, we challenged the participants to verify a key property of the Mondex smart card, and to demonstrate the current state of proof mechanisation. Mondex is an electronic purse hosted on a smart card. It was developed in 1996 to the high-assurance standard ITSEC Level E6 by a consortium led by NatWest, a UK high-street bank. Purses interact using a communications device, and strong guarantees are needed that transactions are secure, in spite of power failures and mischievous attacks. The business case for using Mondex is based on the requirement that electronic cash can’t be counterfeited. The implementation requires that this is achieved with transactions being completely distributed with no centralised control. All security measures must be locally implemented with no real-time external audit logging or monitoring. The original project ten years ago involved extensive verification of this seriously security-critical application. The software house Logica, supported by the University of Oxford, used the Z notation for the development process. Formal models were constructed of the system and its abstract security policy, accompanied by hand-written proofs that the system design possesses the required security properties. The abstract security policy specification is about 20 pages of Z. The concrete specification (an n-step protocol) is about 60 pages. The verification, suitable for external evaluation, is about 200 pages of refinement proof and 100 pages of derivation of refinement rules. The original proof was carefully structured for understanding, a fact much appreciated by the Mondex case study groups. It was vital in successfully getting the required certification, but it was also useful in finding and evaluating different models. The original team made a key modelling discovery: an abstraction which gave a precise security property and explained why the protocol is secure. The proof revealed a bug in the implementation of a secondary protocol. The failed proof attempt explained what had gone wrong and gave a convincing counterexample that the protocol was flawed, providing the insight to change the design to correct it. Third-party evaluators also found a bug: an undischarged assumption. The Mondex challengeA sanitised version of the Mondex documentation is publicly available. It contains Z specifications of the security properties, an abstract specification, an intermediate-level design, a concrete design, and rigorous correctness proofs of security and conformance. Originally, there was no question of mechanising the proofs: a contemporaneous email records, “mechanising such a large proof cost-effectively is beyond the state of the art”. The Mondex challenge was to investigate the degree of automation that can now be achieved in the correctness proofs. The Mondex players
These seven teams agreed to work for one year, without funding. Meanwhile, separately and silently, a group in Augsburg began work using KIV and ASMs. Two distinct approaches quickly emerged. The Archaeologists, who make as few changes as possible to original documentation. Their argument is that they shouldn’t change models just to make verification easier: how would they know that their results had anything to do with the original specification? The Technologists, who use the best proof technology now available. But these new tools don’t work for Z, so they had two choices: either translate the existing models into new languages; or to create new models better suited to new tools. FACJ papers on Mondex
The work of six of the groups is recorded in a special issue of the Formal Aspects of Computing Journal, and the following sections, which are based on the special issue's editorial, summarise these papers. The Certification of the Mondex Electronic Purse to ITSEC Level E6
Woodcock, Stepney, Cooper, Clark, and Jacob were all involved in the original work on Mondex; the first three were specifiers and the last two evaluators. They recall the work that led to the successful certification of the Mondex electronic purse, and the research that this inspired. The paper contains an introduction to the Mondex specification and refinement, and an overview of the proof.
Mondex, an Electronic Purse: Specification and Refinement Checks with the Alloy Model-Finding Method
Ramananandro started from the existing specification on Mondex in Z, and constructed a specification in the Alloy specification language, which is based on relational first-order logic with transitive closures. The experiment shows that, if the concerns about finiteness are dropped, then the Mondex specification can be expressed in first-order logic without transitive closures. Ramananandro checked the specification with the Alloy Analyser, a tool for finding models. The Analyser translates the specification into a boolean formula, which it then tries to satisfy. If an assignment of variables is found, then the program translates it back to get a counterexample. This can be accomplished only for bounded numbers of objects: their scope. The specification has been checked for a scope of at most eight objects of each kind. The analysis found several bugs in Mondex: (i) purses can hold unauthentic transaction details; (ii) a wrong case analysis in a proof; (iii) a mistake in a framing schema.
Verification of Mondex Electronic Purses with KIV: from Transactions to a Security Protocol
Haneberg, Schellhorn, Grandy, and Reif report on three major results from their experiment.
One person month was needed to formally prove the Mondex case study.
An Incremental Development of the Mondex System in Event-B
Butler and Yadav carried out Event-B development of the Mondex system using B4free, a proof obligation generator and proof tool for B. Their development is characterised by the use of many levels of refinement that require a larger number of simpler proofs. Their complete development consists of ten levels: an abstract specification and nine levels of refinement. The full development resulted in 703 proof obligations, of which over 97% were proved automatically. The remaining proof obligations were proved interactively using B4free. The development took approximately two weeks of total effort spread over several months. The bulk of the work was spent in constructing models at different levels of abstraction and in finding the right gluing invariants. They did not make use of the original invariants, but used their theorem prover to guide the discovery of new ones. Most of the interactive proof effort was used to discover new invariants rather than to discharge proof obligations.
Modeling and Validating Mondex Scenarios Described in UML and OCL with USE
Kuhlmann and Gogolla describe the Mondex case study with a simple UML class diagram, including a class representing purses with appropriate attributes and a single operation transfer. The original constraints have been formulated either as OCL class invariants or as OCL pre and postconditions of the transfer operation. The UML class diagram and OCL constraints have been syntactically checked by the USE tool, which validates a specification by testing it with various scenarios. The scenarios are specified as single UML object diagrams, or by constructing a sequence of operation calls leading from an explicitly given start state to a result state. During scenario validation, the validity of invariants and pre and postconditions are checked by the USE tool. The states obtained are then further explored with OCL queries retrieving interesting objects and properties. The authors have validated the abstract specification of Mondex using both positive and negative test cases.
Specification, Proof, and Model Checking of the Mondex Electronic Purse using RAISE
George and Haxthausen’s approach using RAISE is is similar in spirit to the original Z approach, in that it contains an abstract, an intermediate, and a concrete specification, and is based on refinements between these three. But the detail is quite different. The abstract level sees the problem as one in accounting, and contains only three values: the total money in circulation, the total money in messages in transit, and the money that has been lost. The intermediate level introduces purses with individual balances, current payment details and statuses, but with an abstract logging mechanism and no message sequence numbers. The concrete level defines the purses’ exception logs, the log archiving mechanism and the sequence numbers. The proofs were done using a translator from the RAISE Specification Language (RSL) to PVS and the PVS theorem prover itself. The proofs are large, but straightforward; about half were proved automatically. The invariants are quite complicated, and their construction required a detailed understanding of the protocol and why it works. They also used a translator from RSL to SAL and (with the help of Marko Schütz of the University of Puerto Rico at Mayagüez) model checked the specification. This required reducing the size of the model in various ways, in particular to two purses and four sequence numbers. With the SAL model checker they were able to check the basic correctness conditions, and also (i) some liveness properties like transfers between purses and loss of money being possible, (ii) that all the invariants hold, and (iii) that confidence conditions (subtype correctness and precondition satisfaction) are true, using a second translation to SAL generated by the RAISE tool.
Mechanising Mondex with Z/Eves
Freitas and Woodcock mechanised the original work using Z/Eves, making only a few very small changes to the original models, so the mechanisation can be regarded as a reference model. They took about eight weeks to complete the mechanisation of the entire specification and refinement and its proof. The Z/Eves theorem prover was available ten years ago, so the experiment demonstrates that the mechanisation of the proof could have been carried out when the original work was done, and that it would have required about 10% of additional effort. Several problems were found: (i) operations involving inauthentic purses; (ii) assumptions regarding finiteness; (iii) four missing properties in the intermediate model; and (iv) an undocumented assumption in the upper refinement. |
|
Contact: jim@cs.york.ac.uk Last updated: 6th December 2007 |