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 quickly verify the validity of the proof, and it 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 issues like
buffer overflows).
Proof-carrying code was originally described in 1996 by
George Necula and
Peter Lee Peter Lee may refer to:
*Peter Lee (bishop of Christ the King) (born 1947), England-born Anglican bishop, working in South Africa
*Peter Lee (bishop of Virginia) (born 1938), American bishop of the Episcopal Church
*Peter Lee (chess player) (born 19 ...
.
Packet filter example
The original publication on proof-carrying code in 1996
[Necula, G. C. and Lee, P. 1996. Safe kernel extensions without run-time checking. SIGOPS Operating Systems Review 30, SI (Oct. 1996), 229–243.] used
packet filters as an example: a user-mode application hands a function written in machine code to the kernel that determines whether or not an application is interested in processing a particular network packet. Because the packet filter runs in
kernel mode, it could compromise the integrity of the system if it contains malicious code that writes to kernel data structures. Traditional approaches to this problem include interpreting a
domain specific language
A domain-specific language (DSL) is a computer language specialized to a particular application domain. This is in contrast to a general-purpose language (GPL), which is broadly applicable across domains. There are a wide variety of DSLs, ranging f ...
for packet filtering, inserting checks on each memory access (
software fault isolation
In computer security, a sandbox is a security mechanism for separating running programs, usually in an effort to mitigate system failures and/or software vulnerabilities from spreading. The isolation metaphor is taken from the idea of children w ...
), and writing the filter in a high-level language which is compiled by the kernel before it is run. These approaches have performance disadvantages for code as frequently run as a packet filter, except for the in-kernel compilation approach, which only compiles the code when it is loaded, not every time it is executed.
With proof-carrying code, the kernel publishes a security policy specifying properties that any packet filter must obey: for exa