Brett Lymn <blymn@baesystems.com.au> 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 <http://www.cs.cmu.edu/~petel/papers/pcc/pcc.html>.

-- 
Chris

[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.
    <http://www-2.cs.cmu.edu/~necula/popl97.ps.gz>

[2] Andrew W. Appel. Foundational proof-carrying code.  In Symposium
    on Logic in Computer Science (LICS '01), pages 247--258. IEEE, 2001.
    <http://www.cs.princeton.edu/~appel/papers/fpcc.pdf>