Slashdot Mirror
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."
...because although Tokeneer has been released as open source the SPARK toolchain is owned by a company and the specification for SPARK is fully controlled by them. Has money changed hands somewhere?
--- Nick, hard at work
Java is also the perfect high security language, because you can't make security holes with it. Same with C#. Same with VB.NET. We've heard this again and again from people who simply don't understand the problem.
Support my political activism on Patreon.
What is being released is a small sub-component of the Tokeneer called the TIS ("Tokeneer ID Station") which reads biometric info about a user and if it matches signs a token so that the user can be authenticated to other components on the workstation. It's potentially an interesting little nugget of code, but not something I expect the open source community to get very excited about.
As for the existing comments on this story, I agree this is a bit like a sales pitch (and I used to work in Ada myself). Note that it's Ada not ADA (it's named after Ada Byron, Countess of Lovelace).
-- 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.
It's a Biometric Token system. I haven't been able to find out any more, so I'm now downloading all of their software, just to find this out.
It's a lot about ADA, about contract based design, about checking invariants, and NOTHING about the actual functionality. As somebody who is in security and knows about Common Criteria first hand I must say this might be a very interesting thing. EAL 5 is not something to be sneered at.
If the software actually does something, that's another matter. I'll try right away. I'll let you know when I got it running, if it ever does. Now lets hope the website has not been hacked and that it doesn't contain a virus :)
Where's the secure hash stored on an offsite SSL page?
I don't know one way or the other, but one thing is certain -- anything the tax payers pay for should be owned by the taxpayers and controlled by taxpayers as far as can be deemed appropriate. (So, government buildings cannot be used by the homeless to sleep in!) But something as easy to share as software should definitely be owned by and made available to the people.
I wonder what it would take to get that written into law?
There I am replying to myself.
This is basically a proof of concept piece of code. It shows that Common Criteria EAL 5 (and possibly further) is not out of reach for a software program. EAL 5 and further require (semi) formal proof that a system is correct:
* EAL-1: Functionally tested
* EAL-2: Structurally tested
* EAL-3: Methodically tested and checked
* EAL-4: Methodically designed, tested, and reviewed
* EAL-5: Semi formally designed and tested
* EAL-6: Semi formally verified, designed, and tested
* EAL-7: Formally verified, designed, and tested
Now anybody who is in software engineering knows that this is not a very light requirement. You can write tests until you die of old age, but even then you won't be able to prove anything is fully conform demands.
The system itself is pretty "simple": the hardware consists of a biometric device, two smart card readers and a display device. That's all. Oh, and a door of course, since that is the basic function. It's about opening a door :)
But that's not important at all. What's important that this is a development environment with which you can build *very* secure software, that can be verified against EAL 5. In that respect this is indeed a sales pitch. A rather interesting one, I don't think there are many EAL 5 certified *software* products.
It's all about the formal verification, or the "correctness" of the implementation (binary executable) of the problem. If you follow the works of the late Edsger Dijkstra, he argued that all code should really be an abstraction of a formal mathematical proof of a solution to a problem. Now, most "agile" software developers through that out the window as shite, but we need to find a compromise somewhere in between.
If we were able to do formal verification of a binary, then the world wouldn't need to see source code to know you can trust third-party written code. Ada or whatever language, the research significance here is that the characteristics of the language and compilation that yields positive steps towards formal verification. So, maybe for you "secure" is "I patched it and today's signature database from [insert vuln scanner] doesn't find any holes", but for three letter institutions (and anyone who has worked diligently enough in security to become jaded like me) that's just not good enough. A better definition of "secure" software would be "I know what it is intended to do and I can formally prove it does that and only that."
Word of the day is verification.
libertarian: (n) socially liberal, financially conservative; neither left, nor right.
ResultSet readFromDatabase(String userInput)
{
String sql = "select * from users where userid = " + userInput;
PreparedStatement psMyStatement = connMyConnection.prepareStatement(sql);
ResultSet rsResults = psMySQLStatement.executeQuery();
return rsResults;
}
This is called a SQL Injection security hole. You can write it in practically any language that connects to a database.
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.
- David A. Wheeler (see my Secure Programming HOWTO)