NSA Open Sources Tokeneer Research Project 94
An anonymous reader writes to mention that the Tokeneer research project has been released to the open source community by the US National Security Agency. The main goal of this project was to show how highly secure software can be developed cost-effectively. "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."
Re:What is this, an ADA advertisement? (Score:3, Interesting)
Besides, this website it programmed in perl... are you going to claim it is harder than perl when it comes to decent sized projects (scripts, yes perl wins).
Re:ADA propaganda? (Score:5, Interesting)
-- Tokeneer ID Station Core Software
--
-- Copyright (2003) United States Government, as represented
-- by the Director, National Security Agency. All rights reserved.
--
-- This material was originally developed by Praxis High Integrity
-- Systems Ltd. under contract to the National Security Agency.
Though, the funny thing was that I thought the US government was not able to hold copyright.
Re:Very poor summary (Score:3, Interesting)
Tokeneer has been written in SPARK Ada... (Score:2, Interesting)
It's open source software, and important (Score:5, Interesting)
The problem is that they (NSA/Praxis) didn't simply slap an open source software license on it. Instead, you have to hunt in Praxis' user's guide (section 2 on licensing), which says that you (the public) get all the rights that Praxis got from NSA. Then, you have to look at the NSA/Praxis contract, which says that you have the right to use, modify and redistribute (that's an imperfect quote from memory, see the files for the details). I haven't analyzed this in great depth, but I can confirm (after several emails with Praxis) that the intent, at least, was to release Tokeneer as open source software.
I wish Praxis had just slapped a standard open source software license on the code. For the code they wrote themselves, Praxis simply applied the 2-clause BSD license, which is unambiguously open source software. Presumably their contracts made them release it in this unusual way.
Anyway, this is important and a good thing. In theory, if you could prove that any given program is correct, you'd eliminate or greatly reduce a lot of our problems with software. Currently, there are almost no published examples of formal methods applied to actual programs. And without examples, it's hard to make things better, improve on them, etc. This is not the end, but perhaps it's the glimmer of a beginning.
You're absolutely correct, the tools required to prove this are not open source software. Thus, I'd say this is not an "open proof" (an open proof is where the source code of the program, the proofs, and the required tools are all open source software). But it's a step forward from having almost no publicly-available examples of real programs where formal methods have been applied to this degree.