Proof Carrying Code

Proof-Carrying Code is a promising technique, developed on the seminal work of Necula and Lee. In its more general sense, PCC provides a mean to establish trust in a mobile code infrastructure, by requiring that mobile code is sent along with a formal proof, a.k.a. certificate, showing its adherence to a property agreeable by the code consumer. This verifiable evidence may involve adherence to appropriate policies, such as safety, security, or functionality.

PCC has many uses in systems whose trusted computing base is dynamic, either because of mobile code or because or regular bug fixes or updates. Examples include, but are not limited, to extensible operating systems, Internet browsers capable of downloading code, active network nodes and safety-critical embedded controllers.

Proof Carrying Code benefits from a number of distinctive features that make it a very appropriate basis for security architectures for global computers:

• Proof Carrying Code is based on verification rather than trust. Indeed, Proof Carrying Code focuses on the behavior of downloaded components rather than on the origin of such components. In particular, it does not require the existence of a global trust infrastructure.
• Proof Carrying Code is transparent for end users. While Proof Carrying Code builds upon ideas from program verification, which in its full generality requires interactive proofs, the PCC architecture does not require the code consumers to build proofs. Rather, it requires code consumers to check proofs, which is fully automatic.
• The principle of Proof Carrying Code is general. The only restriction on the security policy is that it should be expressible in the formal logic, which is often very expressive. Besides, the basic principles of Proof Carrying Code apply to any logic.
• The Proof Carrying Code architecture is flexible and configurable as it can be used for different policies. In particular, the VC Generator and the proof checker are independent of the policy, while the certifying compiler can in principle be adapted to different safety properties.
• Proof Carrying Code technology does not sacrifice performance to security as it advocates for static verification at compile-time, and therefore does not incur in the overhead cost inherent to dynamic techniques based on monitoring.

Standard PCC builds upon several elements:

• A formal logic for specifying and verifying policies. The specification language is used to express requirements on the incoming component, and the logic is used to verify that the component meets the expected requirements.
• A verification condition generator (VC Generator). The VC Generator produces, for each component and safety policy, a set of proof obligations whose provability will be sufficient to ensure that the component respects the safety policy.
• A formal representation of proofs (Certificates). Certificates provide a formal representation of proofs, and are used to convey to the code consumer easy-to-verify evidence that the code it receives is secure.
• A proof checker that validates certificates against specifications. The objective of a proof checker is to verify that the certificate does indeed establish the proof obligations generated by the VC Generator.

One fundamental issue to be addressed by any practical deployment of logic-based PCC is the generation of certificates. If logic-based certificates are to be used to verify basic safety properties of code, and it is expected that large classes of programs carry a certificate, then it is important that certificates are generated automatically. Certifying compilers extend traditional compilers with a mechanism to generate automatically certificates for sufficiently simple safety properties, exploiting the information available about a program during its compilation to produce a certificate that can be checked by the proof checker. Note that the certifying compiler does not form part of the TCB; nevertheless, it is an essential ingredient of PCC, since it reduces the burden of verification on the code producer side. An early example of certifying compiler is the Touchstone compiler, which was intended to explore the feasibility of the pioneer research on PCC. This compiler generates a formal proof for type-based safety and memory safety of the resulting program in DEC Alpha assembly language. The Touchstone compiler automatically inserts the loops invariants in the resulting program and generated the correctness proofs. The counter part of this approach is that the ensured properties are deliberately restricted to simple type-safety properties.