[cap-talk] C vs. Safety
Jonathan S. Shapiro
shap at eros-os.com
Mon Aug 11 08:42:16 CDT 2008
On Mon, 2008-08-11 at 06:08 +0100, Toby Murray wrote:
> 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.
Since KeyKOS/EROS/CapROS do not, in practice, make any added assumptions
based on static safety, the answer pragmatically would be "no".
Toby and David-Sarah are correct in concept, but mistaken in two
1. In order for the runtime layer (whether OS or VM) to make additional
assumptions, it isn't enough to know that the program is statically
checked (nor is it necessary -- see below). The VM/OS layer has to be
able to confirm that the static check occurred, and that it passed. This
is the role of the Java/CLR verifier. Another way to say this is that
the static check done at compile time is done for the convenience of the
developer, and to speed up the run-time verifier, but the check that
actually matters is the one done by the verifier (because my VM must not
trust your compiler).
2. Static typing isn't a requirement. The requirement in the discussion
that you and I have been having is memory safety, and in particular the
safety of the memory containing the security-relevant state and code of
the VMM. Safety can be achieved more efficiently by static typing, but
it can also be achieved by dynamic typing. The reason to get excited
about static typing is that it can check properties that are much more
interesting than safety.
More information about the cap-talk