Field guide 002 / Air-gapped computers
What configuration prevents covert communication when the observer is standing nearby?
Start with dedicated hardware, a trusted release gate, and a physical boundary covering emissions, power, cooling and access. Then test the entire observation history against a defined threat model.
Defensive research · Proposed controls · No physical deployment qualified
A nearby observer can bring its own camera, microphone, radio receiver, magnetometer or temperature sensor. The thermal model’s cost-57 result assumes a mediated sensor value. It does not block those independent observations.
01 / A configuration to investigate
This is a proposed architecture, not a measured optimum or a shopping specification. Each boundary needs a stated observer model and evidence.
Joint recordings · Independent sensors · Repeated sessions
No direct output or shared untrusted devices
Bounded work, total fallback, fixed release slots
Define allowed locations and minimum distance, sensor bandwidth and precision, prior knowledge, observation duration and collusion. Cover the building’s surfaces, cables, exhaust and later access. No universal safe distance is supplied here.
Remove or physically control unused radios, ports, displays and peripherals. Dedicate CPU, memory, storage and accelerators to the security domain; avoid cross-domain SMT. Check firmware and management paths. Software isolation alone does not account for every shared resource. [Time protection] [SecSMT]
Use a trusted offline gate with bounded verification and a total fallback. For the same authorized result, bytes, size, timing, retry behavior and termination must not remain worker choices. Open-ended prose or a one-way link can still carry an unauthorized message. Restrict tasks when a canonical useful release cannot be specified.
Evaluate radio-frequency and low-frequency magnetic paths separately, including seams, cables and penetrations. Cover visible and infrared light, sound, ultrasound and mechanical coupling. A conductive enclosure or removal of speakers is not a certificate for all these paths. [AIR-FI] [MAGNETO] [Fansmitter]
Qualify the external power feed and grounding, cooling plant, airflow, exhaust and boundary temperature under allowed workloads. Internal buffering or load shaping is a proposal to evaluate, not proof of constant emissions. Include saturation, battery recharge and cooldown. [PowerHammer] [BitWhisper]
Include startup, reset, failure, alarms, logs, maintenance, media movement and disposal. Safety alarms must still function; their visibility belongs in the authorized-release policy. A worker-triggered shutdown can itself be an observable bit. Test with combined sensors across repeated sessions.
Engineering proposals synthesized for this threat model. The cited papers establish channel examples on tested systems; they do not certify these controls. Source notes distinguish literature evidence from this lab’s results.
02 / The channel inventory
{{channel_count}} families across digital output, shared computation, physical emissions and lifecycle effects. This is a broad working inventory, not an exhaustive classification of possible physics.
Showing {{channel_count}} of {{channel_count}} channel families · Deployment qualification remains open.
No families match this search. Clear the search or choose another group.
A covert channel involves unauthorized communication; a side channel can expose secrets without a cooperating sender. Direct interface bypasses and remanence are also included because a complete defense must account for them. [Terminology]
03 / Why the channels must be checked together
Let a fair random bit be R and the private bit be H. One observer sees X = R. Another sees Y = R ⊕ H. Each observation alone is uniformly random for either H.
Choose the private bit
| X ↓ / Y → | 0 | 1 | X alone |
|---|---|---|---|
| 0 | 1/2 | 0 | 1/2 |
| 1 | 0 | 1/2 | 1/2 |
| Y alone | 1/2 | 1/2 | 1 |
H = 0: the observations are equal. X ⊕ Y recovers 0 exactly.
Changing H moves all probability to different pairs. Combining the observations recovers H with certainty, even though both individual distributions stay the same.
A per-sensor checklist cannot establish joint secrecy. Include shared randomness, sensor fusion, time correlations and cooperating receivers in the claim.
This is a mathematical counterexample, not a measured physical attack. It is generated with exact fractions and checked independently by the tests.
Inspect the exact witness ↗04 / What “optimal” actually requires
Choose a configuration only after its candidates, costs, utility requirement and observation model are explicit.
The proposed exact-zero contract
minimize C(c)
subject to service(c) ≥ Umin > 0, public latency ≤ Lmax, and
Law(Ojoint | h, p, d, a, e, c) = Law(Ojoint | h′, p, d, a, e, c)
For every allowed pair of secrets h, h′ with the same public inputs p and authorized declassification d; every permitted observer strategy a and environment e. Ojoint is the full joint transcript over the declared horizon. In a deterministic model, require equal traces. See the quantifiers and assumptions.
Specify the actual hardware, allowed tasks, trusted release policy, sensors and distance, duration, environmental bounds, service floor, deadline and cost model. Construct and review the candidate configuration space.
The worksheet currently has {{contract_gap_count}} unresolved fields. Filling them in does not certify their truth.
Start the deployment worksheet ↗A feasible witness must satisfy the joint observation contract and useful service requirement. A separate lower bound or exhaustive justified search must rule out cheaper feasible candidates.
No such deployment witness or lower bound is available here. A finite quiet recording, added noise, encryption, an air gap or a small observed bitrate is not an all-time zero-leakage proof.
05 / Useful negative knowledge
These counterexamples reject specific claims. They neither prove physical containment impossible nor identify an optimal real machine.
Replay this extension
Python standard library · {{coverage_test_count}} tests · Exact finite arithmetic
python3 scripts/verify_coverage.py
python3 channel_checks.py --check06 / Continue the work
Choose one real air-gapped system. Freeze its hardware, firmware, enclosure and environment. Fill the observer worksheet, including access to power, surfaces and exhaust. Record synchronized sensor traces for permitted workloads, failures and lifecycle events.
Use held-out workloads and combined receivers. Preserve calibration, raw data, uncertainty, negative controls and every successful distinguishing witness. A null result retains its measurement limits.
Formalize the joint observation space and authorized declassification. Prove a composition theorem with explicit independence or conditional hypotheses, then refine each physical and software boundary to it.
For optimization, prove feasibility before a cost lower bound. Track undecided candidates and the remaining gap. The original 24 Lean declarations do not establish this broader deployment claim.
Detailed work packets and acceptance criteria ↗/Research Kernel protocol ↗
Run: covert-channel-lab-coverage-20260918. Semantic theorem searches supplied no adopted proof premise; the formal-corpus lookup timed out. The local finite counterexamples stand on their replay, not retrieval scores. Inspired by Noam Brown of OpenAI’s discussion, quoted on the results page.
07 / Sources & attribution
Primary research and official references identify known classes. Device-specific results do not establish present-day susceptibility of every device or validate this proposed architecture.