NSA Releases Secure Software Project to Open Source Community

Tokeneer project shows the way to develop secure systems in a rigorous and cost-effective manner

NEW YORK, PARIS, and BATH, U.K. - VSTTE 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 project materials, including requirements, security target, specifications, designs, source code, and proofs are now available at www.adacore.com/tokeneer.

The Tokeneer project was commissioned by the NSA from UK-based 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.

“The Tokeneer project has the potential to revolutionize the development of highly secure systems,” said Robert Dewar, President and CEO of AdaCore. “By releasing Tokeneer to the community, the NSA will help drive good programming practice and demonstrate the importance of SPARK and Ada to the emerging security market. We are delighted to be involved with Praxis and the NSA in this ground-breaking project.”

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.

“We are extremely proud of the Tokeneer project,” said Keith Williams, Praxis Managing Director. “We hope the research, teaching, and open-source communities will put the material to good use as a model of high-assurance software development.”

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 Tokeneer project is a milestone in the transfer of program verification technology into industrial application. Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research. It will serve as a touchstone to chart and measure progress of the basic science of programming, on which the technology is based.”

Sir Tony Hoare, Fellow of the Royal Society (FRS) of Microsoft Research, and founder of the Grand Challenge

“The publication by Praxis and NSA of the Tokeneer system is a fantastic contribution to the software engineering research and teaching community. Good case studies have been very hard to find, and have often been proprietary. Finally, we have a full and open example of a development from a world leader in high integrity systems with exemplary requirements, specifications, design and code. I’m very excited about the impact this might have in our field, in both teaching and research, and the potential it might have in moving us towards a more open community with greater collaboration between industry and academia, and a more constructive engagement of theory and practice.”

Professor Daniel Jackson of Massachusetts Institute of Technology, Computer Science Laboratory

“Ada is a very complete language that allows us to present procedural and object-oriented concepts. It supports and encourages data abstraction and provides helpful diagnostic messages to beginning students when they make the usual kinds of beginner’s mistakes. In addition, Ada programs are quite readable due to well-chosen syntax and recognizable symbols for standard operations, and once a student has learned Ada, he or she finds it easy to learn a second language, such as Java or Visual Basic.”

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore’s flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see http://www.adacore.com/home/company/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains such as financial services.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

About Praxis and Correctness by Construction
Praxis is a systems engineering company specializing in safety and mission critical applications. Praxis leads the world in specific areas of advanced systems engineering such as: ultra low defect software engineering, safety engineering for complex or novel systems, and tools/methods for systems engineering. Praxis offers clients a range of services including turn-key systems development, consultancy, training and R&D. Key market sectors are Aerospace, Defence, Air Traffic Management, Railways and Nuclear. The company operates internationally with active projects in the US, Asia and Europe. The UK Headquarters are in Bath with offices also in London, Loughborough and Paris. It is wholly owned by Altran Technologies which is a global leader in innovation engineering and employs 17,500 engineers across the world. www.praxis-his.com

Correctness by Construction (CbyC) is Praxis’s method of developing software. CbyC uses tools and techniques that aim to make it both difficult to introduce defects during software development, and straightforward to correct defects early in the development lifecycle. These tools and techniques are often required by industry standards for safety and security critical software, and as a result Praxis has developed an expert capability and track record for the development of such software. CbyC is cost effective because reducing defects significantly reduces risk and rework.

About National Security Agency
The National Security Agency/Central Security Service is America’s cryptologic organization. Further information is available from the NSA website. www.nsa.gov