Ethernet-level data diode between two full Linux virtual machines running on seL4. Frames flow HIGH to LOW only through a trusted bridge. The VMs are completely isolated by seL4 capabilities — no shared memory, no shared devices.
+-------------------------------+ +-------------------------------+
| vmm_high | | vmm_low |
| (pri 101) | | (pri 101) |
| +-------------------------+ | | +-------------------------+ |
| | vm_high (Linux, pri 100)| | | | vm_low (Linux, pri 99) | |
| | guest_ram: 256MB | | | | guest_ram: 256MB | |
| | UART, GIC | | | | GIC | |
| +-------------------------+ | | +-------------------------+ |
+---------------+--------------+ +---------------+---------------+
| |
net_high_to_diode net_diode_to_low
(2MB ring) (2MB ring)
| |
+-----------------+ +--------------------+
| |
+---------+----+---------+
| data_diode |
| (trusted, pri 200) |
| |
| Ethernet frames: |
| HIGH ----> LOW only |
+------------------------+
VMs are completely isolated by seL4 capabilities.
No reverse path from LOW to HIGH exists.
Each Linux VM runs inside a VMM protection domain with 256MB of guest RAM, a virtual CPU, and mapped hardware (UART, GIC). The data diode PD sits between them, reading Ethernet frames from the HIGH ring buffer and writing them to the LOW ring buffer.
<?xml version="1.0" encoding="UTF-8"?> <system> <memory_region name="guest_ram_high" size="0x10000000" page_size="0x200_000" phys_addr="0x40000000" /> <memory_region name="guest_ram_low" size="0x10000000" page_size="0x200_000" phys_addr="0x50000000" /> <memory_region name="uart" size="0x1_000" phys_addr="0x9_000_000" /> <memory_region name="gic_vcpu" size="0x1_000" phys_addr="0x8040000" /> <memory_region name="net_high_to_diode" size="0x200_000" /> <memory_region name="net_diode_to_low" size="0x200_000" /> <protection_domain name="vmm_high" priority="101"> <program_image path="vmm_high.elf" /> <map mr="guest_ram_high" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" /> <map mr="net_high_to_diode" vaddr="0x6_000_000" perms="rw" setvar_vaddr="net_buf_vaddr" /> <virtual_machine name="vm_high" priority="100"> <vcpu id="0" /> <map mr="guest_ram_high" vaddr="0x40000000" perms="rwx" /> <map mr="uart" vaddr="0x9000000" perms="rw" cached="false" /> <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" cached="false" /> </virtual_machine> <irq irq="33" id="1" /> </protection_domain> <protection_domain name="vmm_low" priority="101"> <program_image path="vmm_low.elf" /> <map mr="guest_ram_low" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" /> <map mr="net_diode_to_low" vaddr="0x6_000_000" perms="rw" setvar_vaddr="net_buf_vaddr" /> <virtual_machine name="vm_low" priority="99"> <vcpu id="0" /> <map mr="guest_ram_low" vaddr="0x40000000" perms="rwx" /> <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" cached="false" /> </virtual_machine> </protection_domain> <protection_domain name="data_diode" priority="200"> <program_image path="data_diode.elf" /> <map mr="net_high_to_diode" vaddr="0x4_000_000" perms="rw" setvar_vaddr="net_in_vaddr" /> <map mr="net_diode_to_low" vaddr="0x5_000_000" perms="rw" setvar_vaddr="net_out_vaddr" /> </protection_domain> <channel><end pd="vmm_high" id="2" /><end pd="data_diode" id="1" /></channel> <channel><end pd="data_diode" id="2" /><end pd="vmm_low" id="2" /></channel> </system>
/* Ethernet frame forwarding: HIGH -> LOW only */ void notified(microkit_channel ch) { if (ch == HIGH_CH) { struct net_ring *in = (struct net_ring *)net_in_vaddr; struct net_ring *out = (struct net_ring *)net_out_vaddr; while (ring_has_data(in)) { struct eth_frame *frame = ring_dequeue(in); /* Forward frame: HIGH -> LOW (one-way only) */ ring_enqueue(out, frame->data, frame->len); } microkit_notify(LOW_CH); } /* No handler for LOW_CH -- reverse path does not exist */ }
The inter-PD choreography between vmm_high, data_diode, and vmm_low is directly expressible in ChorFi today. The one-way channel topology is identical to the basic data diode — Fiducia verifies that no reverse path exists, even with full Linux VMs behind the VMMs.
// Network ring buffers (2MB each) MemoryRegion net_high_to_diode(0x200_000); MemoryRegion net_diode_to_low(0x200_000); // Protection domains (VMMs + trusted diode) ProtectionDomain vmm_high(101); ProtectionDomain vmm_low(101); ProtectionDomain data_diode(200); // One-way channels: HIGH -> diode -> LOW Chan h2d = vmm_high --> data_diode; h2d.set_buffer(net_high_to_diode); Chan d2l = data_diode --> vmm_low; d2l.set_buffer(net_diode_to_low); // System composition System = vmm_high ||| vmm_low ||| data_diode;
import "data_diode.c" as dd; () : dd.init(); Process: Notified(): h2d?frame -> d2l!frame -> Notified();
// Security labels enforce one-way flow at the type level High MemoryRegion net_high_to_diode(0x200_000); Low MemoryRegion net_diode_to_low(0x200_000); // Diode reads High, writes Low — permitted (downgrade) High Mapping in_buf(net_high_to_diode, "r"); // OK Low Mapping out_buf(net_diode_to_low, "rw"); // OK // Reverse would be a compile-time ERROR: // Low Mapping leak(net_high_to_diode, "rw"); // High -> Low!
What the compiler verifies:
unidirectional channels (-->), no reverse path from vmm_low to vmm_high,
information flow labels prevent High→Low leaks, and the |||
composition ensures all PDs are accounted for. The VM guest RAM and device
passthrough remain in the Microkit system description — Fiducia
orchestrates the inter-PD communication layer.