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
...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
a marketing attempt to sell SPARK ada tools?
"To those who are overly cautious, everything is impossible. "
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.
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).
No comprende? Let me type that a little slower for you...
After Ring TFA, I still have no idea what this Tokeneer thing does. Anybody have some more details?
Also, Ada is neat.
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).
How'd they know I did some Token'-eer research last night?
We figured out a long time ago that it's easier to elect seven judges than to elect 132 legislators.
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.
High security languages aren't about fixing things so you CAN'T have bugs. (You always can, because you can write different programs to do different things in them, and a program that does ONE thing - even if perfectly - is horribly buggy if the intent is to do something else.)
High security languages are about making it easier to avoid bugs.
Like with clear syntax. And compiler helping out by checking everything it can possibly check. Just for starters.
(Which is not to say that ADA is such a language. B-) But pre-ANSI C, for instance, is a fine example of being simple and clear while handing you as much rope as you need to fashion your personal noose.)
Bantam Dominique roosters crow a four-note song. Once you've heard it as "Happy BIRTHday" you can't NOT hear it that way
While this example is not particularly interesting, Ada is really a veryn good language and much more secure than what is commonly used.
"Ada is the natural choice for mission-critical, high-integrity systems due to its combination of flexibility, reliability and ease of use". I'm not sure who agrees with that blanket statement, other than the author of the article that this was lifted from. It sounds like a Microsoft spiel on .Net for crying out loud.
I want to delete my account but Slashdot doesn't allow it.
From the full report: "The aim of this activity is to capture the system security properties unambiguously. These security properties are the key system properties that must hold of the system in order for it to satisfy its security obligations. The security properties were expressed using the Z notation; the same notation as was used for the Formal Specification. The security properties were captured as proof obligations on the Formal Specification, so the same level of abstraction and context was used for expression of the security properties as was used in producing the Formal Specification. By using the notation and context of the Formal Specification it was possible to prove that the Formal Specification exhibits the Security Properties. The proof took the form of an informal justification, with a discussion of the arguments required to perform each stage of the proof. EAL5 does not demand proof of these properties, but a sample of the properties were proved to be held by the specification, and then later by the code. At the higher levels of certification such proofs are necessary, and can be carried out either rigorously by hand or using tool support."
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.
.. 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.
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.
"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."
So, first exploit in...?
Oh, say does that Star-Spangled Banner entwine / The myrtle of Venus with Bacchus's vine?
If the National Security Agency is doing a lot of toking, that would explain quite a bit about their recent performance... millions of innocent Americans being spied on without warrants, and Osama Bin Laden still out there.
I piss off bigots.
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.
Tell that to NASA.
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)
Just be because you can teach it doesn't mean it's all simple and easy to use. What's your point? You can teach anything to anyone.
Where did I mention anything about Perl? Sheesh, what are you smoking?
Have you ever actually used Ada for a real project? I have. It is like filling out tax forms. It's not "hard" per-say but it tedious as all hell.
I've done work like that. But it was a long time ago, back in the early 1980s. It took over an hour on a VAX 11/780 to verify a few hundred lines of code. (See the example auto engine control program that starts on page 55; this was funded by the Ford Motor Company.) Today, it would take under a second.
Proof of correctness systems are quite feasible, but a pain to use. They also tend to be developed by people who are in love with the formalism, which can be a problem for programmers. Formal specifications are hard to write and harder to verify, which is the real problem. However, automatically grinding through code and finding all potential overflow and subscript errors is quite practical. We were doing that in 1984. You get about 95% of the checks verified automatically, and then have to provide additional information to get the rest of them satisfied. That's where the human effort goes. If you can formalize the concept of "bad stuff that should never happen", which is something NSA tries hard to do with "mandatory security policies", you have a hope of verifying it.
There have been some impressive proof efforts over the years. There's been quite a bit of effort devoted to proof of correctness for hardware at the VHDL level. Boyer and Moore did a proof of correctness for AMD's FPU after Intel had the famous Pentium divide bug.
What really set back the field was the replacement of Pascal by C. Pascal has well-defined semantics that can be formalized. C, and C++, do not. That's why I got out of the field.
There was some nice work on Modula verification at DEC in the 1990s, but it died with DEC. Some of the same people went to Microsoft and built a verifier for a dialect of C#. There's been some work at Rational over the years. But it's never gone mainstream.
How easy is it to screw up with ADA? From what I understand, the point isn't to enable rapid development, but to have a well-behaved result.
http://outcampaign.org/
They claim "Ada is the natural choice for mission-critical, high-integrity systems due to its combination of flexibility, reliability and ease of use"
Hmm, must have been a different language that than I know as Ada. The Ada I know is about as flexible as concrete. It was reliably painful to program. And 'ease of use' was never part of the language.
My first choice for an Ada program was of course a "Hello, World!"-program. Painful to program, took ages to compile, and the executable was about 60 times bigger than the one of a "Hello World!" in C. And don't ask what it did in the measurable time between launching the program and finally printing that one simple line.
Even the DoD gave up on Ada, and went C/C++. "Ada lives" has the taste of a rising egyptian mummy. Some things better stay dead, once dead. And this language was dead before it was released.