COVERT CHANNEL LAB

Field guide 002 / Air-gapped computers

No network.
Still observable.

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

The key change

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

Contain the machine.
Account for the boundary.

This is a proposed architecture, not a measured optimum or a shopping specification. Each boundary needs a stated observer model and evidence.

Outside the controlled boundaryNearby, possibly cooperating observers

Joint recordings · Independent sensors · Repeated sessions

Qualified physical boundary + controlled access
Dedicated computeUntrusted worker

No direct output or shared untrusted devices

Trusted mediationVerify + canonicalize

Bounded work, total fallback, fixed release slots

Power feedthroughsHeat & airflowSignals & seamsMaintenance & disposal
Only the declared, authorized releaseEvery other observable remains a separate proof obligation.
A design requirement: the receiver’s full transcript includes the enclosure and its supporting systems, not just the application’s output.
01

Specify who can observe what.

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.

02

Remove unnecessary interfaces and sharing.

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]

03

Release one policy-defined answer.

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.

04

Engineer the physical boundary.

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]

05

Include power and heat removal.

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]

06

Keep the contract through the lifecycle.

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

Trace every path
to an observation.

21 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 21 of 21 channel families · Deployment qualification remains open.

D01Output meaning and encodingDigital release and storage

covert carrier · Deployment unqualified

Observation path
A worker chooses among externally distinguishable answers, file names, encodings or provenance.
Proposed control
Release one host-defined canonical authorized result through a trusted gate. Open-ended content needs a separate semantic policy.
Try to refute it
Two accepted outputs for the same authorized task reveal the worker-selected bit.
Evidence here
Original abstract canonical-release proof; open-ended semantic selection remains outside it.
D02Timing, termination and retriesDigital release and storage

covert carrier · Deployment unqualified

Observation path
Completion, withholding, retransmission, failure or release order affects an observer.
Proposed control
Use a public schedule, total independent fallback and bounded admission. Include recovery and every downstream timestamp.
Try to refute it
Withholding or an invalid proposal changes a public release time or a failure flag.
Evidence here
Original fixed-slot and total-fallback model; no real scheduler refinement.
D03Lengths, counts and traffic shapeDigital release and storage

covert carrier · Deployment unqualified

Observation path
Object sizes, export frequency, packet counts and intervals can encode information.
Proposed control
Fix public envelopes from authorized inputs; account for padding, dummy work, acknowledgments and external transport.
Try to refute it
Equal authorized results produce different externally visible sizes or counts.
Evidence here
Unimplemented observation obligation; encryption alone does not settle it.
D04Shared storage and metadataDigital release and storage

covert carrier · Deployment unqualified

Observation path
File existence, free capacity, queues, locks or metadata connects two domains.
Proposed control
Remove cross-domain mutable namespaces or refine a trusted mediator for all visible state.
Try to refute it
A worker changes one shared metadata bit that another domain can read.
Evidence here
A single abstract shared-state coordinate is modeled; real file systems are not.
D05Network, protocol and peripheral pathsDigital release and storage

bypass and covert carrier · Deployment unqualified

Observation path
Network interfaces, DNS, radios, USB or device protocols provide direct or indirect egress.
Proposed control
Enforce the air gap and device allowlist below the worker; mediate any intentional import or export.
Try to refute it
An unmediated path exists, or an allowed protocol field retains worker-controlled freedom.
Evidence here
Original abstract egress flag only. Ordinary unauthorized egress is also inventoried.
D06Logs, errors, telemetry and billingDigital release and storage

covert carrier · Deployment unqualified

Observation path
Diagnostics, counters, alerts and management summaries become public messages.
Proposed control
Keep raw diagnostics within the trusted domain; release only scheduled, policy-defined summaries with their own observation proof.
Try to refute it
A log field or visible alert varies with a private worker choice.
Evidence here
Research obligation; publication logging is not a runtime security implementation.
S01CPU caches, TLBs and prediction stateShared computation and devices

side-channel and covert carrier · Deployment unqualified

