Slashdot Log In
NSA Open Sources Tokeneer Research Project
Posted by
ScuttleMonkey
on Mon Oct 06, 2008 04:14 PM
from the they-aren't-known-for-their-sharing dept.
from the they-aren't-known-for-their-sharing dept.
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."
Related Stories
Submission: NSA Shows the Way to Develop Secure Systems by Anonymous Coward
This discussion has been archived.
No new comments can be posted.
The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
Full
Abbreviated
Hidden
Loading... please wait.
This smells like a Slashvertisement... (Score:5, Insightful)
...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?
Re:This smells like a Slashvertisement... (Score:5, Funny)
...
Oh, right. Carry on.
Parent
Useless (Score:4, Insightful)
High security languages aren't CAN'T have bugs. (Score:2)
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 langua
Re: (Score:2)
Hmm...
I thought the idea of "Secure languages" was being able to PROVE there were no security bugs on your software because it was correct (if you're willing to pay the price in development time, of course).
At least at first glance, SPARK's claim to 'high security' is on that same line: http://www.praxis-his.com/sparkada/intro.asp [praxis-his.com]
From that point of view, one of the big appeals of Java and other VM languages was precisely that software could potentially be 'provably secure' up to some level (typically with s
Re:Useless (Score:4, Insightful)
Don't say I can't make security holes in Java.
I can make security holes in whatever language I want! Really.
Parent
Re:Useless (Score:5, Insightful)
Parent
Re:Useless (Score:4, Insightful)
Parent
Re: (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].
Re: (Score:2, Insightful)
Re: (Score:2)
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.
Parent
Re: (Score:2)
Please don't argue against a straw man. Nobody tries to make a programming language eliminate all bugs. Just all occurrences of a certain class of bug. For example, if the language has checked array access, then that eliminates array overrun memory trampling bugs, or mitigates them to safely thrown errors. A real integer type, or a bounded numeric type with checking, eliminates bugs caused by silent integer overflow in C-like languages. Of course you can't deal with all errors. That is not to say you
Re: (Score:2)
Sun changed their symbol to JAVA. They're all about Java these days. The major selling point I always hear about Java is that it doesn't have flaws like C does (or "unmanaged languages" is what I hear from people who use more than one of Java/.NET/Python) and so you can't make those nasty security holes like you keep seeing everywhere.
I've argued with people extensively about this, even people who work with Sun or as contacts to Sun or as programmers at Sun; I've never met a Microsoft-linked .NET progr
Re: (Score:2)
I think it's unwise to start out with what any company's marketing department says and then argue against that, because marketing always exaggerates. Nobody with any clue has ever said that you can't make security holes in Java, or that C's low-level machine access is a 'flaw'. Just that certain very common kinds of security hole don't happen, and that C is a sharp tool that needs a lot of care to use correctly.
I'm sorry that apparently you have only discussed this with marketers and overenthusiastic ween
Re: (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 th
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.
Parent
Re:Useless (Score:4, Insightful)
Parent
Re:Useless (Score:4, Insightful)
The final line of GP's comment indicates a sarcastic tone was intended. I doubt GP is suggesting that it is not possible to open a security hole with a VB.NET program.
Parent
Tokeneer? (Score:2)
After Ring TFA, I still have no idea what this Tokeneer thing does. Anybody have some more details?
Also, Ada is neat.
Re: (Score:2)
TOKENEER is a proof-of-concept system being used to prototype new Identification and Authentication (I&A) concepts.
...
The TOKENEER system uses a nested approach to authentication based upon the premise that the trust can be distributed throughout a system to allow for untrusted components to operate. It also utilizes a trusted token to provide authentication information to service access points.
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?
Parent
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.
Parent
Very poor summary (Score:5, Insightful)
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).
Re: (Score:3, Interesting)
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?).
Parent
Re: (Score:2)
I thought you actually meant there was a different language Ada vs ADA!!!! It's late in the day.
Re: (Score:2)
Yes, thankfully there is no programming language called "ADA" :)
Re: (Score:2)
Re: (Score:2)
Sure...
ADA is an acronym for American Dental Assocation.
I thought it was Americans with Disabilities Act...
There's a joke in there somewhere about Ada programmers being disabled...
damn NSA (Score:2)
Tokeneer has been written in SPARK Ada... (Score:2, Interesting)
A challenge? (Score:2)
"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...?
Did I read that title correctly? (Score:2)
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.
Early proof efforts. (Score:2)
I've done work like that. [animats.com] 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 specificati
Re: (Score:3, Interesting)
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: (Score:2)
Re:ADA propaganda? (Score:5, Interesting)
-- 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.
Parent
Re:ADA propaganda? (Score:5, Insightful)
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?
Parent
Re: (Score:2, Flamebait)
And I have shares of Blizzard, I want free WoW. I have shares of Apple, I want free OS X upgrades. I have shares of Microsoft, I want free c
Re: (Score:2)
Re: (Score:2)
That just might be the argument commercial vendors might use to discourage the use of F/OSS in government.
Re: (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: (Score:2)
Any software released by the government and not otherwise classified is in the public domain.
Re: (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...
It's open source software, and important (Score:5, Interesting)
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.
Parent
Re: (Score:2)
It says 'United States Government, as represented by the Director, National Security Agency'. I dunno about you, but it seems to me that the United States as intended is a lot different than the United States most government agencies seem to represent these days.
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.
Parent
Re:ADA propaganda? (Score:4, Insightful)
The copyright notice says All Rights Reserved which means, the NSA claims have all the rights and the contractor has none.
The NSA contract isn't here to scrutinize so what ifs about "who really owns the code" are shots in the dark. Relying on the NSA's claim of ownership is a defense to copyright infringement. Everybody here can develop using the code without worrying about legitimate third party copyright infringement claims.
The fact that the public is able to download the software means the public has access to this software and it is not classified or FOUO.
So, everyone can safely conclude that they are allowed to develop using this code.
I don't mean to be argumentative, the parent post just didn't have a conclusion.
Parent
Re: (Score:2)
Just finished browsing through their Formal Spec (117 pages) and Formal Design (171 pages) - all in Z, and although initially it seems at least understandable, it is a bit much. I wanted to post a piece of spec to show you all what it means, but unfortunately ASCII just doesn't capture the idea in full (shudders).
Basically you've got the requirements -> formal spec -> formal design -> informal design -> code -> code verification -> testing (for the software side, then you got the formal us