Residual Data

Domain Switch Flush

Zeroes all shared workspace buffers on every domain switch, verified clean before the new domain activates. Prevents covert channels through residual state in shared memory between SECRET and OFFICIAL domains.

Architecture
System Topology — Shared Workspace with Flush
  +------------------+                        +-------------------+
  |  domain_secret   |                        |  domain_official  |
  |    (pri 100)     |                        |    (pri 100)      |
  +--------+---------+                        +---------+---------+
           |                                            |
       secret_buf                                 official_buf
           |                                            |
           +--------------------+  +--------------------+
                                |  |
                      +---------+--+---------+
                      |  switch_controller   |
                      |  (trusted, pri 200)  |
                      |                      |
                      |  maps: secret_buf    |
                      |        official_buf  |
                      |        workspace     |
                      +----------------------+
                                |
                           workspace
                        (zeroed on switch)

  Workspace is zeroed completely on every domain switch.
  Verified clean before new domain activates.
3
Protection Domains
3
Memory Regions
2
Channels

Security Properties

Current Implementation

seL4 Microkit + C

The switch controller runs at priority 200 with access to both domain buffers and the shared workspace. On receiving a switch notification, it zeroes the workspace and verifies the result before notifying the new active domain.

System Description domain_switch_flush.system 
<?xml version="1.0" encoding="UTF-8"?>
<system>
    <memory_region name="secret_buf" size="0x1_000" />
    <memory_region name="official_buf" size="0x1_000" />
    <memory_region name="workspace" size="0x1_000" />

    <protection_domain name="domain_secret" priority="100">
        <program_image path="domain_secret.elf" />
        <map mr="secret_buf" vaddr="0x4_000_000" perms="rw" setvar_vaddr="secret_buf_vaddr" />
    </protection_domain>

    <protection_domain name="domain_official" priority="100">
        <program_image path="domain_official.elf" />
        <map mr="official_buf" vaddr="0x4_000_000" perms="rw" setvar_vaddr="official_buf_vaddr" />
    </protection_domain>

    <protection_domain name="switch_controller" priority="200">
        <program_image path="switch_controller.elf" />
        <map mr="secret_buf" vaddr="0x4_000_000" perms="rw" setvar_vaddr="secret_buf_vaddr" />
        <map mr="official_buf" vaddr="0x5_000_000" perms="rw" setvar_vaddr="official_buf_vaddr" />
        <map mr="workspace" vaddr="0x6_000_000" perms="rw" setvar_vaddr="workspace_vaddr" />
    </protection_domain>

    <channel><end pd="domain_secret" id="1" /><end pd="switch_controller" id="1" /></channel>
    <channel><end pd="domain_official" id="1" /><end pd="switch_controller" id="2" /></channel>
</system>
Key Code Highlight switch_controller.c 
typedef enum { DOMAIN_SECRET, DOMAIN_OFFICIAL } domain_t;
static domain_t active = DOMAIN_SECRET;

static void flush_workspace(void) {
    /* Zero entire workspace region */
    memset((void *)workspace_vaddr, 0, WORKSPACE_SIZE);
}

static int verify_clean(void) {
    /* Verify every byte is zero before allowing new domain */
    volatile uint8_t *p = (volatile uint8_t *)workspace_vaddr;
    for (size_t i = 0; i < WORKSPACE_SIZE; i++) {
        if (p[i] != 0) return 0;
    }
    return 1;
}

void notified(microkit_channel ch) {
    flush_workspace();
    assert(verify_clean());  /* Must be clean before switch */

    active = (active == DOMAIN_SECRET)
        ? DOMAIN_OFFICIAL : DOMAIN_SECRET;

    microkit_channel target = (active == DOMAIN_SECRET)
        ? SECRET_CH : OFFICIAL_CH;
    microkit_notify(target);
}
Full implementation available on request. Contact us at alex.potanin@anu.edu.au.
Coming Soon

Fiducia Specification

The Fiducia version of this system will express the domain switch and workspace flush as verified events in a CSP-style process specification. The state machine transitions become provably correct process algebra terms.

  • Workspace flush as verified process event — The flush operation becomes a first-class event in the process specification, not just a C function call
  • State machine as process algebra — The SECRET/OFFICIAL state transitions are expressed as guarded choice, proven deadlock-free by the type system
  • Verified clean invariant — The workspace cleanliness property becomes a compile-time guarantee rather than a runtime assertion