The Grand Challenge in Verified Software - Projects
The 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.
A 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.
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.
The The Posix Filestore challenge is the specification and verification of the POSIX file-store interface of Unix. It involves a small subset of POSIX (which is detailed below) suitable for flash-memory hardware with strict fault-tolerant requirements to be used by forthcoming NASA's Jet Propulsion Laboratory missions. Obviously, we do not stop there: following the GC's motto, we see this as an important research opportunity far beyond JPL's original pilot project.
See also:
Page
created by Jim Woodcock, 18th June 2007,
last updated by Juan Bicarregui, 6th August 2007