[tt] NSA shows the way to develop secure systems

[Brian Atkins]

http://www.net-security.org/secworld.php?id=6619

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 Praxisb Correctness by Construction (CbyC) methodology it uses the SPARK 
Ada language and AdaCorebs 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 NSAbs 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 bGrand Challengeb in Dependable 
Systems Evolution.

The project materials, including requirements, security target, specifications, 
designs, source code, and proofs are now available here. 
http://www.adacore.com/tokeneer
-- 
Brian Atkins
Singularity Institute for Artificial Intelligence
http://www.singinst.org/
_______________________________________________
tt mailing list
tt at postbiota.org
http://postbiota.org/mailman/listinfo/tt

----- End forwarded message -----
-- 
Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org
______________________________________________________________
ICBM: 48.07100, 11.36820 http://www.ativel.com http://postbiota.org
8B29F6BE: 099D 78BA 2FD3 B014 B08A  7779 75B0 2443 8B29 F6BE