NSA shows the way to develop secure systems
Posted on 06 October 2008.
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.





Spotlight

Whitepaper: Zero Trust approach to network security

Posted on 20 November 2014.  |  Zero Trust is an alternative security model that addresses the shortcomings of failing perimeter-centric strategies by removing the assumption of trust.


Weekly newsletter

Reading our newsletter every Monday will keep you up-to-date with security news.
  



Daily digest

Receive a daily digest of the latest security news.
  

DON'T
MISS

Fri, Nov 21st
    COPYRIGHT 1998-2014 BY HELP NET SECURITY.   // READ OUR PRIVACY POLICY // ABOUT US // ADVERTISE //