A probabilistic downgrader that buffers, reorders, and adds timing jitter to messages crossing security boundaries. Same topology as a data diode, but with active timing channel mitigation that defeats covert channels simple diodes leave open.
+----------------+ +----------------+
| domain_high | | domain_low |
| (pri 100) | | (pri 100) |
+-------+--------+ +--------+-------+
| |
high_to_pump pump_to_low
(write only) (read only)
| |
+-------------------+ +-------------------+---+
| |
+--------+----+--------+
| nrl_pump |
| (trusted, pri 200) |
| |
| [batch: 4 msgs] |
| [Fisher-Yates] |
| [random jitter] |
+----------------------+
HIGH ---> LOW only. Timing correlations broken by
batching, reordering, and pseudo-random delay.
The system description is identical in topology to a data diode. The pump logic — batching, reordering, and jitter — lives entirely within the nrl_pump protection domain's C implementation.
<?xml version="1.0" encoding="UTF-8"?> <system> <memory_region name="high_to_pump" size="0x1_000" /> <memory_region name="pump_to_low" size="0x1_000" /> <protection_domain name="domain_high" priority="100"> <program_image path="domain_high.elf" /> <map mr="high_to_pump" vaddr="0x4_000_000" perms="rw" setvar_vaddr="outbox_vaddr" /> </protection_domain> <protection_domain name="nrl_pump" priority="200"> <program_image path="nrl_pump.elf" /> <map mr="high_to_pump" vaddr="0x4_000_000" perms="rw" setvar_vaddr="inbound_vaddr" /> <map mr="pump_to_low" vaddr="0x5_000_000" perms="rw" setvar_vaddr="outbound_vaddr" /> </protection_domain> <protection_domain name="domain_low" priority="100"> <program_image path="domain_low.elf" /> <map mr="pump_to_low" vaddr="0x4_000_000" perms="rw" setvar_vaddr="inbox_vaddr" /> </protection_domain> <channel><end pd="domain_high" id="1" /><end pd="nrl_pump" id="1" /></channel> <channel><end pd="nrl_pump" id="2" /><end pd="domain_low" id="1" /></channel> </system>
#define BATCH_SIZE 4 static msg_t batch[BATCH_SIZE]; static int batch_count = 0; /* Fisher-Yates shuffle to destroy ordering correlations */ static void shuffle_batch(void) { for (int i = BATCH_SIZE - 1; i > 0; i--) { int j = prng_next() % (i + 1); msg_t tmp = batch[i]; batch[i] = batch[j]; batch[j] = tmp; } } void notified(microkit_channel ch) { if (ch == HIGH_CH) { batch[batch_count++] = read_msg(inbound_vaddr); if (batch_count == BATCH_SIZE) { shuffle_batch(); add_jitter(prng_next() % MAX_JITTER); for (int i = 0; i < BATCH_SIZE; i++) write_msg(outbound_vaddr, batch[i]); microkit_notify(LOW_CH); batch_count = 0; } } }
The NRL Pump is topologically identical to the data diode — HIGH → PUMP → LOW with two one-way channels and no backward path. The batching, Fisher-Yates reordering, and timing jitter all live within the C implementation imported by the pump PD. Fiducia verifies the structural flow guarantee.
// Shared memory buffers MemoryRegion high_to_pump(0x1_000); MemoryRegion pump_to_low(0x1_000); // Protection domains ProtectionDomain domain_high(100); ProtectionDomain domain_low(100); ProtectionDomain nrl_pump(200); // One-way channels: HIGH -> pump -> LOW Chan h2p = domain_high --> nrl_pump; h2p.set_buffer(high_to_pump); Chan p2l = nrl_pump --> domain_low; p2l.set_buffer(pump_to_low); // System composition System = domain_high ||| domain_low ||| nrl_pump;
import "nrl_pump.c" as pump; () : pump.init(); // The pump receives from HIGH, applies batching/shuffle/jitter // in C, then forwards to LOW. The channel topology is identical // to a simple data diode. Process: Notified(): h2p?msg -> pump.batch_and_shuffle(msg) -> p2l!msg -> Notified();
// Security labels — same as data diode High MemoryRegion high_to_pump(0x1_000); Low MemoryRegion pump_to_low(0x1_000); // Pump reads High, writes Low — permitted High Mapping inbound(high_to_pump, "r"); // OK Low Mapping outbound(pump_to_low, "rw"); // OK // No reverse path — compile-time guarantee // Low Mapping leak(high_to_pump, "rw"); // ERROR!
What the compiler verifies: identical guarantees to the data diode — unidirectional channels, no reverse path, and information flow labels. The batching, Fisher-Yates shuffle, and jitter are computation events inside the pump PD's imported C code, not communication patterns, so they don't affect the choreographic verification.