007CASE / Computer security
Code that carries a checkable argument
A consumer can check evidence that untrusted code meets a named safety policy without trusting its author.
SOURCE STATE · The Last Undo, Chapter 4 draft v0.5.0, opening sections and note 1; G. C. Necula and P. Lee, “Safe Kernel Extensions Without Run-Time Checking,” OSDI 1996.
This record reconstructs the argument in its cited manuscript draft. It is not a certified procedure or an independent audit.
THE JUDGMENT MACHINE
Trace the chain.
- Object
- Untrusted packet-filter code submitted for execution with a supporting proof.
- Observation
- The submitted code and the proof accompanying it.
- Distinction
- Respecting a specified safety policy is different from performing the intended task correctly.
- Representation
- A formal policy and machine-checkable evidence that the code respects that policy.
- Criterion
- The proof must validate against the consumer’s stated safety requirements.
- Judgment
- Accept only when the checker establishes the named policy. Do not enlarge that result into a claim of general correctness.
- Authority
- The code consumer chooses the policy; the checker establishes whether the submitted evidence meets it.
- Last undo / seam
- Before admitting the untrusted code to execution under the protected consumer’s privileges.
- Consequence
- The consumer can refuse code lacking a valid safety argument before it executes.
EVIDENCE & LIMITS
Keep the denominator attached.
The manuscript reports packet filters of 8–47 instructions, complete binaries of 385–1,024 bytes, and validation taking 780–2,350 microseconds in the cited experiment.
These are results for the reported experimental setting, not current performance benchmarks. A valid safety proof does not establish that the filter chooses the right packets, and the guarantee extends only to the policy and checker assumptions.
SOURCE TRAIL · The Last Undo, Chapter 4 draft v0.5.0, source note 1. Site reconstruction of the manuscript draft.