Proof-Carrying Code

Proof - Carrying Code (PCC ) is a 1996 by George Necula and Peter Lee developed, efficient algorithm for computer, with the aid of the characteristics of application software and in particular compliance can be checked and verified by security policies.

The automatic algorithm uses an axiom system to analyze the program code accompanying metadata. It can be concluded, ensuring that certain security-relevant criteria are met. Then no additional appropriate measures must be taken at run time, such as exception handling at critical behavior of the software. Proof - Carrying Code is also particularly useful to ( for example, type of injury, overloading, or polymorphism ) to prevent security vulnerabilities, such as buffer overflows or ambiguities, which are often caused by the use of inadequate languages.

The Proof - Carrying Code, the reliability and trustworthiness of a source program are reviewed in a computer network to a client during the installation and execution of computer programs. This metadata is retrieved from the host, called the program code producer, with the help of the verification on the client, called the program code consumer, can take place.