Jump to content

Proof-carrying code

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Cctoombs (talk | contribs) at 03:54, 2 February 2006 (Added references). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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)