Clipboard Guard — Fiducia

Architecture

  Managed Cross-Domain Clipboard
  ==============================

  +-----------+    high_to_guard    +-----------+    guard_to_low    +-----------+
  |  domain   | ------ ch1 ------> | clipboard |  --- ch2 -------> |  domain   |
  |   HIGH    |                     |   guard   |    (if approved)  |    LOW    |
  | pri = 100 |                     | pri = 200 |                   | pri = 100 |
  +-----------+                     +-----------+                   +-----------+
                                    (TRUSTED)
                                    Policy: reject
                                    "TOP SECRET"
                                    "CLASSIFIED"
                                    "SCI"

3

Protection Domains

2

Memory Regions

2

Channels

Policy

Content-based

Content inspection: Every clipboard item is scanned for forbidden keywords before crossing
Reject or forward: The guard makes a binary decision — approve or block
Audit trail: Approved/rejected counts and reasons logged for every operation
No direct path: HIGH and LOW have no shared memory or channel — all flow through the guard

Current Implementation

seL4 Microkit + C

The clipboard guard is implemented as a trusted protection domain that reads clipboard items from HIGH, applies keyword scanning, and forwards only approved content to LOW.

System Descriptionclipboard_guard.system

<memory_region name="high_to_guard" size="0x1_000" />
<memory_region name="guard_to_low" size="0x1_000" />

<protection_domain name="domain_high" priority="100">
    <map mr="high_to_guard" vaddr="0x4_000_000" perms="rw" />
</protection_domain>

<protection_domain name="clipboard_guard" priority="200">
    <map mr="high_to_guard" vaddr="0x4_000_000" perms="rw" />
    <map mr="guard_to_low" vaddr="0x5_000_000" perms="rw" />
</protection_domain>

<protection_domain name="domain_low" priority="100">
    <map mr="guard_to_low" vaddr="0x4_000_000" perms="rw" />
</protection_domain>

<channel>
    <end pd="domain_high" id="1" />
    <end pd="clipboard_guard" id="1" />
</channel>
<channel>
    <end pd="clipboard_guard" id="2" />
    <end pd="domain_low" id="1" />
</channel>

Policy Enforcementclipboard_guard.c

static int policy_check(const char *msg, int len) {
    for (int k = 0; k < NUM_FORBIDDEN; k++) {
        if (clip_strstr(msg, len, forbidden_keywords[k]))
            return k;  /* Forbidden keyword found */
    }
    return -1;  /* Content is clean */
}

void notified(microkit_channel ch) {
    if (ch == CH_HIGH) {
        int len = clip_buf_read(in_buf, msg, 255);
        int forbidden_idx = policy_check(msg, len);

        if (forbidden_idx >= 0) {
            rejected_count++;
            /* REJECTED: contains forbidden keyword */
        } else {
            approved_count++;
            clip_buf_write(out_buf, msg, len);
            microkit_notify(CH_LOW);
            /* APPROVED: forwarded to LOW paste buffer */
        }
    }
}

Full C implementation with Makefile and QEMU runner available on request. Contact alex.potanin@anu.edu.au

Fiducia Specification

Content policy as guarded choice.

In Fiducia, the clipboard guard's approve/reject decision maps directly to ChorFi's external choice operator. The guard receives a clipboard item, evaluates the policy, and either forwards or drops it. The information flow type system ensures the one-way HIGH→LOW direction is enforced at compile time.

System Declarationclipboard.fis

// Memory regions
High MemoryRegion high_to_guard(0x1000);
Low  MemoryRegion guard_to_low(0x1000);

// Protection domains
ProtectionDomain domain_high(100);
ProtectionDomain clipboard_guard(200);
ProtectionDomain domain_low(100);

// One-way channels: HIGH -> guard -> LOW
Chan h2g = domain_high --> clipboard_guard;
    h2g.set_buffer(high_to_guard);
Chan g2l = clipboard_guard --> domain_low;
    g2l.set_buffer(guard_to_low);

System = domain_high ||| clipboard_guard ||| domain_low;

Guard Process with External Choiceclipboard_guard.fi

import "clipboard_guard.c" as guard;
() : guard.init();

Events:
  Event policy_check: guard.policy_check(item)

Process:
  Notified():
    h2g?item -> Check(item);

  Check(item):
    // External choice: approve or reject
    [ policy_check(item) ] g2l!item -> Notified()
    [ ]                    Skip      -> Notified();

What the compiler verifies: the [ ] external choice ensures exactly one branch is taken (no deadlock), information flow labels prevent High→Low leaks on the memory regions, and the one-way channels (-->) structurally prevent reverse data flow from LOW to HIGH.

Fiducia compiler and specification available on request. Contact alex.potanin@anu.edu.au