Subject: Re: verified executable kernel modification committed
To: None <>
From: Christopher Richards <richards+netbsd@CS.Princeton.EDU>
List: current-users
Date: 10/29/2002 11:34:45
Brett Lymn <> writes:

> Folks,
>         First off let me say a big thanks to the people who told me
> this crazy idea was good.  Especially thanks to Jason R Fink for doing
> the hard yards and helping me out in thrashing this into the shape it
> is currently in.  I feel this code is ready enough to be useful but
> there are some aspects that can be improved on.

It would be a great advantage if the verified exec framework were
flexible enough to accommodate a variety of verification schemes.
Cryptographic hashes may be the most obvious of these, but there are
others -- Proof-Carrying Code [1, 2], for example, where execution of
a binary is permitted only if its associated proof of safety satisfies
the system proof-checker.

For an overview of PCC and mobile-code security, see Peter Lee's page
at <>.


[1] George Necula. Proof-carrying code. In 24th ACM SIGPLAN-SIGACT
    Symposium on Principles of Programming Languages, pages 106--119,
    New York, January 1997. ACM Press.

[2] Andrew W. Appel. Foundational proof-carrying code.  In Symposium
    on Logic in Computer Science (LICS '01), pages 247--258. IEEE, 2001.