Observation path
Shared or retained microarchitectural state changes another computation or its timing.
Proposed control
Use dedicated domains or hardware-specific time protection; verify partitioning, flushing and residual state coverage.
Try to refute it
A competing or subsequent task distinguishes private activity despite process isolation.
Evidence here
Literature establishes the class; no tested hardware configuration is provided here.
S02SMT, execution units and schedulingShared computation and devices

covert carrier · Deployment unqualified

Observation path
Contention over pipelines, execution ports or scheduling budgets changes service to another domain.
Proposed control
Avoid cross-domain SMT and unqualified dynamic sharing; include the entire scheduler and shared fabric in the contract.
Try to refute it
A co-resident task distinguishes two private workload patterns.
Evidence here
No processor-specific contention or scheduler certificate in this lab.
S03GPUs and acceleratorsShared computation and devices

side-channel and covert carrier · Deployment unqualified

Observation path
Shared accelerator memory, execution resources, counters and runtime state connect workloads.
Proposed control
Assign an entire qualified device or prove device-specific partitioning and reset; restrict counter and management exposure.
Try to refute it
A second workload or later session distinguishes another job through an exposed GPU resource.
Evidence here
Published attacks motivate review; current device and driver behavior must be checked separately.
S04Memory buses, I/O queues and DMAShared computation and devices

side-channel and covert carrier · Deployment unqualified

Observation path
Memory traffic, device queues, interrupts and transfers expose contention or writable state.
Proposed control
Separate resources or verify end-to-end arbitration, IOMMU/DMA behavior, device firmware and completion timing.
Try to refute it
A receiver observes a queue delay or transfer state affected by the worker.
Evidence here
Trusted-device and hardware assumptions remain unvalidated.
P01Radio-frequency and electromagnetic emissionsNearby physical observations

covert carrier · Deployment unqualified

Observation path
A nearby independent receiver measures emissions from workload-driven electrical activity.
Proposed control
Engineer an emissions boundary with frequency-specific attenuation and qualified penetrations; constrain and validate receiver positions.
Try to refute it
A permitted receiver distinguishes workloads outside the enclosure.
Evidence here
AIR-FI is a channel demonstration; this lab has no emissions measurements.
P02Low-frequency magnetic fieldsNearby physical observations

covert carrier · Deployment unqualified

Observation path
A nearby magnetometer observes workload-dependent magnetic fields.
Proposed control
Analyze low-frequency magnetic coupling separately from RF shielding, including enclosure materials and permitted proximity.
Try to refute it
A permitted magnetic sensor distinguishes two worker loads.
Evidence here
MAGNETO motivates a separate obligation; an RF enclosure label is insufficient evidence.
P03Acoustic and ultrasonic emissionsNearby physical observations

covert carrier · Deployment unqualified

Observation path
Microphones observe speakers, fans or other electromechanical sound.
Proposed control
Remove unneeded transducers; qualify acoustic treatment and trusted actuation across the allowed sensor bandwidth.
Try to refute it
A nearby microphone distinguishes workloads even with speakers removed.
Evidence here
Fansmitter supplies a demonstrated fan channel; no acoustic barrier is measured here.
P04Visible and infrared lightNearby physical observations

covert carrier · Deployment unqualified

Observation path
A camera or optical sensor sees displays, indicator activity or a path through an opening.
Proposed control
Remove worker-controlled indicators and displays; use an opaque qualified boundary and inspect optical paths and feedthroughs.
Try to refute it
A permitted optical receiver distinguishes workload-dependent emitted light.
Evidence here
LED-it-GO demonstrates an indicator path; proposed infrared review extends the observer inventory.
P05Conducted power and shared electrical infrastructureNearby physical observations

covert carrier · Deployment unqualified

Observation path
A receiver on shared supply infrastructure observes workload-dependent electrical behavior.
Proposed control
Evaluate engineered power isolation, filtering and load regulation against the specified measurement points. A separate outlet is not a certificate.
Try to refute it
A permitted supply-side measurement distinguishes workload patterns.
Evidence here
PowerHammer demonstrates a conducted channel; no supply boundary is qualified here.
P06Mechanical vibration and shared surfacesNearby physical observations

covert carrier · Deployment unqualified

