SPARK toolsuite released under the GPL [LWN.net]

SPARK is MetaL for Ada? Tokeneer is a program written in SPARK?

Posted Jun 9, 2009 16:42 UTC (Tue) by AnswerGuy (guest, #1256) [Link]

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.

SPLINT

Posted Jun 10, 2009 1:17 UTC (Wed) by vonbrand (subscriber, #4458) [Link]

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.

splint --- secure programmer's 'lint'

Posted Jun 10, 2009 8:12 UTC (Wed) by AnswerGuy (guest, #1256) [Link]

I know about splint and Linus' "sparse." I neglected to mention them in my comment for a couple reasons.

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.

sparse: not a search-unfriendly name

Posted Jun 10, 2009 15:57 UTC (Wed) by JoeBuck (subscriber, #2330) [Link]

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.

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

sparse: not a search-unfriendly name

Posted Jun 10, 2009 17:11 UTC (Wed) by ballombe (subscriber, #9523) [Link]

> You write that "sparse" has a poorly-chosen name in a search-engine world, but you clearly didn't search for it.

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.

sparse: not a search-unfriendly name

Posted Jun 11, 2009 20:46 UTC (Thu) by nix (subscriber, #2304) [Link]

Does it make me an idiot that I only just figured out that the name is
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

Posted Jun 10, 2009 22:31 UTC (Wed) by Wol (guest, #4433) [Link]

If problem 1 is that proving anything is hard, problem 2 is that Godel says the proof is meaningless.

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?
2 - the proof contains an error
3 - the specification is wrong

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,
Wol

value of proving properties of software

Posted Jun 11, 2009 12:20 UTC (Thu) by pjm (subscriber, #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.)

SPARK is MetaL for Ada? Tokeneer is a program written in SPARK?

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.

Comparisons with existing tools

Posted Jun 11, 2009 13:16 UTC (Thu) by pjm (subscriber, #2080) [Link]

I'd point out that there's a big difference between something like PyContract, where one tries to check a property at runtime (which often can't be done in practical time compared to the time taken for the operation whose behaviour one is checking) and SPARK/Spade which will verify many properties at compile-time, for all possible inputs (not just the few inputs it's practical to throw at your python program during whatever testing you do).

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