Proof-Carrying Code¶

A code-admission method in which an untrusted producer supplies executable code with a formal proof that the consumer checks against its policy for that received code.

Version: v1 · 2026-10-03 · History
Domain-specific #: 13527
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomains: Computer Security, Formal Methods → Computer Science & Software Engineering

Core Idea¶

Proof-carrying code (PCC) lets an untrusted producer send an executable with a formal proof that the code consumer can check before running it. The consumer fixes a safety policy and computes the obligation for the code it actually receives; the producer's certificate must prove that obligation. The result is policy-relative admission, not a blanket claim of secure code or a trusted statement about its author. Proof construction can be hard and producer-side; checking is intended to be simpler and consumer-side.[^{ref-7d64bce65649][}ref-80d4e3370804][^ref-80d4e3370804-2]

The conclusion depends on a sound policy and machine model, correct verification-condition generation and proof checking, valid calling assumptions, and execution of the same code that was checked. Editing code before checking may fail validation or produce another policy-compliant program with a valid proof; editing code after checking is not covered by that validation.[^{ref-80d4e3370804-2][}ref-8510aeef79b3]

Scope of Application¶

Necula and Lee's original prototype certified native packet filters that run inside an operating-system kernel. Its policy restricted reads and writes, branch direction and preserved registers under a valid kernel calling precondition; validation happened at admission rather than at each filter operation.[^ref-80d4e3370804-3] Their later mobile-agent experiment applied the same architecture to agents accessing an airfare database, with record-access levels and instruction/network resource bounds. This was an experiment, not a production-deployment claim.[^{ref-5fdf2d654b95][}ref-8510aeef79b3]

PCC does not replace every runtime check or authenticate a sender. It also is not the same as ordinary local formal verification, bytecode verification or signed code: the distinctive event is a producer-shipped proof checked against the consumer's own predicate for its received executable.[^{ref-80d4e3370804-2][}ref-8510aeef79b3]

Clarity¶

Ask what code the receiver will execute, what policy it requires, how that code generates an obligation, and whether the accompanying proof discharges that obligation. A proof about a source file or some earlier binary is insufficient unless it is soundly tied to the actual executable. “Tamperproof” here means only that the checked received bundle must prove the stated policy, conditional on sound machinery and no post-check change; it is not ongoing integrity monitoring.[^{ref-80d4e3370804][}ref-80d4e3370804-2]

Manages Complexity¶

PCC shifts proof search to the code supplier and leaves the receiving host with a bounded validation task. That can make sense for frequently run kernel filters: a one-time check can justify omitting selected repeated safety checks. The price moves into formal policy design, program semantics, proof production, certificate size and the trusted validation machinery; a tiny checker is an engineering aim, not an unconditional property of every PCC design.[^{ref-80d4e3370804-3][}ref-8510aeef79b3][^ref-761a74e7ac70]

Abstract Reasoning¶

Classify a proposed system by tracing consumer policy → exact received code → derived predicate → attached derivation → consumer verdict. If any binding is missing, the claimed assurance does not follow. For an altered binary, the consumer recomputes the predicate: it rejects if the certificate no longer proves it, but may admit a changed program that still comes with a valid proof. This separates policy compliance from code provenance and load-time admission from later integrity.[^ref-80d4e3370804-2]

Knowledge Transfer¶

The packet-filter and airfare-agent cases share the proof-transfer and consumer-admission structure while proving unlike properties: memory/control restrictions in one, database access and resource bounds in the other. PCC is proposed as a strict subtype of live Formal Verification, which need not deliver a certificate across an untrusted code boundary. A generic evidence-carrying admission skeleton outside executable software is a future-prime question, not this named computing method.[^{ref-80d4e3370804-3][}ref-5fdf2d654b95]

[^ref-7d64bce65649]: George C. Necula and Peter Lee, “Safe Kernel Extensions Without Run-Time Checking,” OSDI (1996), “Proof-Carrying Code” section. https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node2.html . [^ref-80d4e3370804]: Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” “Defining a Safety Policy.” https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node3.html . [^ref-80d4e3370804-2]: Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” “Validating the Safety Proofs.” https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node10.html . [^ref-80d4e3370804-3]: Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” “Application: Network Packet Filters.” https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node11.html . [^ref-5fdf2d654b95]: George C. Necula and Peter Lee, “Safe, Untrusted Agents Using Proof-Carrying Code,” in Mobile Agents and Security, LNCS 1419 (1998). https://doi.org/10.1007/3-540-68671-1_5 . [^ref-8510aeef79b3]: George C. Necula, original “Proof-Carrying Code” research-project account, especially Overview and Experiments §5. https://people.eecs.berkeley.edu/~necula/pcc.html . [^ref-761a74e7ac70]: George C. Necula and Robert R. Schneck, “Proof-Carrying Code with Untrusted Proof Rules” (2002), author companion abstract. https://people.eecs.berkeley.edu/~necula/ISSS02/ .

Relationships to Other Abstractions¶

Current abstraction Proof-Carrying Code Domain-specific

Parents (1) — more general patterns this builds on

Proof-Carrying Code is a kind of Formal Verification Domain-specific

PCC specializes formal verification to a producer-supplied proof checked by a distrustful code consumer before execution.

Neighborhood in Abstraction Space¶

Proof-Carrying Code sits in a moderately populated region (58^th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Network Security Vulnerabilities & Trust (26 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08