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."
Erm, TFA seems to contain more "facts" about ADA than real information about the project or the release of the source code (license?).
"I decided I could write something better than everything out there in two weeks. And I was right." - Linus Torvalds
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?
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?).
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.
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 and ESC/Java2 which provide similar (though not quite as powerful) facilities for Java.
Craft Beer Programming T-shirts
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.
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 when units of measure don't match up. And it comes with a full set of SI units.