Observation path
Nearby devices sense vibrations transmitted through desks, racks or building structure.
Proposed control
Account for mechanical coupling and trusted moving components; qualify mounting and isolation under the stated observer model.
Try to refute it
A permitted sensor on a shared surface distinguishes private activity.
Evidence here
AiR-ViBeR demonstrates this class; no mounting design is tested here.
P07Heat, airflow and cooling behaviorNearby physical observations

covert carrier · Deployment unqualified

Observation path
Nearby instruments read raw temperature, exhaust, fan behavior or thermal effects on another device.
Proposed control
Bound and qualify external thermal behavior, initialization, aggregate load and cooldown. Receiver-owned instruments cannot be virtualized by the sender.
Try to refute it
Hot and quiet allowed workloads yield distinguishable external readings.
Evidence here
Earlier s=7,r=2 theorem protects a mediated quantizer only; it does not protect this raw observer.
L01Remanence and cross-session stateLifecycle and composition

related leakage and storage carrier · Deployment unqualified

Observation path
Residual memory, media, firmware, caches or learned state connect sessions.
Proposed control
Define every persistent state owner and verified sanitization or restoration step, including hardware and model state.
Try to refute it
A later permitted session observes a bit written during a prior private session.
Evidence here
No lifecycle reset proof. Cold-boot research illustrates why software restart is not an erasure guarantee.
L02Management, maintenance and operatorsLifecycle and composition

assurance boundary and bypass · Deployment unqualified

Observation path
Controllers, firmware updates, service interfaces or human-visible procedures cross the boundary.
Proposed control
Minimize and separately authorize management; include its outputs, maintenance media and operator-visible workflow in the transcript.
Try to refute it
A service interface or visible maintenance response depends on a worker-controlled event.
Evidence here
Proposed threat-model obligation, not a proved operational protocol.
L03Joint observations and colluding receiversLifecycle and composition

composition obligation · Deployment unqualified

Observation path
Receivers combine several individually innocuous signals, or several workers combine actuation.
Proposed control
Prove joint trace independence for the full coalition and aggregate loads; model adaptive observations across time.
Try to refute it
Two uniform individual signals reveal a secret when paired.
Evidence here
New exact two-bit counterexample in channel_checks.py.
L04Faults, alarms, resets and availabilityLifecycle and composition

covert carrier and assurance boundary · Deployment unqualified

Observation path
Selective crashes, shutdowns, failed checks and recovery produce visible differences.
Proposed control
Model failure outputs and deadlines. Preserve required safety behavior while including its observability in the contract.
Try to refute it
An adversary selects whether a public alarm or recovery event occurs.
Evidence here
Fallback proof assumes the total reference result is available; physical fault handling is not verified.

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

Individually silent.
Jointly revealing.

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

Joint probability of observing (X, Y)
X ↓ / Y →01X alone
01/201/2
101/21/2
Y alone1/21/21

H = 0: the observations are equal. X ⊕ Y recovers 0 exactly.

CK-01 / Exact finite counterexample

The pair discloses the whole bit.

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

The least cost.
Subject to useful, private operation.

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.

Inputs still needed

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 15 unresolved fields. Filling them in does not certify their truth.

Start the deployment worksheet ↗

Evidence the optimum needs

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.

A practical project may choose a bounded-leakage target instead. State its metric, confidence, sensor class, horizon and utility tradeoff explicitly. Do not label “below our detection limit” as “no channel.”

05 / Useful negative knowledge

Four shortcuts,
four decisive witnesses.

These counterexamples reject specific claims. They neither prove physical containment impossible nor identify an optimal real machine.

CK-01Secret-independent marginal observations imply a secret-independent joint observation.

Outcome: refuted by a finite witness.

Each coordinate is uniform for either secret. The XOR of the observed pair recovers the secret exactly.

[
  {
    "secret": 0,
    "outcomes": [
      {
        "pair": [
          0,
          0
        ],
        "probability": "1/2"
      },
      {
        "pair": [
          1,
          1
        ],
        "probability": "1/2"
      }
    ]
  },
  {
    "secret": 1,
    "outcomes": [
      {
        "pair": [
          0,
          1
        ],
        "probability": "1/2"
      },
      {
        "pair": [
          1,
          0
        ],
        "probability": "1/2"
      }
    ]
  }
]
CK-02Whitespace normalization and equal output lengths remove all discretionary output channels.

