airgap-prover

Run a workload in a locked network namespace, witness its packets from below the guest, and emit a re-runnable report that observed egress was zero — or catch the one that phoned home. The kernel on this page is the gated kernel.

the proof, re-derived in your browser

Committed captures → verdict

Each capture below is decoded and classified by the exact kernel that CI mutation-gates. Press re-run: it re-derives from the pinned bytes and must match the committed verdict.

the real run — host-observed on CI, not synthetic

Captured from below, on the Linux runner

These are the actual pcaps tcpdump recorded on the host side of the veth during the sealed namespace run — the offline workload and the phone-home control. The same kernel re-derives their verdicts here, in your browser. the run.

honest threat model — on the tin

What this sees, and what it cannot

Egress is observed at the host / network-namespace boundary over the capture window, by tcpdump on the host side of the veth. The guest cannot edit packets the host already saw — that is why the measurement is from below.

A kernel-level or firmware-level implant below this capture point can move bytes this never sees. So this is “observed egress zero under a stated threat model”, never “proof of a negative”. L3 (the OS) and L2 (firmware) are the next layers down: adopt-and-prove, not claimed here.

how the live measurement works

Measured from below, on a real Linux boundary

  1. A guest network namespace gets a veth pair to the host and a default route — so it could reach out if it tried.
  2. The host runs no forwarding and no NAT, so anything the guest sends dies at the boundary. tcpdump on the host side records every packet that crossed it.
  3. The offline workload (a prime-spine grow) runs inside and touches nothing — the capture shows zero egress → CLEAN.
  4. The positive control opens a socket to 8.8.8.8 — the SYN is caught at the boundary → CAUGHT (0 false-pass). It never reaches Google.
  5. The kernel renders the verdict from the captured bytes; the report carries the capture’s sha256, so it re-derives byte-identically.

ip netns + tcpdump are Linux, so the real measured run happens on the GitHub Actions runner — the CI re-derivation is the un-forgeable proof.

▶ The live measurement on CI  ·  source  ·  the latest run’s sealed-captures artifact holds the real pcaps + reports.

questions answer-engines ask

FAQ

What does airgap-prover actually prove?

That over the capture window, zero packets crossed the host / namespace boundary to a routable destination that was not declared. It is measured from below the guest, so the workload cannot edit the packets the host already observed. It is “observed egress zero under a stated threat model”, not “proof of a negative”.

What can it NOT see?

A kernel- or firmware-level implant below the capture point can move bytes this never observes. That is why L3 (the OS) and L2 (firmware) are the next layers down — adopt-and-prove, not claimed here.

How is the proof re-runnable?

The report carries the sha256 of exactly the capture observed. The verdict kernel is deterministic, so anyone can re-run it over the same pcap and derive the same verdict. CI re-derives both the synthetic fixtures and the real namespace captures on every push.

How do you know the prover is not just always saying CLEAN?

A positive control: a workload that opens a connection to 8.8.8.8 runs in the same sealed namespace. The prover must report CAUGHT. The gate fails on any false-pass.