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) makes an untrusted program carry evidence that a separate code consumer can check before running it. The consumer sets the permitted-behavior policy and a formal way to derive a safety obligation from executable code. The producer supplies code and a formal proof of that obligation. On receipt, the consumer derives the obligation from the code it actually received, validates the supplied proof against it, and admits the code only if the check succeeds. The producer may use an expensive compiler or prover; the consumer need not trust either one.^[1]^[2]^[3]

The conclusion is precisely scoped: the checked executable satisfies the stated policy under the soundness and calling assumptions of the consumer's semantics, obligation generator and proof validator. It is not blanket security, authorship authentication or a promise that code cannot later change. If a program or certificate changes before admission, validation either fails or establishes the policy for the changed received program; a modification after validation is outside that one-time check.^[2]^[3]^[4]

Structural Signature¶

Sig role-phrases: consumer-defined policy and semantic model → untrusted producer and executable → code-derived proof obligation → attached formal certificate → consumer checker and admission gate → scoped trust condition.

Consumer-defined policy and semantic model. The receiver states what “safe” means, including the operational semantics and initial calling assumptions needed to relate machine behavior to a logical predicate. The original construction uses a verification-condition (VC) generator, axioms and a precondition. Without this role, a certificate has no determinate consumer-side target.^[2]
Untrusted producer and executable. The sender creates the code and may perform hard proof search. Distrust of this sender is the reason to carry a checkable derivation rather than depend on a trusted origin or compiler.^[1]^[4]
Code-derived proof obligation. The receiver recomputes a predicate for the received executable. A proof merely about a claimed source file or another binary would not bind the code about to run.^[3]
Attached formal certificate. A producer-generated derivation travels with the code and discharges the policy predicate. If the consumer must discover the proof itself, the arrangement may still be formal verification, but it has lost the “carrying” division of labor.^[1]^[4]
Consumer checker and admission gate. A validator determines whether that derivation proves the receiver's predicate and accepts or rejects before execution. “Small and fast” is a design objective demonstrated in the original prototype, not a theorem that every PCC policy has a tiny checker.^[3]^[5]
Scoped trust condition. The result depends on the policy and formal semantics being sound for the intended property, the VC generator and proof checker being implemented correctly, the calling precondition holding, and the host executing the same code that passed checking. Move any of these assumptions and the guarantee must be re-established.^[2]^[3]^[4]

What It Is Not¶

Not a digital signature or provenance check. A signature can identify an issuer or detect a changed signed object; PCC checks an intrinsic, policy-relative program property. It need not establish who supplied the code.^[4]
Not every formal verification exercise. A developer may prove its own program correct without shipping the proof to a distrustful receiver or making receipt conditional on that receiver's policy. PCC adds that cross-boundary proof handoff and admission rule.
Not an interactive proof system. The defining exchange here is executable plus certificate followed by a receiver-side check, not a randomized back-and-forth protocol for language membership.
Not identical to typed assembly language or bytecode verification. Types may help construct or express a PCC proof; a bytecode verifier may check code locally. Neither by itself requires producer-shipped proof for the exact executable and consumer policy.^[4]
Not assurance about all possible hazards. An accepted proof addresses only the formalized policy under its machine model and preconditions. A weak policy, unsound validator or post-check code mutation can leave relevant hazards untouched.^[2]^[3]
Not the abolition of every run-time check. The original examples avoid selected repeated checks because specified properties were statically proved. Other checks, properties and changing environmental facts can remain.^[6]^[4]

Scope of Application¶

PCC is useful when executable code crosses a trust boundary and the receiver wants high-assurance, policy-specific admission without trusting the producer's compiler, proof search or reputation. In the original kernel-extension setting, packet-filter code is invoked on every arriving network packet inside the operating-system kernel. Necula and Lee therefore checked a native filter once at admission under restrictions on memory reads, memory writes, branch direction and preserved registers, rather than relying on a check at each protected operation. The calling precondition, including valid packet and scratch areas, remains part of the safety claim.^[6]

