Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

NSA Open Sources Tokeneer Research Project

ScuttleMonkey posted about 6 years ago | from the they-aren't-known-for-their-sharing dept.

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

Sorry! There are no comments related to the filter you selected.

ADA propaganda? (2, Informative)

etinin (1144011) | about 6 years ago | (#25277653)

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? (4, Interesting)

againjj (1132651) | about 6 years ago | (#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? (0)

Anonymous Coward | about 6 years ago | (#25278105)

It all depends on how the contract was written. Normally if the copyright isn't returned to the government the contractor retains it but transfer of copyright has to be written into the contract. By holding the copyright on this it allows the NSA to license the code however it wants. With SELinux this was originally done with a public domain license until it was merged into the Linux Kernel which then turned it GPLv2.

Re:ADA propaganda? (3, Informative)

binaryDigit (557647) | about 6 years ago | (#25278761)

Sorta. The govt is like any other entity that pays a contractor for copyrightable works. By default, the govt retains the copyright for any works done by the contractor for the govt. Some contracts can grant the contractor either limited/full or shared/exclusive rights depending on how the work is performed and who pays for what.

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? (3, Insightful)

IP_Troll (1097511) | about 6 years ago | (#25280859)

Copyright (2003) United States Government, as represented by the Director, National Security Agency. All rights reserved.

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? (0)

Anonymous Coward | about 6 years ago | (#25313303)

Who owns any of the code you use from the community ?, do you really know ?. NSA's work is open source as is the information. The owner of the linux code can pull it in too !, as anyone who writes code, you as a user/contrib of/to that code doesn't make it yours so get over it please !!!.

Re:ADA propaganda? (4, Insightful)

erroneus (253617) | about 6 years ago | (#25278197)

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:ADA propaganda? (1, Flamebait)

Actually, I do RTFA (1058596) | about 6 years ago | (#25278887)

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 copies of Vista and Office (feel free to throw out jokes about "why?" Short answer, I like security and I have Vista drivers for my hardware).

The tax payers do own it, and it is controlled by the taxpayers via their proxies in Washington/State Capital. Or sometimes, with software, the taxpayers only license some rights.

Re:ADA propaganda? (0)

Anonymous Coward | about 6 years ago | (#25280841)

I see you have admitted to liking a Microsoft product. You may have already noticed that you have been modded down.

For future posts, please refer to Windows as Winblows, Microsoft as M$!!oenELEVENTY and Office as Orifice. Also you should mention the top three things you love about Stallman.

This will help you avoid future karma hits from when Twitter & Friends get their hands on mod points.

Love, Your Friendly Neighbourhood Karma Advisor

Re:ADA propaganda? (1)

Schraegstrichpunkt (931443) | about 6 years ago | (#25283797)

Nobody sold you those Blizzard shares at gunpoint. Taxes are collected at gunpoint.

Re:ADA propaganda? (1)

collinstocks (1295204) | about 6 years ago | (#25279639)

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:ADA propaganda? (1)

erroneus (253617) | about 6 years ago | (#25279677)

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

Re:ADA propaganda? (1)

Linwooder (1228338) | about 6 years ago | (#25280153)

I wonder what it would take to get that written into law?

In an election year? About $150 million.

Re:Ada propaganda? (1)

T.E.D. (34228) | about 6 years ago | (#25284965)

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 bueracracy that often would make Daedalus hang his head in shame. Plus some code is also classified. But the biggest problem is that for code to do you any good, you have to know it exists, and not many DoD organizations promote their sources this way.

Still, I think this should be the model for any company paying for development of software. It is simply unacceptable to pay for someone else to create themselves "property", which they can then refuse to give you (or improve for you) some day.

Re:ADA propaganda? (2, Informative)

Florian Weimer (88405) | about 6 years ago | (#25278381)

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:ADA propaganda? (1)

HBI (604924) | about 6 years ago | (#25279819)

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

Re:ADA propaganda? (3, Informative)

volxdragon (1297215) | about 6 years ago | (#25279111)

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 (4, Interesting)

dwheeler (321049) | about 6 years ago | (#25280733)

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.

Re:It's open source software, and important (0)

Anonymous Coward | about 6 years ago | (#25284229)

@dwheeler:

Today I shall be the Cipher to your Neo.

I'm willing to wager VxWorks and GHS Integrity are a good bit more complicated, probably written in C, and still they jumped straight for EAL 6 and EAL 7.

The problem with this is that the product is addressing a simple problem, it is written in a verbose language, and the majority of the development activity was in support of assurance; and their only immediately claiming they could meet EAL 5.

I don't think this is a realistic situation for a good part of the industry, including those in service of the US government.

So while this might be a good example -- is it a realistic example? Can it scale well to solutions to less academic problems?

Re:It's open source software, and important (1)

againjj (1132651) | about 6 years ago | (#25288525)

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.

Re:ADA propaganda? (1)

Sentry21 (8183) | about 6 years ago | (#25281103)

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.

What is this, an ADA advertisement? (-1, Troll)

Anonymous Coward | about 6 years ago | (#25277657)

Ada is the natural choice for mission-critical, high-integrity systems due to its combination of flexibility, reliability and ease of use

Riiiight... Maybe explain exactly why no-one uses it?

The one that gets me is "ease of use"... LOL. Yeah, I think they mean "easy" like it's easy to fill out your tax forms.

Re:What is this, an ADA advertisement? (2, Interesting)

iamhigh (1252742) | about 6 years ago | (#25277811)

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

Re:What is this, an ADA advertisement? (0)

Anonymous Coward | about 6 years ago | (#25280929)

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.

Re:What is this, an ADA advertisement? (1)

Schraegstrichpunkt (931443) | about 6 years ago | (#25283813)

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.

This smells like a Slashvertisement... (4, Insightful)

Wulfstan (180404) | about 6 years ago | (#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?

Re:This smells like a Slashvertisement... (5, Funny)

PotatoFarmer (1250696) | about 6 years ago | (#25277745)

Nah. If that were the case then the summary would be more about SPARK than the project that was actually open sourced.

...

Oh, right. Carry on.

ada is easy to use (-1, Flamebait)

Anonymous Coward | about 6 years ago | (#25277691)

bahahaha

fIRST SPARKLING POST (-1, Offtopic)

Anonymous Coward | about 6 years ago | (#25277705)

HA

Re:fIRST SPARKLING POST (-1, Offtopic)

Anonymous Coward | about 6 years ago | (#25277797)

You missed. Your post is tossed into the Phail Pail.

Is this an open source announcement, or.... (0, Redundant)

stox (131684) | about 6 years ago | (#25277721)

a marketing attempt to sell SPARK ada tools?

Useless (4, Insightful)

bluefoxlucid (723572) | about 6 years ago | (#25277735)

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.

Re:Useless (0)

FrankSchwab (675585) | about 6 years ago | (#25277849)

You have a very narrow definition of "security holes".

Re:Useless (3, Insightful)

ushering05401 (1086795) | about 6 years ago | (#25277897)

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.

Re:Useless (-1, Troll)

Anonymous Coward | about 6 years ago | (#25277915)

Heh, narrow holes.

High security languages aren't CAN'T have bugs. (1)

Ungrounded Lightning (62228) | about 6 years ago | (#25277875)

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

Re:High security languages aren't CAN'T have bugs. (1)

Bodrius (191265) | about 6 years ago | (#25281295)

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 subsets / extensions of the language providing more or less comfortable definitions of 'secure'). Strong static typing and no pointer arithmetic means a duck will not turn into a dog on you - so you can trust strong pre/post conditions to a greater extent.

Provability of correctness is an objective statement. That doesn't make software magically secure - but it means it is *possible*, with enough work, to *prove* that *the part of the software you wrote* implements the security of your design *correctly*. You're still vulnerable to design gaps, and security bugs in any reused libraries / runtime - but that narrow proof of security still eliminates whole categories of end-of-the-world-scenarios from your list.

Making security bugs 'easier to avoid' - like other 'bug preventing language features' - is a much more subjective claim (how do you define a 'security bug' for such a claim anyway?), and is what can backfire into non-sensical assumptions. They're typically a net gain int he hands of an informed developer, but naive programmers can be misled that because a very specific type of security bug X 'cannot happen' in the language, 'security' is taken care of.

Re:Useless (3, Insightful)

Talennor (612270) | about 6 years ago | (#25277893)

Don't say I can't make security holes in Java.

I can make security holes in whatever language I want! Really.

Re:Useless (1, Funny)

Anonymous Coward | about 6 years ago | (#25278131)

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

kbielefe (606566) | about 6 years ago | (#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:Useless (0, Offtopic)

bytesex (112972) | about 6 years ago | (#25278395)

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:Useless (1)

lindi (634828) | about 6 years ago | (#25278443)

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 (3, Insightful)

Lost Engineer (459920) | about 6 years ago | (#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.

NASA (0)

Anonymous Coward | about 6 years ago | (#25279069)

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.

Re:Useless (0)

Anonymous Coward | about 6 years ago | (#25279127)

type mismatch? isn't that in pretty much every compiler? A C++ compiler would give you an error if you tried to convert an instance of the Meters class to Feet with no defined conversion operator. Any type-safe language can do this.

Re:Useless (2, Insightful)

GXTi (635121) | about 6 years ago | (#25280901)

The problem is, as always, with the humans: when was the last time you saw an actual application that used instances for scalar dimensions? I've never seen one, because the laziest (and therefore most productive) thing to do is to use a bare integer and just agree on what unit system to use.

Re:Useless (1)

pjt33 (739471) | about 6 years ago | (#25283611)

I'm working on one right now, and I wrote the dimensions framework for it. If you can agree on the unit system then that's great, but when the spec mixes units then the sensible thing to do is to encapsulate it properly so that everyone is forced to be explicit about their units.

Re:Useless (2, Informative)

howardjeremy (241291) | about 6 years ago | (#25282095)

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 (5, Informative)

A non-mouse Coward (1103675) | about 6 years ago | (#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.

Re:VERIFICATION (1)

Windrip (303053) | about 6 years ago | (#25289707)

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

Re:VERIFICATION (0)

Anonymous Coward | about 6 years ago | (#25296309)

...shite...

You misspelled Shiite. That's OK, though, this is Slashdot, we don't expect you to be able to spell words correctly.

Re:VERIFICATION (1)

sjames (1099) | about 6 years ago | (#25303525)

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 somewhere between reluctant and unwilling to allow adequate time to define the problem and do a high level design overview before demanding a time estimate (and is fairly likely to add features and remove alloted time) we're not going to see formal validation in wide use any time soon. Possible exceptions may be the lower layers of code operating a nuclear plant, airliner, or medical equipment.

Re:Useless (1)

Ed Avis (5917) | about 6 years ago | (#25278405)

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 should therefore not try to do anything.

Re:Useless (1)

bluefoxlucid (723572) | about 6 years ago | (#25280205)

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 programmer but I've got the same stuff from regular .NET programmers. The virtual machine is secure to the point that you can't get it to alter virtual machine bytecode (CIL or Java assembly) because if you do, the VM will have a fit and abort. The security manager makes it impossible to access anything the application shouldn't (random files etc). Given languages simply don't let you do anything that leads to malicious code execution, at all; the worst someone can do is find a very banal bug, like getting a calculation to come out off and produce strange and interesting but harmless effects.

I've heard it from marketing, I've heard it from professors, I've heard it from simple programmers. It's always wrong. Yes you can make the language not bug out on stupid stuff like in C; but you can't make air tight security that way. No amount of marketing makes it work that way (see Todd Davis).

Re:Useless (1)

Ed Avis (5917) | about 6 years ago | (#25280759)

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 weenies, but please don't feel you have to repeat the obviously bogus arguments they trot out.

I completely agree that not trampling memory on buffer overruns is not enough for airtight security. But it is a necessary bare minimum! To make a secure app you at least need to get the basic stuff right, and any help the computer can give you for that is welcome. If you look at the typical security holes _still_ being discovered in software (in 2008, for goodness' sake) you will see that buffer overruns and bad pointer accesses represent a good chunk. If you're a perfect programmer you don't need any assistance from the compiler or runtime and C is just fine for you. Sadly, most programmers are all too fallible. I know I am, and I would never trust myself to get details like buffer length checking correct when I can get the computer to do that for me.

Can Java or C# eliminate all security holes? Of course not! Are they suitable languages for 100% of programs? Nope. Can they often help you automatically take care of the low-level stuff, so you can spend your precious and limited brainpower on something else? Damn right they can!

Re:Useless (2, Informative)

Coryoth (254751) | about 6 years ago | (#25278587)

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 [jmlspecs.org] and ESC/Java2 [kind.ucd.ie] which provide similar (though not quite as powerful) facilities for Java.

A Security Hole in Java (4, Informative)

KnowlerLongcloak (904607) | about 6 years ago | (#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:A Security Hole in Java (-1, Redundant)

Anonymous Coward | about 6 years ago | (#25282627)

Just use prepared statments to get rid off SQL Injection security holes.

Re:Useless (3, Insightful)

Yvanhoe (564877) | about 6 years ago | (#25278651)

Buffer overflows are not the only security errors out there, you know. Yet it is the only one that the languages you quote prevent.

Re:Useless (1)

Profane MuthaFucka (574406) | about 6 years ago | (#25279851)

For a Java program, prove that it cannot possibly run out of memory. Impossible to do in a language which allows dynamic allocations.

Re:Useless (0)

Anonymous Coward | about 6 years ago | (#25283849)

How you can assure correctness of the Java WM?
How about validated compilers (and run-time environments) for Java, C#, and VB.NET?
Are there any tools that perform a formal analysis of the source code? What about the hardware resources to run these things on?

Re:Useless (1)

spinkham (56603) | about 6 years ago | (#25288235)

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:Useless (1)

sjames (1099) | about 6 years ago | (#25303049)

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? (1)

friedo (112163) | about 6 years ago | (#25277815)

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

Also, Ada is neat.

Re:Tokeneer? (1)

againjj (1132651) | about 6 years ago | (#25277965)

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? (4, Informative)

owlstead (636356) | about 6 years ago | (#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? (4, Informative)

owlstead (636356) | about 6 years ago | (#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.

Re:Tokeneer? (1)

wacaday (1379991) | about 6 years ago | (#25282655)

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:Tokeneer? (1)

owlstead (636356) | about 6 years ago | (#25291647)

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 do with the user interface.

Even then you are on questionable ground: with any actual PC software you will rely on libraries. Going for EAL 7 seems to be a waste of resources to me.

Re:Tokeneer? (0)

Anonymous Coward | about 6 years ago | (#25283919)

Semi-formal means consistent. It's not difficult to produce consistent documentation. A picture which uses a consistent legend. A series of statements that use a "must" and "may" statements. It might not be part of your development process, and that's one aspect of how CC works, it declares certain practices that you ought to do, sort of like CMMI. As you approach higher assurance levels, formal becomes a requirement, and that is certainly more challenging to produce, and it is even less likely that your development already encompasses this, unless you are engineering a weapons control system or medical device. There are not many EAL 5 certified products, but the number of products at EAL 5 and higher is slowly rising.

This entire Tokeneer project is indeed very simple: just under 10,000 lines of code. Knowing Ada to be a pretty verbose language, this means not very much functionality is encompassed. It also seems the majority of time on this project was spent doing non-coding development activities:

        * lines of code: 9939
        * total effort (days): 260
        * productivity (lines of code per day, overall): 38
        * productivity (lines of code per day, coding phase): 203

As Linus Torvalds once said, "Yes, you can have crazy ideas in both schedulers and security... [T]he *discussion* on security seems to never get down to real numbers. So the difference between them is simple: one is hard science. The other one is people wanking around with their opinions.'"

How many times can you re-write 10,000 lines of code in 260 days in your language of choice?

Re:Tokeneer? (0)

Anonymous Coward | about 6 years ago | (#25284091)

As someone who is in security and knows about Common Criteria, you must also know that a high EAL nearly nothing about the functional security of the product being evaluated. The vendor defines the Security Target, and the EAL is the degree to which it does the things the ST says it does. That's it. The main benefit of EAL 5 level testing in the US is the involvement of NSA penetration testing teams, but this tends to be a time consuming exercise.

There are other EAL 5 and higher products, which I am certain are comprised of much more complicated software than this, likely written in C, and very likely without formal verification tools. This product allegedly *could* achieve a given EAL, but it is unclear that it achieved ANY evaluation. This is because CC is expensive and time consuming.

As someone who is in security and knows about the CC, the fact that NSA and some vendor says it's possible to EAL 5 evaluate a 10K LOC product that does not do much of anything, really doesn't surprise or impress me at all. It's another academic project. Not that academic projects are all bad -- but where's the application?

In Soviet Amerika, (-1, Offtopic)

Anonymous Coward | about 6 years ago | (#25277825)

Tokeneer Research Project open YOU [keatingeconomics.com] .

Very poor summary (5, Insightful)

mihalis (28146) | about 6 years ago | (#25277871)

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:Very poor summary (2, Interesting)

iamhigh (1252742) | about 6 years ago | (#25278025)

Can you elaborate on Ada vs. ADA? Obviously googling gets you know where fast on that one.

Re:Very poor summary (3, Informative)

mihalis (28146) | about 6 years ago | (#25278179)

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:Very poor summary (1)

iamhigh (1252742) | about 6 years ago | (#25278201)

WHOOSH!

I thought you actually meant there was a different language Ada vs ADA!!!! It's late in the day.

Re:Very poor summary (1)

mihalis (28146) | about 6 years ago | (#25278319)

Yes, thankfully there is no programming language called "ADA" :)

Re:Very poor summary (1)

stonemetal (934261) | about 6 years ago | (#25279421)

It would be like pulling teeth.

Re:Very poor summary (1)

iamhigh (1252742) | about 6 years ago | (#25321511)

Horrible, just horrible.

I love it!

Re:Very poor summary (1)

againjj (1132651) | about 6 years ago | (#25278565)

Actually, Augusta Ada King, Countess of Lovelace, generally known as Ada Lovelace [wikipedia.org] , born Augusta Ada Byron, wrote for Charles Babbage's Analytical Engine.

Re:Very poor summary (1)

mihalis (28146) | about 6 years ago | (#25285495)

Right, my mistake.

Re:Very poor summary (1)

mortonda (5175) | about 6 years ago | (#25278749)

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 (1)

Corpuscavernosa (996139) | about 6 years ago | (#25277873)

How'd they know I did some Token'-eer research last night?

Ada=great language (0)

Anonymous Coward | about 6 years ago | (#25277963)

While this example is not particularly interesting, Ada is really a veryn good language and much more secure than what is commonly used.

More copy and paste please (0, Redundant)

Gothmolly (148874) | about 6 years ago | (#25277999)

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

Re:More copy and paste please (-1, Flamebait)

Zerth (26112) | about 6 years ago | (#25278251)

Ada is also the natural choice for open-sourcing software you don't want anyone to look at, try to use, or care about.

It avoids those drawn to the readability challenges of perl, stays outside the sanity requirements of brainfuck, avoids the in-joke uselessness of languages such as LOLCODE, and it was designed by enough committees with contrary goals and skillsets so as to hold no particular value to anyone.

In short, Ada is the perfect government language. Everyone GS13 and up will be learning it as a spoken language and future laws will be written in it. Despite the above, this will probably be an improvement.

Claim of formal verification too grand (1)

lemaymd (801076) | about 6 years ago | (#25278175)

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

Re:Claim of formal verification too grand (1)

owlstead (636356) | about 6 years ago | (#25278507)

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 user manuals etc).

Some idea of the SPARK code, this is matched with the Z code as far as I understood.

pre ( ( Latch.IsLocked(Latch.State) and
                  Door.TheCurrentDoor(Door.State) = Door.Open and ...
post ( ( Latch.IsLocked(Latch.State) and
                  Door.TheCurrentDoor(Door.State) = Door.Open and
                  Clock.GreaterThanOrEqual(Clock.TheCurrentTime(Clock.CurrentTime),
                                                                    Door.prf_alarmTimeout(Door.State)) )

Some stuff cut because of
"Filter error: Please use fewer 'junk' characters."
says it all really :)

mo3 3own (-1, Offtopic)

Anonymous Coward | about 6 years ago | (#25278183)

and the Bazzar So that their Ass of them all, Assholes, as they Create, manufacture filed countersuit, The mobo blew departures of And the striking than a fraction

Tokeneer has been written in SPARK Ada... (1, Interesting)

hAckz0r (989977) | about 6 years ago | (#25278401)

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

A challenge? (1)

HTH NE1 (675604) | about 6 years ago | (#25278691)

"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? (1)

EWAdams (953502) | about 6 years ago | (#25279013)

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. (1)

Animats (122034) | about 6 years ago | (#25281971)

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

Which Ada are they talking about? (0)

Anonymous Coward | about 6 years ago | (#25289881)

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.

Check for New Comments
Slashdot Login

Need an Account?

Forgot your password?