Safe, Untrusted Agents Using Proof-Carrying Code

PCC Charactristics

1. General
2. Low-risk & automatic
3. Efficient
4. Don't need to trust code producer
5. Flexible

Components

The code and annotations are sent to a parser, which generates IL to be executed in a symbolic evaluator. The symbolic evaluator derives a predicate and asks an untrusted prover to solve it. The proof is encoded in Edinburgh Logical Framework. A type of proof is type checked means proving the right predicate.

Gadgets

• Invariant annotation is the most important one
• Their security policy: safe read/write; execution time bounded