Re: PolySpace?

From: Crispin Cowan (crispin@wirex.com)
Date: 12/12/01 

Date: Tue, 11 Dec 2001 15:04:28 -0800
From: Crispin Cowan <crispin@wirex.com>
To: Ryan Russell <ryan@securityfocus.com>

Ryan Russell wrote:

>http://www.polyspace.com/
>
>Now there are some ambitious claims. Anyone tried this?
>
Note that this claim "The first product to automatically detect 100% of
run-time errors at Compilation Time" is not quite as goofy as it sounds.
You can prove that a program will not incur any run-time exceptions at
compile time. With a few caveats:

    * You cannot prove whether the program will halt or not (Turing's
      "Halting Problem"). You can only prove that, while the program is
      running, it will not perform a set of defined "bad things". More
      precisely, you prove that the program will only do a set of
      predefined "good things" (well-defined operations) and the
      corrolary falls out :-)
    * You must use a strongly typed programming language, or you won't
      be proving very much. For example, C programs that do arithmetic
      on void * pointers and then write back to them can have arbitrary
      failure modes.
    * "No runtime exceptions" really means "no undefined behavior." You
      will still see programs die on failures like "disk full", or
      "memory exhausted", but they will be well-defined exception
      handlers, not seg faults.
    * The claim of "The first" is outright wrong, as at least one
      previous system has done this. Hermes
      http://www.idiom.com/free-compilers/TOOL/Hermes-1.html is my
      favorite strongly typed programming language, and one of it's
      prominent features was that, in principle, programs that get
      passed the compiler's "Typestate" checker would not suffer
      run-time exceptions. Unfortunately, Hermes died and is not really
      available anymore. Fortunately, the papers are available
      http://citeseer.nj.nec.com/lalis94hermes.html and
      http://citeseer.nj.nec.com/context/283272/0 and the Java designers
      showed good taste in what they stole from :-) Java incorporates
      some of the Typestate features into the compiler and the bytecode
      verifier.

Disclaimer: I worked for the Hermes authors (Rob Strom, Shaula Yemini,
Josh Auerbach) at the IBM Watson lab back in 1991 and 1992 when some of
this stuff was coming out.

Crispin 

-- 
Crispin Cowan, Ph.D.
Chief Scientist, WireX Communications, Inc. http://wirex.com
Security Hardened Linux Distribution:       http://immunix.org
Available for purchase: http://wirex.com/Products/Immunix/purchase.html