Jump to content

Proof-carrying code

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by 221.6.69.10 (talk) at 07:43, 10 April 2006. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Proof-Carrying Code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can compare the conclusions of the proof to its own security policy to determine whether the application is safe to execute. This can be particularly useful in ensuring memory safety (i.e. preventing buffer overflows), and other vulnerabilities common in some programming languages.


References

  • George C. Necula and Peter Lee. Proof-Carrying Code. Technical Report CMU-CS-96-165, November 96. (62 pages)
  • George C. Necula and Peter Lee. Safe, Untrusted Agents Using Proof-Carrying Code. Mobile Agents and Security, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlin, ISBN 3-540-64792-9, 1998.
  • George C. Necula.

Compiling with Proofs. PhD thesis, School of Computer Science, Garnegie Mellon Univ., Sept. 1998.

Stub icon

This programming-language-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Proof-carrying_code&oldid=47770775"