[cap-talk] Confessions of a C programmer

[Rob Meijer]

On Wed, September 23, 2009 08:28, David Wagner 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.)

Interesting way to look at it. I could imagine that given a specific
language (and all the pro's and cons of that language itself apparently
being equal independent of the use of a compiler or interpreter for THAT
language), choosing between compiler or interpreter with respect to
verification might involve run-time time constraints that interpreters
need to consider carefully that would be less relevant if these are payed
for in compile time.

Following this line of reasoning, a compiler could in theory verify more
relevant security properties than an interpreter if any of these
verifications are or can become CPU intensive.

Would there also be considerations that would favor an interpreter over a
compiler when looking at verifying security properties?