Proofs of Safety for Untrusted Code
Skip to main content
Open Access Publications from the University of California

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-0633

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View