[GAP] Announcement: NSA Releases Secure Software Project to Open Source Community

[Kathy Fairlamb]

Dear GAP members,

For those of you teaching courses related to secure software  
engineering, you may be interested to learn about the Tokeneer  
project, which AdaCore and Praxis have been working on together for  
the US National Security Agency, and all materials of which have been  
made available to the open source community.

Below is a press release on the project which we have put out today.

Kind regards to all,

Kathy Fairlamb
Communications & Administration
www.adacore.com
---------------------------------------------------
T: +33 1 49 70 67 16
F: +33 1 49 70 05 52
---------------------------------------------------


Tokeneer project shows the way to develop secure systems in a rigorous  
and cost-effective manner
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

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






-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/gap/attachments/20081006/1e7a4ace/attachment.htm