ProofCarryingCode

• The code itself
• A specification of the security guarantees provided by the code
• A proof that the code adheres to the specification.

• http://www.cs.berkeley.edu/~necula/pcc.html

• Nec-Lee-96 G.C. Necula and P. Lee. Safe kernel extensions without run-time checking. In proocedings of the second symposium on operating systems design and implementation (OSDI'96), Seattle.http://citeseer.nj.nec.com/necula96safe.html