Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a

formal proof In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the seq ...

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 Security policy is a definition of what it means to ''be secure'' for a system, organization or other entity. For an organization, it addresses the constraints on behavior of its members as well as constraints imposed on adversaries by mechanisms ...

to determine whether the application is safe to execute. This can be particularly useful in ensuring

memory safety safety is the state of being protected from various software bugs and security vulnerabilities when dealing with memory access, such as buffer overflows and dangling pointers. For example, Java is said to be memory-safe because its runtime error ...

(i.e. preventing issues like

buffer overflows In information security and programming, a buffer overflow, or buffer overrun, is an anomaly whereby a program, while writing data to a buffer, overruns the buffer's boundary and overwrites adjacent memory locations. Buffers are areas of memor ...

). Proof-carrying code was originally described in 1996 by

George Necula George Ciprian Necula is a Romanian computer scientist, engineer at Google, and former professor at the University of California, Berkeley who does research in the area of programming languages and software engineering, with a particular focus on ...

and Peter Lee.

Packet filter example

The original publication on proof-carrying code in 1996Necula, 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 filter In computing, a firewall is a network security system that monitors and controls incoming and outgoing network traffic based on predetermined security rules. A firewall typically establishes a barrier between a trusted network and an untrusted n ...

s 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 In computer science, hierarchical protection domains, often called protection rings, are mechanisms to protect data and functionality from faults (by improving fault tolerance) and malicious behavior (by providing computer security). Compute ...

, 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 ...

for packet filtering, inserting checks on each memory access ( software fault isolation), 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 example, will not access memory outside of the packet and its scratch memory area. A theorem prover is used to show that the machine code satisfies this policy. The steps of this proof are recorded and attached to the machine code which is given to the kernel program loader. The program loader can then rapidly validate the proof, allowing it to thereafter run the machine code without any additional checks. If a malicious party modifies either the machine code or the proof, the resulting proof-carrying code is either invalid or harmless (still satisfies the security policy).

References

* George C. Necula and Peter Lee
''Proof-Carrying Code''
Technical Report CMU-CS-96-165, November 1996. (62 pages) * George C. Necula and Peter Lee.
''Safe, Untrusted Agents Using Proof-Carrying Code''
Mobile Agents and Security, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlin, {{ISBN, 3-540-64792-9, 1998. * George C. Necula.
Compiling with Proofs
'. PhD thesis, School of Computer Science, Carnegie Mellon Univ., Sept. 1998. Computer security Dependently typed programming Formal methods Programming language theory

Packet filter example

See also

References