An Automatically Verified Prototype of the Tokeneer ID Station Specification

TL;DR

This paper demonstrates that Z specifications for the Tokeneer ID Station can be encoded in {log}, enabling automatic proof of security properties and generating correct prototypes, thus supporting rigorous and cost-effective secure system development.

Contribution

It introduces a method to encode Z specifications in {log} for automatic proof and prototype generation, enhancing verification of security properties.

Findings

All proof obligations were discharged using {log}

The generated prototypes are correct with respect to verified properties

Supports empirical validation of {log} for Z-based specifications

Abstract

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.