US National Security Agency 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 – October 6, 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 here.

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 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 the 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, making development costs lower than traditional methods per line of code.

“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.”

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 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."

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, 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

Discover more about the Tokeener Project here.   

Discover more about SPARK here.

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.

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 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, railway 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 National Security Agency www.nsa.gov
The National Security Agency/Central Security Service is America’s cryptologic organisation. Further information is available from the NSA website.

Press Contacts
Leena Chauhan
Praxis High Integrity Systems
leena.chauhan@praxis-his.com

Jamie Ayre
AdaCore
press@adacore.com