Trusted Input

Keyboard Switch

Routes HID keyboard input to one security domain at a time with complete buffer flush on domain switch. Keystrokes are delivered exclusively — no broadcast, no residual data leakage between SECRET and UNCLASSIFIED domains.

Architecture
System Topology
                          +------------------+
                          |    keyboard      |
                          |   (pri 100)      |
                          +--------+---------+
                                   |
                            kbd_to_switch
                                   |
                          +--------+---------+
                          |   kbd_switch     |
                          | (trusted, pri 200)|
                          +---+----------+---+
                              |          |
                       switch_to_a  switch_to_b
                              |          |
                    +---------+--+  +----+---------+
                    |  domain_a  |  |  domain_b    |
                    |  (SECRET)  |  | (UNCLASSIFIED)|
                    |  (pri 100) |  |  (pri 100)   |
                    +------------+  +--------------+

  No shared memory between domain_a and domain_b.
  kbd_switch has exclusive routing authority.
4
Protection Domains
3
Memory Regions
3
Channels

Security Properties

Current Implementation

seL4 Microkit + C

The system description defines four protection domains connected by three unidirectional shared memory channels. The trusted kbd_switch PD runs at priority 200 and has exclusive access to both outbound buffers.

System Description keyboard_switch.system 
<?xml version="1.0" encoding="UTF-8"?>
<system>
    <memory_region name="kbd_to_switch" size="0x1_000" />
    <memory_region name="switch_to_a" size="0x1_000" />
    <memory_region name="switch_to_b" size="0x1_000" />

    <protection_domain name="keyboard" priority="100">
        <program_image path="keyboard.elf" />
        <map mr="kbd_to_switch" vaddr="0x4_000_000" perms="rw" setvar_vaddr="outbox_vaddr" />
    </protection_domain>

    <protection_domain name="kbd_switch" priority="200">
        <program_image path="kbd_switch.elf" />
        <map mr="kbd_to_switch" vaddr="0x4_000_000" perms="rw" setvar_vaddr="inbound_vaddr" />
        <map mr="switch_to_a" vaddr="0x5_000_000" perms="rw" setvar_vaddr="outbound_a_vaddr" />
        <map mr="switch_to_b" vaddr="0x6_000_000" perms="rw" setvar_vaddr="outbound_b_vaddr" />
    </protection_domain>

    <protection_domain name="domain_a" priority="100">
        <program_image path="domain_a.elf" />
        <map mr="switch_to_a" vaddr="0x4_000_000" perms="rw" setvar_vaddr="inbox_vaddr" />
    </protection_domain>

    <protection_domain name="domain_b" priority="100">
        <program_image path="domain_b.elf" />
        <map mr="switch_to_b" vaddr="0x4_000_000" perms="rw" setvar_vaddr="inbox_vaddr" />
    </protection_domain>

    <channel>
        <end pd="keyboard" id="1" />
        <end pd="kbd_switch" id="1" />
    </channel>
    <channel>
        <end pd="kbd_switch" id="2" />
        <end pd="domain_a" id="2" />
    </channel>
    <channel>
        <end pd="kbd_switch" id="3" />
        <end pd="domain_b" id="3" />
    </channel>
</system>
Key Code Highlight kbd_switch.c 
static int active_domain = 0;  /* 0 = domain_a, 1 = domain_b */

static void flush_buffers(void) {
    /* Zero both outbound buffers on domain switch */
    memset((void *)outbound_a_vaddr, 0, BUF_SIZE);
    memset((void *)outbound_b_vaddr, 0, BUF_SIZE);
}

void notified(microkit_channel ch) {
    if (ch == SWITCH_CH) {
        flush_buffers();
        active_domain = !active_domain;
        log_switch_event(active_domain);
    } else if (ch == KBD_CH) {
        /* Route keystroke to active domain only */
        if (active_domain == 0)
            forward_to(outbound_a_vaddr, DOMAIN_A_CH);
        else
            forward_to(outbound_b_vaddr, DOMAIN_B_CH);
    }
}
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 keyboard switch as a choreographic specification with compile-time guarantees. The Fiducia compiler will verify the routing topology, buffer isolation, and domain exclusivity structurally — eliminating entire classes of implementation bugs.

  • External choice routing — Domain switch expressed as guarded external choice in CSP-style process algebra
  • Buffer flush as process event — The flush operation becomes a verified event in the process specification, not just a C function call
  • ProtectionDomain composition with ||| — Interleaved composition proves domain_a and domain_b can never interfere