Proof-carrying code
Appearance
Proof-Carrying Code is a software mechanism that allows a host system to verify properties about an application via a safety proof that accompanies the application. The host system can compare the conclusions of the safety proof to its own security policy to determine whether the application is safe to execute. This can be particularly useful in prevent buffer overflows and other vulnerabilities common in some programming languages.
References
- George C. Necula & Peter Lee, Proof-Carrying Code. Technical Report CMU-CS-96-165, November 96. (62 pages)