Enforces strict one-way information flow between HIGH and LOW security domains through a trusted intermediary. The diode applies policy checks and audit logging—no data ever flows backwards. This is the canonical Fiducia example from the ChorFi paper.
Guarantee One-way Data Flow
===========================
+-----------+ high_to_diode +------------+ diode_to_low +-----------+
| domain | ------ ch1 ------> | data | ------ ch2 ------> | domain |
| HIGH | | diode | | LOW |
| pri = 100 | | pri = 200 | | pri = 100 |
+-----------+ +------------+ +-----------+
(TRUSTED)
No shared memory or channel between domain_high and domain_low.
All information must pass through the trusted data_diode.
The data diode is currently implemented as three C protection domains running on seL4 Microkit. The system description XML defines the architecture, and seL4 capabilities enforce the isolation.
<!-- Shared memory: domain_high writes, data_diode reads --> <memory_region name="high_to_diode" size="0x1_000" /> <memory_region name="diode_to_low" size="0x1_000" /> <protection_domain name="domain_high" priority="100"> <program_image path="domain_high.elf" /> <map mr="high_to_diode" vaddr="0x4_000_000" perms="rw" /> </protection_domain> <protection_domain name="data_diode" priority="200"> <program_image path="data_diode.elf" /> <map mr="high_to_diode" vaddr="0x4_000_000" perms="rw" /> <map mr="diode_to_low" vaddr="0x5_000_000" perms="rw" /> </protection_domain> <protection_domain name="domain_low" priority="100"> <program_image path="domain_low.elf" /> <map mr="diode_to_low" vaddr="0x4_000_000" perms="rw" /> </protection_domain> <!-- Channels: HIGH -> diode -> LOW --> <channel> <end pd="domain_high" id="1" /> <end pd="data_diode" id="1" /> </channel> <channel> <end pd="data_diode" id="2" /> <end pd="domain_low" id="1" /> </channel>
void notified(microkit_channel ch) { if (ch == CH_HIGH) { int len = diode_buf_read(in_buf, msg, 255); /* Apply policy check */ if (!policy_check(msg, len)) { microkit_dbg_puts("[DIODE] BLOCKED by policy!\n"); return; } /* Forward to low side (the one-way transfer) */ diode_buf_write(out_buf, msg, len); microkit_notify(CH_LOW); } /* We deliberately ignore any notification from CH_LOW. * domain_low has no channel carrying data back to HIGH. */ }
In Fiducia, the entire data diode architecture is expressed in two concise files. The compiler verifies information flow security, channel directionality, and deadlock freedom—properties that in the C version are enforced only by careful manual discipline.
// Memory regions used as channel buffers MemoryRegion eth_outer_output(0x200_000); MemoryRegion eth_inner_input(0x200_000); // Protection domains: (priority, irq, budget, period) ProtectionDomain eth_outer(99, 159, 1000, 100_000); ProtectionDomain eth_inner(199, 155); ProtectionDomain dd(100); // One-way SPSC channels Chan o2d = eth_outer --> dd; o2d.set_buffer(eth_outer_output); Chan d2i = dd --> eth_inner; d2i.set_buffer(eth_inner_input); // System composition System = eth_outer ||| eth_inner ||| dd;
import "ddiode.c" as dd; () : dd.init(); Process: Notified(): o2d?pkt -> d2i!pkt -> Notified();
// Add security labels — the compiler catches leaks Low MemoryRegion eth_outer_output(0x200_000); High MemoryRegion eth_inner_input(0x200_000); Low Mapping input_buf(eth_outer_output, "r"); // OK: read Low High Mapping output_buf(eth_inner_input, "rw"); // OK: write High // This would be a compile-time ERROR: // Low Mapping leak(eth_inner_input, "r"); // High -> Low!
What the compiler verifies:
unidirectional channel flow (--> not <->),
information flow labels prevent High→Low leaks,
well-typed choreography guarantees deadlock freedom,
and the ||| composition ensures all PDs are accounted for.