# Channel prevention for air-gapped computers with nearby observers

The proposed starting architecture is **dedicated computation inside a controlled
physical boundary, with a trusted offline release gate and qualified supporting
power, cooling and lifecycle procedures**. Its deployment optimum is
**UNDETERMINED**. No hardware configurations were measured or qualified in this
extension. There is no established universal setting that blocks every covert
channel on arbitrary useful hardware.

The [interactive field guide](https://thedarklightx.github.io/CovertChannelLab/channels.html)
contains 21 channel families, control proposals, falsifiers and primary sources.
The [machine-readable catalogue](research/coverage/catalogue.json) is a broad
inventory, not a completeness theorem about physics. A source demonstrating a
channel does not validate our proposed defense.

## The deployment boundary

The user selected **air-gapped computers with nearby observers**. Assume the
worker may deliberately choose its behavior to communicate unauthorized data.
Observers may own their sensors and combine recordings. The detailed capabilities
are still to be specified; they are not silently limited to the computer's APIs.

List allowed observer positions, minimum distance, physical access, cameras,
microphones, radio receivers, magnetometers, thermal sensors, accelerometers,
power-line access, precision, bandwidth, prior knowledge and recording duration.
Include any other apparatus allowed by the threat model. State whether observers
can stimulate the environment or operate a co-resident or subsequent workload.
Record multiple receivers and collusion explicitly. An unrestricted adversary is
not a meaningful measured specification with the current evidence.

An air gap removes intended network connectivity; it is not a claim that the
system emits no observable signal. The cited primary work demonstrates examples
on particular systems: [AIR-FI](https://arxiv.org/abs/2012.06884),
[MAGNETO](https://arxiv.org/abs/1802.02317),
[Fansmitter](https://arxiv.org/abs/1606.05915),
[LED-it-GO](https://arxiv.org/abs/1702.06715),
[PowerHammer](https://arxiv.org/abs/1804.04014),
[AiR-ViBeR](https://arxiv.org/abs/2004.06195), and
[BitWhisper](https://arxiv.org/abs/1503.07919).
Their demonstrated ranges and rates are not general constants, so this lab does
not turn them into universal safe distances or enclosure specifications.

The original cost-57 model assumes that the receiver sees a **mediated quantized
thermal value**. Its raw hot and quiet trajectories differ. An external sensor
can violate the observation premise even while that theorem remains true.
Keep [the original contract](CONTRACTS.md) and its result as a separate benchmark.

## Proposed architecture and open obligations

| Boundary | Proposed configuration to investigate | Obligation still open |
|---|---|---|
| Tasks and output | A policy-defined canonical result, sound private verifier, bounded checking work, total fallback, fixed public sizes and release slots | The task remains useful when the worker withholds or misbehaves; all permitted releases have the same authorized semantics and no extra discretion |
| Hardware sharing | Dedicated CPU, memory, storage and accelerators; no cross-domain SMT; controlled firmware and management interfaces | Enumerate shared and retained state, including buses, controllers and later sessions; prove or qualify partitioning and reset |
| Direct interfaces | Physically control unnecessary radios, ports, displays and removable media; route allowed input/output through the gate | No alternative release or maintenance path bypasses the policy; a one-way link alone does not sanitize its payload |
| Electromagnetic paths | Engineered boundary and feedthroughs; separate RF and low-frequency magnetic evaluation | Demonstrated attenuation and residual observation bounds for the stated sensor model, frequency range, seams, cables and workload envelope |
| Light, sound and vibration | Controlled visible/IR paths, acoustic isolation and mechanical coupling | The enclosure, fans, indicators, coils, surfaces and supporting equipment stay within the joint observation contract |
| Power and heat | Qualify supply/ground paths, load buffering or shaping, cooling, exhaust and external temperature | Bound transients, saturation, duration, recharge and cooldown; controller telemetry is itself an observable |
| Lifecycle | Controlled boot, reset, fault handling, alarms, logs, maintenance, reuse and disposal | The full transcript and subsequent access obey the same policy; necessary safety responses are explicitly included in authorized disclosure |

These are proposed engineering obligations, not controls implemented by this
repository. Dedicated resources reduce sharing opportunities; they do not by
themselves eliminate physical emissions. Constant software runtime does not imply
constant power or electromagnetic behavior. A conductive enclosure should not be
assumed to eliminate low-frequency magnetic, conducted, thermal or acoustic paths.
A local sensor API cannot constrain an observer's independent instrument.

[Time Protection](https://arxiv.org/abs/1810.05345v2),
[SecSMT](https://www.usenix.org/system/files/sec22-taram.pdf), and
[Rendered Insecure](https://www.cs.ucr.edu/~nael/pubs/ccs18.pdf) motivate separate
review of shared processor and accelerator resources. Their results are scoped
to their models and tested systems. The
[seL4 assumptions](https://sel4.systems/Verification/assumptions.html) illustrate
why a strong software proof still needs an explicit observation and hardware map.

## Exact-zero optimization contract

Let `c` be a candidate configuration in an explicitly defined space `C`.
Let `h` be protected information and arbitrary unauthorized worker choices, `p`
the public inputs, and `D(h,p)=d` the allowed declassification. `D` is fixed by
policy before the experiment; it cannot be chosen afterward to excuse leakage.
Its timing and availability are part of that policy, not free exceptions.

For fixed `p`, compare any `h,h'` with `D(h,p)=D(h',p)`. Let `a` range over all
allowed observer strategies, including adaptive actions and cooperating
receivers. Let `e` range over the declared environmental behaviors, initial-state
relations and uncertainty envelope. Use the same public environment strategy and
exogenous law in both runs; do not condition away a secret-dependent observable
by declaring it an external environment parameter. Include permitted histories,
repeated sessions, failures and all relevant lifecycle phases.

Let `O_joint(c,h,p;a,e)` be the entire jointly visible transcript over the declared
horizon: values, ordering, timing, absence of events, termination and physical
measurements. Require equal probability laws on this transcript space:

```text
for all c-admissible p, h, h', a, e with D(h,p) = D(h',p):
  Law(O_joint(c,h,p;a,e)) = Law(O_joint(c,h',p;a,e)).
```

For deterministic systems this becomes equality of traces. For randomized
systems it is equality of joint laws, not equality of averages or individual
sensor marginals. An infinite-horizon claim needs a well-defined trace space and
proof at that horizon; a finite capture cannot silently replace it. A claim
about one fixed duration does not establish secrecy under unlimited repetition.

The optimization is:

```text
minimize C_lifecycle(c), c in C
subject to joint noninterference under the declared observation contract,
           useful service(c) >= U_min > 0,
           public latency(c) <= L_max,
           implementation and physical refinement obligations.
```

Specify whether service and deadlines are worst-case guarantees; for a total
fallback claim they must cover every allowed worker behavior, not only successful
average runs. Cost should cover hardware, floor space, energy, cooling, validation,
operations and maintenance under declared weights. Security and service predicates
must be justified independently of those weights.

There may be no feasible candidate. An optimizer might also fail to attain an
infimum in an infinite design space. Return **INFEASIBLE**, **UNKNOWN**, a scoped
best candidate with a gap, or a certified optimum as the evidence warrants.
Do not assert a minimum merely because a solver returned a point.

A sufficient containment certificate can reject a safe configuration it cannot
prove. Optimizing only over certified candidates establishes an optimum of that
restricted set. It establishes a global secure optimum only with an additional
completeness, necessary-condition or lower-bound argument covering the excluded
designs. Preserve this distinction when generalizing the original benchmark.

The [deployment worksheet](research/coverage/deployment-contract.json) deliberately
leaves required inputs and evidence unset. `channel_checks.assessment` checks only
whether fields are populated; even a filled worksheet returns
`REQUIRES_INDEPENDENT_VERIFICATION`, never a security certificate. No solver for
physical configurations is implemented here.

## A practical bounded-leakage alternative

Exact-zero noninterference is a clear mathematical target. A deployment may instead
adopt a bounded distinguishability, information leakage or communication-capacity
goal. State the chosen metric, prior or adversarial quantifiers, confidence
procedure, sensor capabilities, horizon, repetition model and useful service
tradeoff. These metrics are different and should not be interchanged without an
argument. Treat unmeasured channels as unknown.

Noise, encryption, rate caps and finite negative measurements do not independently
establish all-time zero leakage. Masking may still leave correlations that survive
aggregation or repeated recordings. An observation below one instrument's
detection limit says nothing about an unspecified better receiver.
[NIST SC-31](https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-53r5.pdf)
calls for channel analysis and assessment in the operating environment, with
bandwidth reduction and performance tradeoffs addressed explicitly. This is not a
claim that this lab has satisfied a NIST certification.

## Negative knowledge in this extension

| ID | Rejected claim | Exact counterexample | Reusable lesson |
|---|---|---|---|
| CK-01 | Secret-independent marginals imply joint secrecy | `(R,R XOR H)` with uniform R; both marginals are uniform, but XOR recovers H | Check the full joint transcript and permitted coalitions |
| CK-02 | Whitespace normalization and equal lengths remove all output discretion | `Answer: 42.` and `Result: 42.` have the same length and authorized number, but differ | Define canonical semantic release, not cosmetic normalization |
| CK-03 | Silent shutdown meets a positive service floor | Abstract empty trace has service 0, required service 1 | Optimize useful operation; this says nothing about remanence of actual powered-off equipment |
| CK-04 | One abstract plan minimizes every positive cost weighting | Vectors A=(1,5), B=(4,1); weights (1,1) select B, (5,1) select A | Publish the objective; illustrative arithmetic is not a hardware price model |

Reproduce all witnesses and eight tests:

```sh
python3 scripts/verify_coverage.py
python3 channel_checks.py --check
```

The new [verification receipt](evidence/coverage/verification.json) pins sources
and generated results. The original 34 tests and 24 checked Lean declarations
remain separate; the new joint probability examples are checked in Python and
have not been formalized in Lean.

## Research Kernel record

Run: `covert-channel-lab-coverage-20260918`. Preserve the original publication
run and its exports. This extension uses `research/coverage/` for its report,
events, frontier and retrieval metadata. The user-selected deployment is a
decision record; the deployment optimum remains an open question. Four explicit
counterexamples refute four shortcut hypotheses. They do not prove a universal
physical impossibility statement.
The raw report lists eight REFUTED atoms: four hypotheses and their four witness
records, not eight distinct rejected hypotheses.

TheoremSearch returned adjacent or low-signal results; no retrieved theorem was
adopted as a premise. The formal-corpus request timed out and remains an inconclusive
tool result. There is no formal-corpus coverage claim. Public retrieval receipts
include identifiers, source links, classifications and body hashes instead of
republishing retrieved third-party theorem text. Raw tool evidence is retained in
the local ledger as retrieval-only evidence. Morph suggestions remain proposals.

Follow the [Research Kernel protocol](RESEARCH.md#research-kernel-protocol): state
the contract, retrieve prior failures, try to refute it, attach replayable evidence,
search contradictions, promote only within scope, and leave the next falsifier.
Keep negative and inconclusive results with their environment and source hashes.

## Work packet A1 — researchers: one real boundary

**First deliverable:** fill the observer and service worksheet for one owned or
authorized system. Freeze hardware, firmware, peripherals, enclosure, power,
cooling, sensor positions, calibration and allowed environment. Decide the
authorized output and safety disclosure policy before collecting data.

**Experiment:** compare permitted worker behaviors under the same public task and
authorized result, including adversarial withholding and lifecycle transitions.
Use synchronized multi-sensor recordings and controlled negative/positive checks.
Separate training, tuning and held-out workloads or sessions when estimating
distinguishability. Record bandwidth, resolution, duration, uncertainty, source
pins, raw data hashes and analysis code. Avoid adaptive test selection disguised
as a preregistered confidence claim.

**Falsifier:** a repeatable distinguishing transcript within the stated envelope,
or one admitted observable missing from the inventory. Keep successful and failed
attempts. Preserve calibration failures as inconclusive, not quiet successes.

**Acceptance:** a reviewed, reproducible measurement package with a precise
bounded claim and explicit untested regions. Measurement alone does not discharge
an infinite universal quantifier or establish global optimality.

## Work packet A2 — mathematicians: composition and refinement

**Question:** what assumptions make jointly observed software and physical
boundaries noninterfering? Define the declassification relation, observer
coalitions, adaptive traces, common randomness and allowed initial states.
State exactly which conditional independence or joint-kernel equality hypotheses
a composition theorem requires. Prove it, then map implementations to the premises.

**Falsifiers:** CK-01, correlated noise, shared controllers, repeated sessions,
adaptive sensors, secret-dependent alarms and out-of-envelope transients. Do not
silently assume that individually private marginals compose.

**Acceptance:** independently checked theorem statements with explicit premises,
counterexample regressions and a hardware/implementation assumption map. A future
Lean extension must pin its environment and audit every new theorem's axioms.

## Work packet A3 — joint team: a scoped optimum

**Question:** within the frozen design space and evidence envelope, find the least
cost design that delivers the required service and observation guarantee.
Publish candidate feasibility evidence separately from optimizer output.

**Falsifiers:** a cheaper feasible candidate, omitted cost component, unhandled
configuration, service failure, or a counterexample to the observation contract.

**Acceptance:** one validated feasible witness plus an independent lower bound,
or an explicit remaining gap and unknown candidates. Report infeasibility only
for the specified domain with supporting evidence. Keep the original thermal
optimum as a regression, not a premise for all-channel security.

## Inspiration

This independent project was inspired by **Noam Brown of OpenAI**, quoted with
attribution on the [results page](https://thedarklightx.github.io/CovertChannelLab/#inspiration-title)
from his [September 17, 2026 Dwarkesh interview](https://www.dwarkesh.com/p/noam-brown).
The architecture and research questions here are our synthesis. They are not
claims attributed to Brown or OpenAI, and no endorsement is implied.