Applying Formal Methods to the Design of Smart Card Software

The goal of this work is the design of a language for the implementation of smart card applications, specifically an operating system, as high integrity software. The integrity of a piece of software is demonstrated by proving various properties of the software. The language must therefore exclude any constructs that would make such proofs unreasonably difficult. An untyped language is not only very difficult to reason about formally but also allows many unchecked run-time errors that are eliminated in a, suitably, typed language. We would like the type system of the language to be strong, expressive and simple. Unfortunately the language is required to be able implement certain routines that might normally be part of the run-time system, notably the storage allocation routines. This requirement is likely to force the adoption of a weaker type system than we would ideally prefer. In order to understand the consequences of this requirement we first had to understand in more detail the storage allocation system required. To this end we prepared an initial Z specification of a memory manager for a smart card system. We then produced an executable specification and a Miranda implementation of the memory manager. These led to a modified Z specification for the existing implementation in both an abstract and refined form. The refined form of the modified Z specification was further refined to a detailed design. This was followed by some analysis about the general requirements and implications of a storage allocation function and an example implementation in Modula-3. Finally a proposal for a type system was prepared, describing the advantages of certain choices and the problems introduced by others