MLS Email Guard — Fiducia

Architecture

  Asymmetric Multi-Level Security Email
  =====================================

  +-----------+   secret_to_guard   +-----------+  guard_to_official  +-----------+
  |  domain   | ------  ch1 ------> |   mail    | ------- ch2 ------> |  domain   |
  |  SECRET   |                     |   guard   |                     | OFFICIAL  |
  | pri = 100 | <--- guard_to_    | pri = 200 | <--- official_to_ | pri = 100 |
  +-----------+      secret         +-----------+      guard          +-----------+
                  (unused: upgrade                  (BLOCKED: upgrade
                   not permitted)                    OFFICIAL->SECRET)

  Downgrade:  SECRET -> OFFICIAL    ALLOWED (with sanitisation)
  Upgrade:    OFFICIAL -> SECRET    ALWAYS BLOCKED

Protection Domains

Memory Regions

Channels

Asymmetric

Security Policy

Direction	Policy	Action
SECRET → OFFICIAL	ALLOWED	Sanitise: strip "CLASSIFIED:" prefix, add "[DOWNGRADED]" to subject
OFFICIAL → SECRET	BLOCKED	Rejected unconditionally — no upward flow without accreditation

Asymmetric flow: Downgrade permitted with sanitisation; upgrade always blocked
Email sanitisation: Classified markers stripped, downgrade label inserted
Architectural isolation: No direct path between SECRET and OFFICIAL
Audit logging: Every email decision (allowed/blocked) logged with direction

Current Implementation

seL4 Microkit + C

The mail guard uses bidirectional channels but enforces asymmetric policy: it reads from both domains but only forwards in the SECRET→OFFICIAL direction after sanitisation.

System Descriptionmls_email.system

<!-- 4 memory regions for bidirectional mailboxes -->
<memory_region name="secret_to_guard" size="0x1_000" />
<memory_region name="guard_to_secret" size="0x1_000" />
<memory_region name="official_to_guard" size="0x1_000" />
<memory_region name="guard_to_official" size="0x1_000" />

<protection_domain name="domain_secret" priority="100">
    <map mr="secret_to_guard" vaddr="0x4_000_000" perms="rw" />
    <map mr="guard_to_secret" vaddr="0x4_001_000" perms="rw" />
</protection_domain>

<protection_domain name="mail_guard" priority="200">
    <map mr="secret_to_guard"   vaddr="0x4_000_000" perms="rw" />
    <map mr="guard_to_secret"   vaddr="0x4_001_000" perms="rw" />
    <map mr="official_to_guard" vaddr="0x4_002_000" perms="rw" />
    <map mr="guard_to_official" vaddr="0x4_003_000" perms="rw" />
</protection_domain>

<protection_domain name="domain_official" priority="100">
    <map mr="official_to_guard" vaddr="0x4_000_000" perms="rw" />
    <map mr="guard_to_official" vaddr="0x4_001_000" perms="rw" />
</protection_domain>

<!-- Bidirectional channels (policy is asymmetric, not the channels) -->
<channel>
    <end pd="domain_secret" id="1" />
    <end pd="mail_guard" id="1" />
</channel>
<channel>
    <end pd="domain_official" id="1" />
    <end pd="mail_guard" id="2" />
</channel>

Asymmetric Policy Enforcementmail_guard.c

void notified(microkit_channel ch) {
    if (ch == CH_SECRET_GUARD) {
        /* SECRET -> OFFICIAL: downgrade allowed */
        int len = mail_buf_read(secret_in, email, 511);
        len = sanitise_for_downgrade(email, len, 511);
        /* Strips "CLASSIFIED:" prefix, adds "[DOWNGRADED]" */
        mail_buf_write(official_out, email, len);
        microkit_notify(CH_OFFICIAL_GUARD);
    }

    if (ch == CH_OFFICIAL_GUARD) {
        /* OFFICIAL -> SECRET: BLOCKED unconditionally */
        mail_buf_read(official_in, email, 511);
        microkit_dbg_puts("BLOCKED: upward flow not permitted\n");
        /* Message is consumed and discarded */
    }
}

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

Fiducia Specification

Asymmetric security enforced by the type system.

In Fiducia, the MLS email guard is the most compelling example of how the information flow type system catches errors that C cannot. The bidirectional channels carry notifications, but the High/Low labels on memory regions ensure that the compiler rejects any attempt to flow data upward from OFFICIAL to SECRET.

System Declarationmls_email.fis

// Memory regions with security labels
High MemoryRegion secret_to_guard(0x1000);
High MemoryRegion guard_to_secret(0x1000);
Low  MemoryRegion official_to_guard(0x1000);
Low  MemoryRegion guard_to_official(0x1000);

// Protection domains
ProtectionDomain domain_secret(100);
ProtectionDomain mail_guard(200);
ProtectionDomain domain_official(100);

// Channels: both domains communicate with guard
Chan sec = domain_secret <-> mail_guard;
Chan off = domain_official <-> mail_guard;

System = domain_secret ||| mail_guard ||| domain_official;

Mail Guard Processmail_guard.fi

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

// Mappings: the guard reads HIGH and writes LOW
High Mapping secret_in(secret_to_guard, "r");
Low  Mapping official_out(guard_to_official, "rw");

// This would be a compile-time ERROR:
// High Mapping upgrade(guard_to_secret, "rw");
//   with Low Mapping official_in(official_to_guard, "r");
//   -> the type system blocks Low data flowing to High mapping

Events:
  Event sanitise: guard.sanitise_for_downgrade(email)

Process:
  Notified():
    // Downgrade: SECRET -> OFFICIAL (allowed)
    sec?email -> sanitise(email) -> off!email -> Notified()
    // Upgrade attempts: consumed and discarded
    [ ] off?email -> Skip -> Notified();

Type System Catches Upward Flowcompile-time error

// If someone tried to write OFFICIAL data to SECRET's inbox:
Low  Mapping official_in(official_to_guard, "r");
High Mapping secret_out(guard_to_secret, "rw");

// The Fiducia compiler would reject this:
//   ERROR: Information flow violation
//   Low data from 'official_to_guard' cannot flow to
//   High mapping 'secret_out' without explicit declassification.
//
// In the C version, this protection relies entirely on the
// developer never writing such code. In Fiducia, the compiler
// catches it automatically.

What the compiler verifies: High/Low labels enforce that SECRET data only flows downward (to OFFICIAL) after explicit sanitisation. The bidirectional channels (<->) carry notifications, but the memory region labels ensure data can only move in the permitted direction. External choice in the process handles both incoming directions with the correct policy for each.

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