Outcome: refuted by a finite witness.

A one-bit choice remains between accepted headers. Canonical release must remove every unauthorized choice, including semantic alternatives.

{
  "authorized_numeric_answer": 42,
  "accepted_variants": [
    "Answer: 42.",
    "Result: 42."
  ],
  "normalized_outputs": [
    "Answer: 42.",
    "Result: 42."
  ],
  "same_length": true
}
CK-03A silent shutdown is feasible under a strictly positive service floor.

Outcome: refuted by a finite witness.

Require useful service in the optimization contract. This is an abstract example, not a claim that powered-off hardware cannot leak.

{
  "abstract_shutdown_trace": [],
  "service": 0,
  "minimum_service": 1,
  "feasible": false
}
CK-04The same abstract plan minimizes every positive resource-cost weighting.

Outcome: refuted by a finite witness.

Even with fixed security and utility premises, changing the objective can change the optimum.

{
  "illustrative_vectors": {
    "A": [
      1,
      5
    ],
    "B": [
      4,
      1
    ]
  },
  "scenarios": [
    {
      "weights": [
        1,
        1
      ],
      "costs": {
        "A": 6,
        "B": 5
      },
      "unique_optimum": "B"
    },
    {
      "weights": [
        5,
        1
      ],
      "costs": {
        "A": 10,
        "B": 21
      },
      "unique_optimum": "A"
    }
  ],
  "scope": "Counterexample to a cost-independent optimizer over all positive weightings. No hardware optimum is inferred."
}

Replay this extension

Python standard library · 8 tests · Exact finite arithmetic

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

06 / Continue the work

One boundary. One falsifier.
One replayable result.

For researchers

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.

For mathematicians

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

Evidence for the paths.
Obligations for the controls.

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.

  1. NIST glossary: covert channel ↗

    Terminology for unauthorized communication between cooperating entities.

  2. NIST SP 800-53 Rev. 5: SC-31, PE-19, SI-11 ↗

    Channel analysis, deployment-specific bandwidth assessment, physical leakage and error-message obligations.

  3. Ge et al.: Time Protection, the Missing OS Abstraction ↗

    Time protection addresses shared microarchitectural state beyond memory access control.

  4. seL4: What the proofs assume ↗

    Confidentiality coverage is limited to modeled information channels; hardware and DMA assumptions remain explicit.

  5. Taram et al.: SecSMT (USENIX Security 2022) ↗

    Shared SMT pipeline resources can carry contention-based covert channels.

  6. Naghibijouybari et al.: Rendered Insecure (CCS 2018) ↗

    GPU sharing, memory APIs, counters and timing provided demonstrated leakage paths on tested devices.

  7. RFC 4303: IP Encapsulating Security Payload, section 2.7 ↗

    Traffic-flow confidentiality needs consideration of lengths and traffic patterns in addition to encrypted content.

  8. Guri: AIR-FI ↗

    Demonstrated radio emissions from memory activity on air-gapped computers.

  9. Guri et al.: MAGNETO ↗

    Demonstrated CPU-generated magnetic signaling to nearby sensors.

  10. Guri et al.: Fansmitter ↗

    Demonstrated acoustic signaling using fans on speakerless computers.

  11. Guri et al.: LED-it-GO ↗

    Demonstrated optical signaling using storage activity indicators.

  12. Guri et al.: PowerHammer ↗

    Demonstrated conducted signaling through power lines.

  13. Guri: AiR-ViBeR ↗

    Demonstrated surface vibration signaling.

  14. Guri et al.: BitWhisper ↗

    Demonstrated thermal signaling between nearby compromised computers.

  15. Halderman et al.: Lest We Remember (USENIX Security 2008) ↗

    Memory remanence can outlive an operating session; this is related leakage, not itself a claim of covert collusion.

  16. This lab: explicit model and contracts ↗

    The original digital and quantized-thermal assumptions, with limits stated explicitly.