The original authors also experimented with mobile agents accessing an airfare database. There the receiving host's policy concerned which records an agent could read, as well as instruction-count and network-bandwidth bounds. This is a distinct use of the same architecture: the code's risk is not just writing outside a packet buffer, but using host data and resources beyond a stipulated level. It was a research experiment, not evidence of broad deployment.^[7]^[4]

The method can be implemented using different proof representations or producer-side tools. The 1996 prototype used LF proof terms whose validation reduces to type checking; later work explored other representations and untrusted high-level proof rules. Such choices change proof size, effort and trust-base engineering, but not the producer–consumer obligation/checking pattern.^[3]^[4]^[5]

Clarity¶

PCC answers a narrow question: Does this received executable carry a valid proof of the receiver's stated policy predicate? The checker does not take the producer's claim “this code is safe” at face value. It computes its own predicate from the code and tests whether the certificate proves that predicate. The distinction between a proof about code and a proof bound to this code is decisive. The 1996 validation procedure explicitly extracts native code from the binary, recomputes its safety predicate and checks the proof.^[3]

“Tamperproof” in early descriptions is conditional shorthand, not immunity to edits. A changed proof may fail; a changed binary may have a different unproved predicate; but some changes leave the predicate unchanged, or a new valid proof can accompany newly changed code. Such a program can legitimately pass. Conversely, if validated memory can subsequently be changed before execution, the previously checked certificate no longer establishes a property of the executed bytes. PCC itself does not supply ongoing code-integrity monitoring or sender authentication.^[3]^[4]

Manages Complexity¶

The architecture relocates difficult proof construction to the party supplying code and makes admission a bounded consumer-side check. The receiver need not repeat proof discovery for every incoming extension and need not trust a complex upstream compiler. In the kernel packet-filter case, this matters because the filter can execute on every packet: the up-front proof-check cost is paid when the binary is admitted, while repeated protected operations can avoid selected checks whose safety has been proved.^[6]^[4]

That compression is not free. A policy must be precisely modeled; the VC generator must connect machine instructions to logical claims; proofs must be generated, encoded and transmitted; and the consumer's checker and trusted rules require audit. The authors explicitly identify proof size, checker speed/size and proof-to-program binding as implementation difficulties. Moving proof search outside the trust boundary does not remove the need to trust sound policy machinery inside it.^[2]^[4]^[5]

Abstract Reasoning¶

To analyze a claimed PCC system, first identify the distrust boundary: who produces the executable, and who decides whether it may run? Then name the exact policy property, model of execution and preconditions. Trace how the receiving side derives the proof obligation from the executable it has, and how it validates the accompanying certificate. Only then state what the admission verdict warrants. This prevents a certificate for source-level intent, for an earlier binary, or for a different policy from silently standing in for a proof about the executable being launched.^[2]^[3]

For a changed code bundle, apply the same test again. If the consumer derives a different obligation that the old proof does not establish, reject. If the altered bundle still supplies a valid derivation of the received code's policy predicate, acceptance is consistent with PCC even though the sender or behavior changed. This reasoning separates policy compliance from Provenance and separates a load-time result from continuing integrity after loading.^[3]

Knowledge Transfer¶

The packet-filter and airfare-agent prototypes transfer the same relation: untrusted code plus producer certificate crosses to a host; the host derives a code-specific policy predicate and checks the proof before admission. What changes is the safety property. In the kernel case, the filter's permissible memory and control effects dominate. In the database-agent case, record access levels and bounded resources dominate. The proof-transfer architecture stays recognizable because those policies are receiver-controlled and formally checked against the received program.^[6]^[7]^[4]

The broad “attach evidence to an object so a recipient can check it” motif also occurs outside code, but that motif alone is not PCC. The literal identity requires executable software, a formal program-to-policy obligation and a receiving execution gate. Whether that portable skeleton deserves its own prime is a future-prime question, not a reason to classify this computer-security method as substrate-independent.

Examples¶

Native packet filters in a kernel¶

