[cap-talk] Confessions of a C programmer

[Bill Frantz]

daw at cs.berkeley.edu (David Wagner) on Tuesday, September 22, 2009 wrote:

>Bill Frantz  wrote:
>> Languages with a run-time interpreter, such as Java, have the issue of
>> verifying what is usually a fairly large C program.
>
>On the other hand, compiled languages have the issue of verifying what
>is usually a fairly large program (the compiler).  I'm not sure there is
>necessarily a big win for compiled languages over interpreted languages.
>Either way, you are relying on the compiler/interpreter and the associated
>runtime libraries and related infrastructure.  It's pretty rare to see
>those formally verified, no matter what language you use, so in practice
>almost any language involves relying upon a large, unverified program.
>(Now there might be reasons why that program is more trustworthy in
>some cases than others, to be sure.)

(Hehe) And probably the easiest "compiler" to verify is an assembler, since
the output is directly related to the input. Of course you lose portability
and memory safety, although Norm wrote some ideas for verifying machine
code in <http://cap-lore.com/Software/CodeProof/>.

If one could verify some useful static properties of machine code, and run
the verifier in a way that it could not modify the code being verified, you
might end up with smallest development system to verify. Just a thought.

Cheers - Bill

---------------------------------------------------------------------------
Bill Frantz        |"We used to quip that "password" is the most common
408-356-8506       | password. Now it's 'password1.' Who said users haven't
www.periwinkle.com | learned anything about security?" -- Bruce Schneier