[cap-talk] C vs. Safety

[Jonathan S. Shapiro]

On Mon, 2008-08-11 at 06:08 +0100, Toby Murray wrote:
> I've heard it said by one of the PL people that in type-checking your
> program you're essentially proving lots of little theorems about it.

Yes. And when this is done in a system based on dependent kinds, those
theorems need not be so little. At that point, your running all of the
power of something like the TWELF prover!

> But having
> proved *anything* at all about your program means that it's behaviour is
> less unknown than what it was before. So I'd answer your question with
> "Yes, it's more secure. But in what ways are hard to quantify" ;).

I disagree. They are very easy to quantify. You know because you know
what property you proved. My quibble is that the property in question
may or may not be relevant to security.

In the case of static type checking, the property you have proved is
that the security enforcing and security relevant portions of the
runtime system are not manipulable by the program, except through the
designated interfaces (which, presumably, are implemented by the VMM
author on the assumption that the program should be treated with
suspicion).

Aside: this is true up to memory integrity, which we usually take for
granted, but which we probably should not.


shap