Using Formal Methods to Cultivate Trust in Smart Card Operating Systems

To be widely accepted, smart cards must contain completely trustworthy software. Because smart cards contain relatively simple computers, and are used only for a specific class of applications, it is feasible to make the language used to program the software components focused and tiny. Formal methods can be used to precisely specify this language and to reason about properties of the language, which results in more trustworthy software. We explore this process by specifying the core of a proprietary systems programming language for smart card operating systems. We show how the specification obtained is used in proofs, and in the development of tool support