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."
ADA propaganda? (Score:1, Informative)
Re:Tokeneer? (Score:5, Informative)
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?
Re:Very poor summary (Score:4, Informative)
Sure...
ADA is an acronym for American Dental Assocation.
Ada is a girls name (short for Adeline).
Ada (the programming language) was named after Ada Byron. Calling it ADA would be like calling me CHRIS.
Ada Byron is credited with being the worlds first programmer as she came up with some punch cards for the Jacquard (programmable) loom. Something like that. It's been a while.
She was the daughter of Lord Byron - "Mad, Bad and Dangerous to Know" as someone put it (Oscar Wilde?).
Re:Tokeneer? (Score:5, Informative)
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.
VERIFICATION (Score:5, Informative)
If we were able to do formal verification of a binary, then the world wouldn't need to see source code [slashdot.org] to know you can trust third-party written code [slashdot.org]. 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.
Re:ADA propaganda? (Score:3, Informative)
Though, the funny thing was that I thought the US government was not able to hold copyright.
It's not possible to enforce it against U.S. citizens, but it's possible to enforce it abroad. The lack of an explicit software license (free or not) is a bit surprising.
Re:Useless (Score:3, Informative)
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.
Yes, the first assumption should always be that the NSA don't understand security... Or perhaps there are languages and tools that help you write more secure code. Let's be honest, the average Java program is more secure than the average C program, thanks to slightly stronger type checking and bounds checking. Sure, Java isn't a going to magically make your code perfectly secure, but it does make it a little harder to make mistakes, and a little easier to catch them when you do make them. One can imagine that perhaps there are other things that can be done to make mistakes harder again to make, and even easier to catch. Sure, it's all incremental, and nothing is going to be a silver bullet, but enough small gains and it can become worthwhile for software you want to be robust and/or secure.
I've programmed in C and Java, and I've also played with SPARK Ada. Believe me when I tell you that SPARK really does make a huge difference in catching mistakes. Just using SPARK won't magically make your code secure, but it will provide you with very powerful tools to help you write secure code. It really is a very distinct improvement. If it's the Ada part that you find distasteful, then check out JML [jmlspecs.org] and ESC/Java2 [kind.ucd.ie] which provide similar (though not quite as powerful) facilities for Java.
A Security Hole in Java (Score:4, Informative)
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.
Re:ADA propaganda? (Score:4, Informative)
Note that just because it belongs to the US govt, it doesn't mean that the public has access to it. Many works are either classified, or very commonly, deemed FOUO (For Official Use Only) which restricts access to software.
Re:ADA propaganda? (Score:3, Informative)
Though, the funny thing was that I thought the US government was not able to hold copyright.
Government employees cannot initiate copyright (ie, create a work and claim it has a copyright), but copyrighted works (ie, those developed by contractors) can have the copyright assigned to the government (and may be required by contract to do so). Yes, it's a fine splitting of hairs, but that's the deal...
Re:Useless (Score:2, Informative)
Until you've seen in real life a compiler error telling you that you accidentally tried to add a variable holding a distance in meters to one with a distance in feet, you don't know what you're talking about. Although people can find a way to break any language, some programming languages indeed are much more resistant to bugs than others.
In fact, the latest version of F# not only gives a compiler error, but Visual Studio shows the error in real time [msdn.com] when units of measure don't match up. And it comes with a full set of SI units [microsoft.com].