[cap-talk] C vs. Safety

[Toby Murray]

On Mon, 2008-08-11 at 00:26 +0000, Baldur Johannsson wrote:
> so is an KeyKos domain (the 2nd vm in your example)
> running an staticly type checked program more safe and secure than an
> domain that is just running an program that hasnt been subjected to
> static type checking?
> If yes then why?

Yes it is necessarily "more secure" in that we can make more assumptions
about how it will behave.

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. Now
the nature of those theorems will depend on the type system. 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" ;).