Copyright © 2001 Logica UK Ltd

In the early 1990s, platform seven , then part of the National Westminster Bank, started developing an electronic cash system, Mondex, based on smartcards.

With e-cash no third party authentication or authorisation is involved, so it is vitally important that the card's security cannot be broken, otherwise criminals could 'print' electronic money. platform seven therefore decided to develop Mondex to the very highest standards.

The highest standards and guidelines for developing systems have traditionally mainly been the domain of the military and security services, with their interest in safety-critical and security-critical systems. But now that such systems are becoming part of every-day consumer services, these standards are being used to develop some of them.

One such standard is the UK IT Security Evaluation and Certification scheme (ITSEC), initially devised to provide levels of assurance for secure operating systems. The scheme, recognised throughout the European Union, is run in the UK by the Communications-Electronics Security Group, which licences organisations known as Commercial Evaluation Facilities to evaluate products.

The highest certification level in this scheme, level E6, mandates stringent requirements on design, development, testing and documentation procedures.

But E6 also mandates the use of formal methods to specify the high level abstract formal specification of the desired security properties (as opposed to the functional behaviour), to specify the lower level design, and to provide a formal proof of correspondence between the two levels, to show that the design does indeed have the abstract security properties.

There is a view that formal methods are too difficult to use on real applications, that the process is slow, cumbersome and costly.

There is also a perception among many in the industry that level E6 is not possible, mainly because of this formal methods requirement. They see formal proofs as being just too difficult, and people equate 'mathematics' with 'impossible'.

Yet platform seven still decided to develop the full Mondex to this highest level -- despite the fact that it had never been achieved before, not even for government sponsored secure computing developments, let alone for a commercial product.

Furthermore, adding this overhead to a development process was thought to be too onerous and costly for a full commercial product.

Designing the secure cash-transfer protocol and correctly implementing it was certainly challenging for platform seven , given the space and speed constraints of a smartcard. These cards have very limited memory, with no built-in operating system support for tasks such as memory management. In addition, careful programming is required to ensure correct functioning if power is withdrawn at any point during processing a transaction: for example if the card has been withdrawn from the reader.

Early in 1994 platform seven contracted Logica to deliver the specification and proof requirements of the E6 development.

Logica's formal methods specialists chose the Z language to write the high level abstract formal specification and the lower level design, and to perform the correspondence proof between them.

The team had little difficulty formalising the design from the existing semi-formal design documents, but producing an abstract security policy model that both captured the desired security properties and could be proved to correspond to the lower level specification was much harder. A very small change in the design -- very small from the perspective of the formal methods team, that is -- would have made the abstraction much easier, but it was deemed to be too expensive, as the implementation work had already gone beyond that point.

Once the original design was successfully abstracted, after much experimentation with different approaches, it emerged that proving the correspondence between the high level specification and the design was not possible using the standard proof rules available in the literature at the time.

The team consulted Oxford University's Computing Laboratory and found that those proof rules were suitable for only certain classes of specification.

Oxford researchers had been aware of the problem for some time but had never come across a major live example. They therefore went back to first principles and with considerable work helped produce an 80-page set of Z proof rules that were applicable to the Mondex specification. Logica then took these raw rules and applied them to the specific case, and achieved the proof with 200 pages of mathematics. The proof discovered one small flaw, and the design was changed to rectify it.

The development of these new proof rules exposed many previously hidden assumptions and restrictions of the classical Z refinement rules, and this has brought a boom a boom in academic research in this area.

The rules have since been published and are now available as part of the standard literature, for others to use.

This development thus demonstrates a fruitful synergy between academia and industry, with each doing what it does best while providing interesting problems and valuable results to the other.

All three organisations involved in this development brought unique skills, without which the full development of the products would not have been possible.

Once it became clear that E6 was indeed going to be achievable for Mondex -- a fact not obvious from the outset -- the decision was taken to develop Multos, a secure smartcard operating system, also to level E6.

Multos allows several applications to reside together yet remain secure from each other on a single smartcard.

This means different application providers can be confident that another application cannot harm their own. Without such guarantees developers would be reluctant to allow their applications, with their secure algorithms and data, to co-reside with others, yet consumers would be reluctant to carry a separate smartcards for each application. A secure operating system is essential for e-commerce based on smartcards.

There were major technical challenges for platform seven in fitting Multos into the very small memory space available while still leaving room for applications such as Mondex to be loaded, all without compromising the clarity of the design needed to achieve correct implementation and E6 certification.

Multos has a seemingly paradoxical security policy: applications are segregated from each other, yet they are allowed to communicate in certain well-defined ways. Furthermore, areas of memory have to be shared, yet the applications must not be able to use this feature to communicate.

Logica, again handling the formal methods development requirements, took ideas from the formal languages CSP and Z, both from Oxford, and showed what the required segregation property meant mathematically. This segregation property was eventually formalised in just two lines of Z, but it then had to be shown to hold for the full scale Multos application. This required several hundred pages of Z proof.

For the Multos project the Logica formal methods team were in close consultation with platform seven's design team from the start.

This raised different issues from those in the Mondex development, where the formal methods specialists came in later. It meant the formal methods team could influence the design in order to make specification work cleaner and clearer -- and the design did change As a result they had to rework their specifications and proofs to keep them in line with the changing design, trying to hit this moving target.

This did result in some frustration, but the improvement in clarity of final design was well worth the effort and did ease the final proof task considerably.

Given a secure operating system, Mondex was then re-engineered into a Multos application.

In 1999, both Mondex and Multos achieved ITSEC level E6 certification -- the first products ever to do so. Mondex is now used around the world in a variety of applications. Multos is internationally recognised as the most secure smartcard operating system available.

Other smartcard application developers recognise that these two products have raised the standard and are themselves beginning to develop their own products to ITSEC certification levels. platform seven is now developing further smartcard products.

Both Mondex and Multos were developed to the highest non-formal industry practice, in parallel with the development of the Z specifications and proofs, in order to gain maximum assurance and quality from the entire process. This stringent development resulted in an initial system design and implementation with astonishingly few bugs. So the E6 certification process, both in its informal and formal requirements, demonstrably resulted in higher quality products. This provided the increased security and consumer confidence necessary to make these products possible.

Some formal development, outside the E6 process, was also applied to defining the intermediate programming language used to write Multos applications. The formal development resulted in a programmer's manual that had a clearer description of the language -- derived in part from the formal specification -- and an implementor's manual that had a clearer definition of the necessary security checks. So the formal methods work demonstrably resulted also in higher quality documentation.

These projects showed that formal proofs do not have to be very big and cumbersome and slow down a project. In neither development were the formal methods tasks on the critical path. All the specification and proof work occurred in parallel with the rest of the development and was ready for evaluation on time.

In fact such new special purpose products provide ideal opportunities for an organisation's first real formal methods development, after the smaller initial training and pilot projects. They are relatively small, simple devices; they have a relatively well defined purpose; the software is not sharing the device with a multitude of other diverse applications. The applications are usually close to the bare metal, under full developer control. All these factors -- small size, isolation and control -- make the formal methods task much more tractable than it is in a less well defined, less controlled area.

Formality brought the platform seven products increased assurance, discovery of errors, cleaner design, and a better understanding of the security properties being claimed. Usability, robustness, fitness for purpose, these are all of paramount importance for products. Formal methods can help make software correct.

Susan Stepney is a principal consultant in Logica's security practice, specialising in the application of formal methods, and a visiting professor of computer science at York University. She is a Chartered Engineer and a professional Member of the BCS.