Libre

Project Summary

In order to demonstrate that developing highly secure systems to the level of rigor required by the higher assurance levels of the Common Criteria is possible, the NSA (National Security Agency) asked Altran Praxis to undertake a research project to develop part of an existing secure system (the Tokeneer System) in accordance with Praxis’ Correctness by Construction development process.

This development and research work has now been made available by the NSA to the software development and security communities in an effort to prove that it is possible to develop secure systems rigorously in a cost effective manner.

Process

The development process applied to the Tokeneer ID Station high-integrity development can be summarised in terms of the following key phases:

• Requirements analysis (the REVEAL® process)
• Formal specification (using the formal language Z)
• Design (formal refinement of the specification and the INFORMED process)
• Implementation in SPARK Ada
• Verification (using the SPARK Examiner toolset)
• Top-down system testing

At each stage in the process verification activities were undertaken to ensure that no errors had been introduced. These activities included review and semi-formal verification techniques applicable to the entities being developed.

Project Findings

The Tokeneer ID Station development project has demonstrated that the Praxis Correctness by Construction development process is capable to produce a high quality, low defect system in a cost effective manner following a process that conforms to the Common Criteria EAL5 requirements.

The Tokeneer ID Station system’s key statistics are:

• lines of code: 9939
• total effort (days): 260
• productivity (lines of code per day, overall): 38
• productivity (lines of code per day, coding phase): 203
• defects discovered since delivery: 2

With the aim of achieving EAL5 levels of assurance, we believe that the Correctness by Construction process can achieve EAL7. The proof activity we use in our Correctness by Construction process is sufficient for EAL7, which involves tool supported code proof but manual proof of the Specification and Design. The process can be tightened appropriately to meet the additional quality control requirements of EAL7 by using tools that provide fully integrated electronic support.

What’s Included

The material generated by Praxis under contract to the NSA is distributed under the terms of the Technology Transfer Agreement agreed by Praxis and the NSA. A copy of this agreement is included with (and must always accompany) the release. This material consists of

• The “Core” Tokeneer ID Station Software
• The “Support” Tokeneer ID Station Software
• Tokeneer Discovery Tutorial
• The project documents
• The test cases derived from the system test specification
• The test tokens and biometric data

Read the full report »

Download Tokeneer »