Re: Proof-Carrying Code Mark S. Miller (markm@caplet.com)
Wed, 08 Dec 1999 22:24:08 -0800

At 09:19 AM 12/6/99 , Paul E. Baclace wrote:
>I just ran across this...thought you might be interested:
>
>http://foxnet.cs.cmu.edu/afs/cs.cmu.edu/project/fox/mosaic/people/petel/papers/pcc/pcc.html

Thanks Paul, I'd come across PCC before, but this message got me to take a closer look. Thanks. I'm taking the liberty of cc'ing this response to the e-lang list

Since E is already a safe/secure simple language (as is Trusty Scheme), I don't need PCC for basic safety. There are two ways I can see where PCC might fit into the future of E:

  1. If A wants B not to compile A's E code to Java bytecodes (or whatever instructions) before running them on B's platform, but rather wants B to run A's pre-compiled code, it suffices for A to provide an E source parse tree, the compiled target, and a proof that the target is a valid compilation (describes the same computation) as the source. The cool thing is, the PCC issue of "what is the kernel's security policy?" that the proof must satisfy is, for us, always simply equivalence with an E source program, since E already defines all the remaining "kernel security policy" issues.
  2. As an extension of the auditor technique. Right now, all my auditors, like "confined", prove simple enough properties that they always perform this proof directly on the un-augmented source parse tree. However, we have already run across the fascinating case http://eros.cis.upenn.edu/~majordomo/e-lang/1076.html of MarcS's fully unprivileged implementation of sealer/unsealer pairs, which behaves in a confined fashion, but necessarily violates the properties any simple confinement auditor would use to prove confinement. In this case, we can (and will) solve the problem by adopting MarcS's code into the TCB, and causing it to be recognized as confined by decree. However, this is a dangerous kind of move that must be used very rarely, and can only be used by us TCB designers, and not by our users.

Were the "confined" auditor to be a PCC consumer, and were the notion of "confinement" stated as an abstract property, such that it were possible to prove that MarcS's code is actually confined, then MarcS, without privilege, could contribute his code to other's E systems along with a proof, constructed by MarcS, that this code satisfies the abstract confinement property.

Needless to say, if this is in E's future, it's not the immediate future. It all adds value, but none of it is required to meet E's goals. I'd rather wait until there is more software engineering experience actually using PCC in Scheme- or ML-like languages before diving in. Of course, E is open source, so if anyone else wants to experiment with it along these lines, feel free, and we'd love to hear about it! 

         Cheers,
         --MarkM