Proof Carrying Code
Proof-Carrying Code is a promising technique, developed on the seminal
work of Necula
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
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
Proof Carrying Code benefits from a number of distinctive features that make it
a very appropriate basis for security architectures for global
- 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.