[Infowarrior] - NSA Tokeneer (high-assurance computing)

[Richard Forno]

http://www.adacore.com/home/gnatpro/tokeneer/

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 Praxis  
High Integrity Systems 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.

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: 1

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.

< - >

http://www.adacore.com/home/gnatpro/tokeneer/