The development of highly secure, low defect software will be dramatically helped by the release of the Tokeneer research project to the open source community by the US National Security Agency (NSA).

The Tokeneer project was commissioned by the NSA from Praxis High Integrity Systems as a demonstrator of high-assurance software engineering. Developed using Praxis’ Correctness by Construction (CbyC) methodology it uses the SPARK Ada language and AdaCore’s GNAT Pro environment. The project has demonstrated how to meet or exceed Evaluation Assurance Level (EAL) 5 in the Common Criteria thus demonstrating a path towards the highest levels of security assurance.

The unprecedented release of the project into the open source community aims to demonstrate how highly secure software can be developed cost-effectively, improving industrial practice and providing a starting point for teaching and academic research. Originally showcased in a conference paper in 2006, it has the long-term aim of improving the development practices of NSA’s contractors. Tokeneer was created as a fixed-price project, taking just 260 person days to create nearly 10,000 lines of high-assurance code, achieving lower development costs than traditional methods per line of code.

Tokeneer has been written in SPARK Ada, a high level programming language designed for high-assurance applications. Originally a subset of the Ada language, it is designed in such a way that all SPARK programs are legal Ada programs. Ada is the natural choice for mission-critical, high-integrity systems due to its combination of flexibility, reliability and ease of use, and SPARK further adds a static verification toolset that combines depth, soundness, efficiency and formal guarantees.

The project is aimed at both the industrial and academic communities, forming an ideal base for further research in program verification and as a high level teaching aid for educators. It will also be contributed to the Verified Software Repository under the auspices of the current “Grand Challenge” in Dependable Systems Evolution.

The project materials, including requirements, security target, specifications, designs, source code, and proofs are now available here.