MRS Award‎ > ‎

2011 Microsoft Research Verified Software Milestone Award Citation

The Microsoft Research Verified Software Milestone Award is made jointly to Janet Barnes and Rod Chapman for the Tokeneer Project. Specifically, the award is given in recognition for Janet's technical leadership and Rod's management of the public release and promotion of Tokeneer. The project was a decisive success. As a verified software experiment, Tokeneer demonstrates the cost-effective application of software verification tools in an industrial context. The leadership shown by both Janet and Rod was fundamental to this success and the significant contribution Tokeneer has made to the Verified Software Initiative.

The Tokeneer ID Station is a project conducted by Altran Praxis for the US National Security Agency. The project was eventually intended as an experiment to supply evidence about whether it is economically feasible to develop systems that can be assured to the higher levels of the Common Criteria Security Evaluation, the ISO/IEC 15408 standard for computer security certification. The project was a rare and valuable experiment in the controlled measurement of productivity and defect rates and, remarkably, the entire project archive is openly available and may be freely downloaded.

The Tokeneer ID Station project extended an earlier NSA research project investigating the use of biometrics for physical access control to a secure room containing user workstations. Users have smartcard security tokens that must be used both to gain access to the room and to use the workstations once the user is inside. There are smartcard and biometric readers outside the room; if a user passes certain identity tests, then the door opens for entry. Authorisation information is written onto the card for subsequent workstation access, describing privileges the user can enjoy for this visit, including times of working, security clearance, and user roles.

Praxis developed this small-sized security system using formal verification methods, showing that it was possible to reach the higher assurance levels of the Common Criteria. The high-integrity development process used the following phases:

  • Requirements analysis, using the REVEAL process
  • Formal specification, using the Z formal specification language.
  • Design, formally refining the specification, and using the INFORMED process.
  • Implementation in SPARK Ada.
  • Verification, using the SPARK Toolset.
  • Top-down system testing.

Since the open-source release of the project, its results have been subjected to intense scrutiny by research teams and individual security experts, leading to instructive and constructive discussions.