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: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.
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: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.
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?
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:1)
I'm not sure what it would take to get it written into law, but I have some sort of idea how a precedent could be set:
I'm hoping that someone starts a project based on it and releases it under a different license on the basis that the government is not allowed to hold copyright. Hopefully this person will be a good lawyer or at least be able to afford one. Then, if the government sues said person, hopefully said person will win in court.
My $0.02
Re: (Score:2)
That just might be the argument commercial vendors might use to discourage the use of F/OSS in government.
Re:Ada propaganda? (Score:2)
Usually anything developed under DoD contract will be owned by the DoD. The nice thing about this is that it means if you are working on a DoD contract, you can ask for the sources to any other relevant DoD program that might help you in your development.
That's only the theory of course. The reality is that anything under someone else's bailiwick is going to require navigating a
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)
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.
Re: (Score:2)
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: (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)
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.
Is this an open source announcement, or.... (Score:1, Redundant)
a marketing attempt to sell SPARK ada tools?
Useless (Score:4, Insightful)
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.
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.
Re: (Score:1, Funny)
Hah, finally found you! I knew sooner or later you would reveal yourself. You're causing the industry trillions of losses each year, immediately refrain from doing us any further harm, evildoer!
Re:Useless (Score:5, Insightful)
Re: (Score:1, Offtopic)
Well, ideally, distances measured in meters and in feet would be two (sub)classes that, when cast to each other, automatically take care of the conversion. And in C++, you could even add them up, yielding the distance in units of the right hand side (presumably). -pedantic mode off-
Re: (Score:1)
is
type distance_feet is new float;
type distance_meters is new float;
x : distance_meters
y : distance_feet;
begin
y
end proc;
causes GCC to print
prog.adb:18:145: expected type "distance_feet" defined at line 18
prog.adb:18:145: found type "distance_meters" defined at line 18
Re:Useless (Score:4, Insightful)
Re: (Score:2, Insightful)
Re: (Score:2)
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].
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: (Score:1)
Formally prove resistance to XSS or XSRF and I'll listen. Until then...
Re: (Score:2)
Personally, I wouldn't call formal proof shite, but I would call it unattainable for practically any software of sufficient complexity to be useful. This is even more true once you factor in acceptable cost of development in both time and money.
That's not to say that tools that help with validation are useless, just that they will tend to either fall short of the goal (but may be better than nothing) or will add too much cost to a project (even if the tool itself is free).
In a world where management is some
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.
Re:Useless (Score:4, Insightful)
Re: (Score:1)
For a Java program, prove that it cannot possibly run out of memory. Impossible to do in a language which allows dynamic allocations.
Re: (Score:2)
Strange, I spend most of my day finding security holes in applications written in Java and C#.
Certain classes of attack are made difficult by bounds checking in virtual machine run languages, but let me assure you they are still full of logic flaws and other security holes.
There is no language that can compensate for people who don't know and/or don't care about security. There are tools and frameworks that can help people who do know and care however.
Re: (Score:2)
These days, Java might easily invite security holes, just not buffer overflows of stack violations. The manageability of security is inversely proportional to the number of layered modules, libraries, and buzzwords in the application ;-)
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?
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.
Re: (Score:1)
The Common Criteria replaces an earlier scheme here in the UK known as ITSEC. It had a range that went to E6 (broadly equivalent to Common Criteria EAL-7). There were in fact a number of software products commercially produced to ITSEC E6. These were the MULTOS smartcard operating system, and the Mondex electronic purse that sat thereon.
Re: (Score:2)
Multos seems to have an E6 and EAL 4 at the moment. I wonder how you could create a smart card OS that does EAL 7 actually, but maybe it is possible, even though the functionality of a smart card OS is already pretty large.
But this is on a rather restricted system. The problem comes when you get to PC software. There are just too many things that may come in contact with the part you are trying to certify, so it gets a lot harder that way. You can see from this project how many things are, for instance, to
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?).
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:1)
Re: (Score:2)
I love it!
Re: (Score:2)
Re: (Score:2)
Right, my mistake.
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)
Claim of formal verification too grand (Score:1)
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
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