SPARK toolsuite released under the GPL
Posted Jun 9, 2009 0:57 UTC (Tue)
by sanxiyn (guest, #44599)
[Link]
Posted Jun 9, 2009 16:42 UTC (Tue)
by AnswerGuy (guest, #1256)
[Link] (9 responses)
First observation ... these press releases an blog entries left to obscurity any links to the Praxis High Integrity Systems website. (Somewhere I found an erroneous link to praxis-his.com rather than praxis-his.co.uk which was understandably confusing) Overall this seems to be similar to the "metal level compilation" work that Dawson Engler was doing back at Stanford. (I guess this eventually became Coverity). That was originally implemented (or at least prototyped) as a set of extensions to GCC to provide support for the static code checking "annotations" (assertions about pre-conditions, invariants, and post-conditions embedded in the sources). (See also: Programming by contact). In the case of SPARK the support for these "contractual" annotations has been added to the Ada programming language (by extension of GNU Ada, gnat). From Wheeler's blog it's evident that these extensions are implemented through "magic" comments in the target's source code. This sort of "contractual annotation through magic comments" has also been used to retrofit other languages for PBC. For example: PyContract takes this approach. In Eiffel these features are an integral feature of the language. It appears that Tokeneer is a particular program being written in SPARK (i.e. using these extensions to Ada). That program is apparently a component for supporting smart cards, biometrics, and other authentication tokens. It all makes for some interesting reading. However, it would have been nice if the LWN posting for this story had provided a little more context and set the readers expectations. This is niche stuff that isn't going to be installed on your Linux box nor included in the next updates from your distribution vendor/team any time soon.
Posted Jun 10, 2009 1:17 UTC (Wed)
by vonbrand (subscriber, #4458)
[Link] (6 responses)
This sounds awfully similar to splint.
I tried (a bit) writing programs that pass its checks, and gave up (I could find no way to write linked list manipulation). Not that I tried too hard.
David A. Wheeler has a (dated) page on packages for checking source code for problems.
The basic problem is that proving anything is hard work. And as long as very few people use it, and even less are competent to hack on it, much of the advantage of open source becomes moot. Sadly.
Posted Jun 10, 2009 8:12 UTC (Wed)
by AnswerGuy (guest, #1256)
[Link] (3 responses)
splint, like RATS, is focused on parsing and scanning sources for security vulnerabilities ... and adding "magic comment" (annotations) support is somewhat optional for them. It helps them find some vulnerabilities that couldn't be statically detected without a bit of extra help.
sparse has an unfortunate name. Horrifically unfriendly in a search engine world. There's also no online documentation for it that I can find. We learn from very short blurbs that it's a source code parser but we get know sense of how advanced it may have become and whether it's actively maintained, etc. I see that it was a candidate for Google SOC (summer of code) sponsorship. But I don't see that anyone signed up for project to work on sparse.
I haven't used any of these tools. I'm primarily a sysadmin and trainer (on sysadmin focused topics). The "programming" that I do is mostly in Python or Perl ... or Bourne shell ... and thus is relatively lightweight.
I would, however, love to see some in-depth discussion of some of these tools ... with practical HOWTO and case study stories. (Perhaps a tale of how a qualified developer took $TOOL ... applied it to $PROJECT_CODE and discovered $VULNERABILITIES by running the tool and refining annotations to it.
Perhaps Jon and his associates will host a series of articles by people who are far more qualified that I am on this sort of topic. (I wonder if Valerie Aurora or Ulrich Drepper would be so inclined.
Posted Jun 10, 2009 15:57 UTC (Wed)
by JoeBuck (subscriber, #2330)
[Link] (2 responses)
If you think about it, the reason is clear: "sparse" is an adjective, and people searching for, say, sparsely populated areas or sparse matrix libraries would have to include at least two words. A one-word search has to refer to some product or program named "sparse".
Posted Jun 10, 2009 17:11 UTC (Wed)
by ballombe (subscriber, #9523)
[Link]
How is it clear ? One find only one relevant link (to http://www.kernel.org/pub/software/devel/sparse/) whose content was summarized by the grand-parent post, and does not include documentation.
Posted Jun 11, 2009 20:46 UTC (Thu)
by nix (subscriber, #2304)
[Link]
Posted Jun 10, 2009 22:31 UTC (Wed)
by Wol (subscriber, #4433)
[Link] (1 responses)
While the incompleteness theorem doesn't say this exactly, when applied to computer proofs you end up with one of three conclusions:
1 - the problem is so simple why are you using a computer?
Okay, doing a formal proof is often worth it for finding bugs, but if the client wants confirmation that the program actually works then a mathematical proof (ANY proof) is worthless.
Cheers,
Posted Jun 11, 2009 12:20 UTC (Thu)
by pjm (guest, #2080)
[Link]
Regarding conclusion 1, there are lots of properties that don't require great intellect to prove, but do require lots of mechanical operations that computers are good at and that humans make errors with. Proving that array accesses are in bounds, or that a heap invariant is always maintained, is a valuable service that a compiler or other static checker can provide. As Wol points out, automated checks (or occasionally even constructing a formal proof semi-manually) are often worth it for finding bugs (or for directing one's effort when searching for cause of a bug). For me, this means that the proof isn't meaningless. (Incidentally I don't see the connection between Gödel's incompleteness theorems and either the claim that the proof is meaningless or the claim that those three conclusions are the only possibilities.)
Posted Jun 11, 2009 4:45 UTC (Thu)
by dwheeler (guest, #1216)
[Link]
I certainly did NOT mean to omit Praxis High Integrity Systems - thanks for noting that. It's sometimes easy to "omit the obvious", unintentionally.
"Programming by contract" is certainly an old idea, but many implementations only check these conditions at run-time (PyContract is this way)... which means that if your test doesn't hit the problem case, nothing happens. If it's not THAT important when the software fails, that's fine... but if it matters, it matters. In many other cases, the 'contracts' are checked statically, but only for fairly trivial statements (e.g., X and Y are integers and they stay integers). In this case, there are actually proof-checkers to prove that more complex statements stay true.
"This is niche stuff that isn't going to be installed on your Linux box nor included in the next updates from your distribution vendor/team any time soon."... well, only partly true. Actually, I *DO* want this (and other similar tools) available in major distributions, for easy installation. We (at www.openproofs.org) already have several such tools either in distributions or in progress (such as ACL2, Frama-C, Krakatoa, etc.). They certainly aren't ready today for use on arbitrary programs; I agree that today they are pretty specialized. But that's okay, from the point of view of getting them in distros; there are lots of programs in today's distros that are specialized (for electronic circuit design, genetic research, etc.). But take the longer view. The only way to get these tools more mature is to make them easy enough to use, with examples, so that they can be used for SOME purposes (e.g., for the most critical programs). Then, using the experiences from them, work to refine the tools so that they're easier to use. Rinse, later, repeat, until they can be more broadly applied.
Posted Jun 11, 2009 13:16 UTC (Thu)
by pjm (guest, #2080)
[Link]
(Of course one should take "many properties" to mean "many very simple properties", but this is still useful: lots of correctness conditions are simple enough that a computer program can verify them.)
Regarding the extent to which we can expect this to be in free software distributions soon, it will at least to the extent that PyContract, Eiffel and Ada tools are already available in free software distributions. As David A. Wheeler wrote, the significance for most casual readers is more in its longer term effects: having this as open-source software facilitates progress in reducing bugginess in important software.
(Disclaimer: I've never used SPARK.)
Posted Jun 9, 2009 22:28 UTC (Tue)
by jordanb (guest, #45668)
[Link]
GNAT (the GNU Ada Compiler) has been getting some support for Design by Contract through Pragmas (pragma Precondition, pragma Postcondition). It's no where near as powerful as SPARK, and pragmas present some syntactic issues. There are certianly syntactic issues about SPARK too (as annotations are embedded in comments) of course, and the ideal solution would be for DbC to be fully standardized and integrated into the language as it's such a natural fit for the type of code being written in Ada. But that would take until at least the next language revision in 2015.
Posted Jun 10, 2009 14:37 UTC (Wed)
by nelzas (subscriber, #4427)
[Link] (5 responses)
Posted Jun 10, 2009 15:15 UTC (Wed)
by Los__D (guest, #15263)
[Link] (2 responses)
Posted Jun 10, 2009 15:57 UTC (Wed)
by Los__D (guest, #15263)
[Link]
I actually got my own lazy self to check out the OSI definition again, and yes: 6. No Discrimination Against Fields of Endeavor
Posted Jun 10, 2009 19:56 UTC (Wed)
by sjw (guest, #59040)
[Link]
Posted Jun 10, 2009 19:54 UTC (Wed)
by sjw (guest, #59040)
[Link] (1 responses)
If you get your GCC+Ada from the FSF, this is obviated by an extension to the license that allows
If you get GNAT GPL from AdaCore, the maintainers (www.adacore.com), this license extension is
Posted Jun 11, 2009 20:48 UTC (Thu)
by nix (subscriber, #2304)
[Link]
Not to be confused with Scanning, Parsing, and Rewriting Kit by John Aycock.
Another SPARK
SPARK is MetaL for Ada? Tokeneer is a program written in SPARK?
SPLINT
splint --- secure programmer's 'lint'
You write that "sparse" has a poorly-chosen name in a search-engine world, but you clearly didn't search for it. Google's top choice for "sparse" is, in fact, Linus's Sparse tool.
sparse: not a search-unfriendly name
sparse: not a search-unfriendly name
sparse: not a search-unfriendly name
split 's-parse', i.e. 'source parse'? I've been wondering why it was
called that and what it had to do with sparseness for some years now...
SPLINT
2 - the proof contains an error
3 - the specification is wrong
Wol
value of proving properties of software
SPARK is MetaL for Ada? Tokeneer is a program written in SPARK?
Comparisons with existing tools
SPARK toolsuite released under the GPL
SPARK toolsuite released under the GPL - license question
Does this kind of limitation is allowed by GPL? Maybe I'm wrong but I think it is allowed to develop non Free Software using GCC, so what's different here?
SPARK toolsuite released under the GPL - license question
SPARK toolsuite released under the GPL - license question
The license must not restrict anyone from making use of the program in a specific field of endeavor. For example, it may not restrict the program from being used in a business, or from being used for genetic research.SPARK toolsuite released under the GPL - license question
SPARK toolsuite released under the GPL - license question
SPARK toolkit; but since it analyses code rather than compiling it I think it's not relevant) is that any
Ada program will involve instantiating generics, the equivalent of including the library source code.
you to build proprietary software. (Similar applies to the C++ template library).
removed, in other words you can only make free software (or proprietary software that you never
distribute, of course). Don't ask me to explain why, that's just the way it is!
SPARK toolsuite released under the GPL - license question
to pay for the commercial GNAT. Seems reasonable to me: if you're going to
write proprietary software (and make people pay for it), please pay the
authors of the tools you use, first.