NSA Open Sources Tokeneer Research Project

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

Comments

Re:What is this, an ADA advertisement?

[iamhigh]

The Air Force was teaching it to all programmers in the first level of training at least until 2004 or so. Maybe they still are, but I wouldn't know.

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?

[againjj]

It looks like that a company (Praxis) was able to create part of a security software product (Tokeneer) while following development process for developing security software, in partnership with another company (AdaCore) which provided the tools, and it was funded by NSA. Then it was put out as a press release. The source code is available for free (as in beer) but is not free (as in speech). This was extracted from one of the source files:

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

[iamhigh]

Can you elaborate on Ada vs. ADA? Obviously googling gets you know where fast on that one.

Tokeneer has been written in SPARK Ada...

[hAckz0r]

.. and then linked together by an application written in C, to dynamically loaded/replaceable libraries written in C, and all for running on an OS written primarily in C. Yup, that 'Ada language' sure is secure! I can't tell you how many times I have seen mission critical Ada code linked to faulty C libraries or calling unsafe functions some where below it. Quite often Ada type checking breaks, or becomes null and void, at those interface boundaries and then all bets are off.

It's open source software, and important

[dwheeler]

It's released as open source software - free as in speech, not just free as in beer. At least, that was the intent (I've had lengthy email conversations with Praxis about this). It's just that figuring that out is complicated; you have to seriously trudge through their docs to get the real licensing story.

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.