Necula and Lee's original prototype accepts application-provided native packet-filter subroutines that the kernel invokes on incoming packets. Its policy restricts reads to the packet and scratch memory, writes to scratch memory, branch direction and certain registers, assuming valid input addresses. A producer certifies a filter; the kernel computes the safety predicate for the binary it receives, checks the proof and then admits the filter. This does not say every possible kernel hazard has been proved away—only the specified restrictions under the stated precondition.^[2]^[6]^[3]

Mapped back: consumer-defined policy and semantic model = kernel packet-filter access/control rules and machine/calling assumptions; untrusted producer and executable = application-supplied native filter; code-derived proof obligation = VC for its received instructions; attached formal certificate = packaged proof of that VC; consumer checker and admission gate = proof validation before kernel invocation; scoped trust condition = sound rules, valid packet/scratch inputs and execution of the validated binary.

Experimental airfare-database mobile agent¶

In the authors' mobile-agent study, an untrusted agent reaches a host with an airfare database. The host assigns an access level, and the agent must establish that it reads only eligible records; the research account also describes bounded instruction use and network bandwidth. The receiving host checks the supplied proof instead of taking the agent's claim of harmlessness or its producer's reputation as authority. This is an experimental demonstration, not a claim that a production airfare service ran PCC.^[7]^[4]

Mapped back: consumer-defined policy and semantic model = host's record-access and resource rules; untrusted producer and executable = incoming agent; code-derived proof obligation = predicate over that agent's admissible accesses and resource behavior; attached formal certificate = producer's derivation; consumer checker and admission gate = host validation before execution; scoped trust condition = correctness of the database/resource model and execution of the checked agent under the assumed host interface.

Negative case: signed plugin only¶

A host may accept a plugin because a trusted vendor signed it. That can establish an origin claim or integrity of the signed bytes, but without a formal certificate of the host's code-specific policy obligation and a consumer proof check, the attached formal certificate and consumer checker roles are absent. Signing can complement PCC; it does not instantiate it by itself.^[4]

Structural Tensions¶

T1 — Richer policies versus an auditable trusted base. The consumer may want memory, data-access and resource properties, but proving those requires semantics, axioms and VC generation strong enough to express them. Hard-wiring higher-level proof rules into the consumer enlarges what must be trusted; schemes that make producers justify those rules shift work outward but still need a sound low-level kernel. Diagnostic: Which rules and program-to-predicate translations are trusted rather than proved?^[2]^[5]

T2 — Upstream proof burden versus downstream cheap checking. Producer-side proof search and certificate creation can be hard or yield large evidence; receiver-side validation can be comparatively simple and amortized across many executions. The bargain is attractive for a frequently executed filter but can be poor if proof production or transport dominates. Diagnostic: How often will a checked binary run, and how costly is its certificate to find, ship and validate?^[3]^[6]^[4]

T3 — Static policy assurance versus changing code or assumptions. A successful load-time check can discharge a covered safety obligation for the admitted executable. It does not freeze later code bytes, certify unaudited environmental behavior or prove a property outside the policy. Diagnostic: Are the executed bytes, host interface and policy assumptions the ones for which the certificate was checked, and which separate run-time controls remain?^[2]^[3]

Structural–Framed Character¶

PCC is structural within software assurance but domain-bound. Evaluative weight: it specifies a proof-carrying admission relation; “safe” means meets a chosen policy, not that every desirable value is realized. Human-practice dependence: engineers choose the policy, semantics and risk boundary, but the code–predicate–proof relation is mechanically checkable once fixed. Institutional origin: the named method emerged in particular systems research; no standards body grants the identity. Vocabulary travel: “carrying evidence” travels metaphorically, while executable code and formal program-policy proofs do not. Import versus recognition: an analyst recognizes PCC by the actual proof transport and receiver check, not by a developer labeling a build “certified.”^[1]^[2]

Its character: a domain-specific formal code-admission architecture. A broader evidence-carrying acceptance mechanism remains a future-prime question; this node does not inherit prime status merely because its proof-transfer roles are abstractable.

