Forgot your password?
typodupeerror

NSA Open Sources Tokeneer Research Project 94

Posted by ScuttleMonkey
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."
This discussion has been archived. No new comments can be posted.

NSA Open Sources Tokeneer Research Project

Comments Filter:
  • ADA propaganda? (Score:1, Informative)

    by etinin (1144011)
    Erm, TFA seems to contain more "facts" about ADA than real information about the project or the release of the source code (license?).
    • Re:ADA propaganda? (Score:5, Interesting)

      by againjj (1132651) on Monday October 06, 2008 @05:43PM (#25277923)
      It looks like that a company (Praxis) was able to create part of a security software product (Tokeneer) while following development process for developing security software, in partnership with another company (AdaCore) which provided the tools, and it was funded by NSA. Then it was put out as a press release. The source code is available for free (as in beer) but is not free (as in speech). This was extracted from one of the source files:

      -- 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:5, Insightful)

        by erroneus (253617) on Monday October 06, 2008 @06:07PM (#25278197) Homepage

        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)

          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.

          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

        • 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

          • by erroneus (253617)

            That just might be the argument commercial vendors might use to discourage the use of F/OSS in government.

        • anything the tax payers pay for should be owned by the taxpayers and controlled by taxpayers as far as can be deemed appropriate.

          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)

        by Florian Weimer (88405)

        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.

        • by HBI (604924)

          Any software released by the government and not otherwise classified is in the public domain.

      • Re: (Score:3, Informative)

        by volxdragon (1297215)

        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...

      • by dwheeler (321049) on Monday October 06, 2008 @11:33PM (#25280733) Homepage Journal
        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.
        • by againjj (1132651)
          Thank you for this analysis. I agree that they really should have been clearer on this. The files imply no rights (they explicitly say "all rights reserved"), and having to dig through the other documentation to see otherwise is stupid.
      • by Sentry21 (8183)

        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.

  • by Wulfstan (180404) on Monday October 06, 2008 @05:19PM (#25277675)

    ...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?

  • a marketing attempt to sell SPARK ada tools?

  • Useless (Score:4, Insightful)

    by bluefoxlucid (723572) on Monday October 06, 2008 @05:24PM (#25277735) Journal
    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.
    • 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

      • by Bodrius (191265)

        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)

      by Talennor (612270) on Monday October 06, 2008 @05:40PM (#25277893) Journal

      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)

        by Anonymous Coward

        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)

      by kbielefe (606566) <karl.bielefeldt+ ... m ['il.' in gap]> on Monday October 06, 2008 @06:00PM (#25278099)
      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.
      • Re: (Score:1, Offtopic)

        by bytesex (112972)

        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-

      • by lindi (634828)
        procedure proc
        is
        type distance_feet is new float;
        type distance_meters is new float;
          x : distance_meters := 2.0;
          y : distance_feet;
        begin
          y := x;
        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)

        by Lost Engineer (459920) on Monday October 06, 2008 @06:42PM (#25278549)
        Any language with type checking could do that. Ada's selling point is that it's easy to make a static analysis tools for it because you can't do certain things that make static analysis hard. That could actually be said about a lot of "academic" languages as well, but Ada caught on in certain niches a long time ago and so continues to be used.
      • Re: (Score:2, Informative)

        by howardjeremy (241291)

        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)

      by A non-mouse Coward (1103675) on Monday October 06, 2008 @06:18PM (#25278325)
      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 [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.
      • by Windrip (303053)

        Formally prove resistance to XSS or XSRF and I'll listen. Until then...

      • by sjames (1099)

        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

    • by Ed Avis (5917)

      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

      • 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

        • by Ed Avis (5917)

          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)

      by Coryoth (254751)

      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

    • by KnowlerLongcloak (904607) on Monday October 06, 2008 @06:50PM (#25278629)

      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)

      by Yvanhoe (564877) on Monday October 06, 2008 @06:53PM (#25278651) Journal
      Buffer overflows are not the only security errors out there, you know. Yet it is the only one that the languages you quote prevent.
    • For a Java program, prove that it cannot possibly run out of memory. Impossible to do in a language which allows dynamic allocations.

    • by spinkham (56603)

      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.

    • by sjames (1099)

      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 ;-)

  • After Ring TFA, I still have no idea what this Tokeneer thing does. Anybody have some more details?

    Also, Ada is neat.

    • by againjj (1132651)
      It appears to be a device that is able to authenticate someone. Googling gets me:

      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)

      by owlstead (636356) on Monday October 06, 2008 @05:59PM (#25278083)

      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)

        by owlstead (636356) on Monday October 06, 2008 @06:15PM (#25278283)

        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.

        • by wacaday (1379991)

          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.

          • by owlstead (636356)

            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)

    by mihalis (28146) on Monday October 06, 2008 @05:38PM (#25277871) Homepage

    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)

      by iamhigh (1252742) *
      Can you elaborate on Ada vs. ADA? Obviously googling gets you know where fast on that one.
      • Re:Very poor summary (Score:4, Informative)

        by mihalis (28146) on Monday October 06, 2008 @06:06PM (#25278179) Homepage

        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?).

  • How'd they know I did some Token'-eer research last night?
  • 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 fo
    • by owlstead (636356)

      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

  • .. 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.
  • "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...?

  • 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'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

Some people carve careers, others chisel them.

Working...