Proofs of Safety for Untrusted Code

Proof-carrying code is a technique that can be used to execute untrusted code safely. A code consumer specifies requirements and safety rules which define the safe behavior of a system, and a code producer packages each program with a formal proof that the program satisfies the requirements. The consumer uses a fast proof validator to check that the proof is correct, and hence the program is safe. In this report, we discuss applications for which proof-carrying code is appropriate, explain the mechanics of proof-carrying code, compare it with other security techniques and propose research directions for the method.Pre-2018 CSE ID: CS1999-063