Subject: Re: verified executable kernel modification committed
To: None <email@example.com>
From: Christopher Richards <richards+netbsd@CS.Princeton.EDU>
Date: 10/29/2002 11:34:45
Brett Lymn <firstname.lastname@example.org> writes:
> 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
 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.
 Andrew W. Appel. Foundational proof-carrying code. In Symposium
on Logic in Computer Science (LICS '01), pages 247--258. IEEE, 2001.