[tt] NSA shows the way to develop secure systems
Brian Atkins
brian at posthuman.com
Mon Oct 6 14:53:28 PDT 2008
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
More information about the Testlist
mailing list