Paper detail

An Automatically Verified Prototype of the Tokeneer ID Station Specification

The Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost effective manner. Altran Praxis (UK) was selected by NSA to carry out the development of the Tokeneer ID Station. The company wrote a Z specification later implemented in the SPARK Ada programming language, which was verified using the SPARK Examiner toolset. In this paper, we show that the Z specification can be easily and naturally encoded in the {log} set constraint language, thus generating a functional prototype. Furthermore, we show that {log}'s automated proving capabilities can discharge all the proof obligations concerning state invariants as well as important security properties. As a consequence, the prototype can be regarded as correct with respect to the verified properties. This provides empirical evidence that Z users can use {log} to generate correct prototypes from their Z specifications. In turn, these prototypes enable or simplify some verificatio activities discussed in the paper.