Proof-Carrying Code

from Wikipedia, the free encyclopedia

Proof-Carrying Code (PCC) is an efficient algorithm for computers developed by George Necula and Peter Lee in 1996 , with the help of which the properties of application software and, in particular, compliance with security guidelines can be checked and verified.

The automatic algorithm uses a system of axioms to analyze metadata accompanying the program code . It can be concluded and guaranteed that certain safety-relevant criteria are met. To maturity no appropriate additional measures must be taken then, for example, the exception handling in critical behavior of the software. Proof-carrying code is also particularly useful to prevent security vulnerabilities such as buffer overflows or ambiguities ( e.g. type violation , overloading or polymorphism ), which are often caused by the use of inadequate programming languages .

With the proof-carrying code, the reliability and trustworthiness of a program source in a computer network can be checked on a client during the installation and execution of computer programs . Metadata is retrieved from the host , the so-called program code producer, with the help of which the check can take place on the client, the so-called program code consumer.

Web links

  • George C. Necula and Peter Lee: Safe, Untrusted Agents Using Proof-Carrying Code , Mobile Agents and Security, Giovanni Vigna (editor), Lecture Notes in Computer Science, Volume 1419, Springer-Verlag, Berlin, ISBN 3-540-64792 -9 , 1998
  • George C. Necula: Compiling with Proofs (PDF; 1.6 MB) . PhD thesis, School of Computer Science, Carnegie Mellon University, September 1998
  • Proof-Carrying Code in the MOBIUS project