Strips EXIF, GPS, camera data, and comments from JPEG images crossing a security boundary. Only pixel data passes through. Operates inline between Linux VMs at wire speed using the same VM diode architecture.
+-------------------------------+ +-------------------------------+
| vmm_high | | vmm_low |
| (JPEG source) | | (JPEG sink) |
| (pri 101) | | (pri 101) |
| +-------------------------+ | | +-------------------------+ |
| | vm_high (Linux, pri 100)| | | | vm_low (Linux, pri 99) | |
| | guest_ram: 256MB | | | | guest_ram: 256MB | |
| +-------------------------+ | | +-------------------------+ |
+---------------+--------------+ +---------------+---------------+
| |
net_high_to_filter net_filter_to_low
(2MB ring) (2MB ring)
| |
+-----------------+ +--------------------+
| |
+---------+----+---------+
| jpeg_filter |
| (trusted, pri 200) |
| |
| STRIPS: EXIF, GPS, |
| APP1-15, COM |
| KEEPS: SOI, SOF, |
| DHT, DQT, SOS, EOI |
+------------------------+
Only pixel data crosses the boundary.
All metadata is removed by the trusted filter.
| Segment | Marker | Action | Reason |
|---|---|---|---|
| SOI | 0xFFD8 | PASS | Start of image (required) |
| SOF | 0xFFC0 | PASS | Frame header (image dimensions, channels) |
| DHT | 0xFFC4 | PASS | Huffman tables (needed for decoding) |
| DQT | 0xFFDB | PASS | Quantisation tables (needed for decoding) |
| SOS | 0xFFDA | PASS | Start of scan + compressed pixel data |
| EOI | 0xFFD9 | PASS | End of image (required) |
| APP1 (EXIF) | 0xFFE1 | STRIP | Camera info, GPS coordinates, timestamps |
| APP2-APP15 | 0xFFE2-EF | STRIP | ICC profiles, extensions, vendor data |
| COM | 0xFFFE | STRIP | Comments (may contain sensitive text) |
The system uses the same VM diode architecture as the Linux VM Data Diode, but the trusted intermediary parses JPEG data instead of forwarding raw Ethernet frames. The filter walks the JPEG segment structure and only emits segments that contain pixel data.
<?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_filter" size="0x200_000" /> <memory_region name="net_filter_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_filter" 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_filter_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="jpeg_filter" priority="200"> <program_image path="jpeg_filter.elf" /> <map mr="net_high_to_filter" vaddr="0x4_000_000" perms="rw" setvar_vaddr="net_in_vaddr" /> <map mr="net_filter_to_low" vaddr="0x5_000_000" perms="rw" setvar_vaddr="net_out_vaddr" /> </protection_domain> <channel><end pd="vmm_high" id="2" /><end pd="jpeg_filter" id="1" /></channel> <channel><end pd="jpeg_filter" id="2" /><end pd="vmm_low" id="2" /></channel> </system>
/* JPEG segment markers */ #define JPEG_SOI 0xFFD8 /* Start of Image */ #define JPEG_EOI 0xFFD9 /* End of Image */ #define JPEG_SOS 0xFFDA /* Start of Scan */ #define JPEG_APP1 0xFFE1 /* EXIF / GPS data */ #define JPEG_COM 0xFFFE /* Comment */ static int is_safe_marker(uint16_t marker) { /* Allow only structural segments needed for decoding */ switch (marker) { case 0xFFD8: /* SOI */ case 0xFFC0: /* SOF0 */ case 0xFFC4: /* DHT */ case 0xFFDB: /* DQT */ case 0xFFDA: /* SOS */ case 0xFFD9: /* EOI */ return 1; default: return 0; /* Strip everything else */ } } size_t filter_jpeg(const uint8_t *in, size_t in_len, uint8_t *out, size_t out_cap) { size_t r = 0, w = 0; while (r < in_len - 1) { uint16_t marker = (in[r] << 8) | in[r+1]; if (is_safe_marker(marker)) { /* Copy safe segment to output */ size_t seg_len = get_segment_length(in, r, in_len); memcpy(out + w, in + r, seg_len); w += seg_len; r += seg_len; } else { /* Skip unsafe segment (EXIF, GPS, COM, etc.) */ r += get_segment_length(in, r, in_len); } } return w; }
The JPEG filter uses the same one-way channel topology as the data diode.
The filter PD's process receives JPEG data from HIGH, calls the C
metadata-stripping function (which transforms the buffer contents in place),
and forwards the clean image to LOW. ChorFi's c?x → c!x
pattern handles this naturally since x is a buffer reference
whose contents the C event modifies.
// Network ring buffers (2MB each) MemoryRegion net_high_to_filter(0x200_000); MemoryRegion net_filter_to_low(0x200_000); // Protection domains (VMMs + trusted filter) ProtectionDomain vmm_high(101); ProtectionDomain vmm_low(101); ProtectionDomain jpeg_filter(200); // One-way channels: HIGH -> filter -> LOW Chan h2f = vmm_high --> jpeg_filter; h2f.set_buffer(net_high_to_filter); Chan f2l = jpeg_filter --> vmm_low; f2l.set_buffer(net_filter_to_low); // System composition System = vmm_high ||| vmm_low ||| jpeg_filter;
import "jpeg_filter.c" as jf; () : jf.init(); // Receive JPEG from HIGH, strip metadata in C, // forward clean image to LOW Process: Notified(): h2f?jpeg -> jf.strip_metadata(jpeg) -> f2l!jpeg -> Notified();
// Security labels enforce one-way image flow High MemoryRegion net_high_to_filter(0x200_000); Low MemoryRegion net_filter_to_low(0x200_000); // Filter reads High (raw JPEG), writes Low (clean JPEG) High Mapping in_buf(net_high_to_filter, "r"); // OK Low Mapping out_buf(net_filter_to_low, "rw"); // OK // No reverse path — metadata can never flow back // Low Mapping leak(net_high_to_filter, "rw"); // ERROR!
What the compiler verifies:
unidirectional channels (-->), no reverse path from vmm_low to vmm_high,
and information flow labels prevent any data flowing back. The JPEG segment
parsing and metadata stripping are computation events — they
transform the buffer contents but don't affect the communication topology
that ChorFi verifies.