Structural Core vs. Domain Accent¶

The core is receiver policy and program semantics → untrusted executable → executable-specific obligation → producer certificate → receiver proof check → conditional admission. The proposed DAG parent is Formal Verification by strict subsumption: both rely on a machine-checkable formal proof that an engineered artifact meets a stated specification; PCC adds untrusted producer/consumer separation, proof delivery with code, receiver recomputation and an execution gate. The parent can hold for a locally verified program without any of those PCC-specific commitments.^[1]^[3]

The domain accent is executable binary loading, instruction semantics, memory/resource policies, calling conventions, VC generation and certificate representation. Formal System is already a presupposed parent of live Formal Verification and need not be redundantly asserted here. Verification is that parent's broader genus. A portable “claim plus checkable evidence crossing distrust” skeleton is not yet an admitted prime; it is the explicit future-prime question, not a license to erase the computing-specific policy and code binding.

This entry is a kind of Formal Verification.

Asserted parent — Formal Verification. PCC adds proof delivery and receiver-side admission to a code-specific formal conformance result.
Inherited prerequisite — Formal System. A logical policy and derivation rules make proof checking meaningful; this relation is already represented above the asserted parent.
Inherited genus — Verification. The receiver checks an object against a criterion and produces an accept/reject verdict, but the proof-carrying handoff is narrower.
Related, not parent — Interactive Proof System. Its verifier–prover protocol is an interactive complexity-theoretic object, not this executable-plus-certificate loading arrangement.
Related implementation — Typed Assembly Language. Typed low-level code can aid proof generation, but PCC does not require that specific language or type discipline.^[4]

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

Not to Be Confused With¶

Signed code. Tell: origin or integrity may be certified, but no formal policy predicate about executable behavior is necessarily proved.^[4]
Local formal verification. Tell: proof might exist without accompanying the delivered program or being checked by a separate distrustful receiver.
Bytecode verification. Tell: the consumer may run a verifier on delivered bytecode without receiving a producer-generated proof certificate; the original authors compared and combined such techniques.^[4]
Proof about source only. Tell: if the receiving side cannot relate the proof to the exact executable it admits, code-proof binding has not been supplied.^[3]
Absolute tamper resistance. Tell: pre-check edits may yield a new accepted policy-compliant program, while post-check edits invalidate any inference about the bytes eventually executed.^[3]

References¶

[1] George C. Necula and Peter Lee, “Safe Kernel Extensions Without Run-Time Checking,” OSDI (1996), “Proof-Carrying Code” section. Original publication: https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node2.html . registry ↩a ↩b ↩c ↩d ↩e

[2] Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” “Defining a Safety Policy,” numbered policy elements and abstract-machine discussion. https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node3.html . registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k

[3] Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” “Validating the Safety Proofs,” especially first three paragraphs on computing the received code's predicate and checking its proof. https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node10.html . registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q

[4] George C. Necula, “Proof-Carrying Code,” original research-project account, Overview, Technical Difficulties, Implementation and Experiments §5 (mobile agents). The page identifies itself as historical/out of date. https://people.eecs.berkeley.edu/~necula/pcc.html . registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s

[5] George C. Necula and Robert R. Schneck, “Proof-Carrying Code with Untrusted Proof Rules” (2002), original author companion abstract on trusted high-level rules. https://people.eecs.berkeley.edu/~necula/ISSS02/ . registry ↩a ↩b ↩c ↩d

[6] Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” “Application: Network Packet Filters,” policy and implementation discussion. https://www.usenix.org/legacy/publications/library/proceedings/osdi96/full_papers/necula/html/node11.html . registry ↩a ↩b ↩c ↩d ↩e ↩f

[7] George C. Necula and Peter Lee, “Safe, Untrusted Agents Using Proof-Carrying Code,” in Mobile Agents and Security, LNCS 1419 (1998), chapter abstract and experimental case. https://doi.org/10.1007/3-540-68671-1_5 . registry ↩a ↩b ↩c