Framebuffer Compositor

Architecture

System Topology — Fan-In Pattern

  +--------------+   +--------------+   +---------------+
  | domain_red   |   | domain_blue  |   | domain_green  |
  |  (pri 100)   |   |  (pri 100)   |   |  (pri 100)    |
  +------+-------+   +------+-------+   +-------+-------+
         |                   |                   |
      fb_red              fb_blue            fb_green
     (write)              (write)             (write)
         |                   |                   |
         +-------------------+-------------------+
                             |
                    +--------+--------+
                    |   compositor    |
                    | (trusted, 200)  |
                    |  reads all FBs  |
                    +-----------------+

  Each domain writes ONLY to its own framebuffer.
  Only the compositor reads all three.
  Trusted border decorations added by compositor.

4

Protection Domains

3

Memory Regions

3

Channels

Security Properties

Write-only framebuffers — Each domain can only write to its own framebuffer region
Trusted compositor reads all — Only the compositor PD has read access to all framebuffers
Trusted border decorations — Visual security indicators drawn by compositor cannot be spoofed by any domain
No shared memory between domains — No domain pair shares any memory region

Current Implementation

seL4 Microkit + C

Three domain PDs each write to their own framebuffer region. The compositor PD maps all three regions and composites them into a final display output with trusted border decorations indicating the security level of each region.

System Description framebuffer_compositor.system

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <memory_region name="fb_red" size="0x1_000" />
    <memory_region name="fb_blue" size="0x1_000" />
    <memory_region name="fb_green" size="0x1_000" />

    <protection_domain name="domain_red" priority="100">
        <program_image path="domain_red.elf" />
        <map mr="fb_red" vaddr="0x4_000_000" perms="rw" setvar_vaddr="fb_vaddr" />
    </protection_domain>
    <protection_domain name="domain_blue" priority="100">
        <program_image path="domain_blue.elf" />
        <map mr="fb_blue" vaddr="0x4_000_000" perms="rw" setvar_vaddr="fb_vaddr" />
    </protection_domain>
    <protection_domain name="domain_green" priority="100">
        <program_image path="domain_green.elf" />
        <map mr="fb_green" vaddr="0x4_000_000" perms="rw" setvar_vaddr="fb_vaddr" />
    </protection_domain>

    <protection_domain name="compositor" priority="200">
        <program_image path="compositor.elf" />
        <map mr="fb_red" vaddr="0x4_000_000" perms="rw" setvar_vaddr="fb_red_vaddr" />
        <map mr="fb_blue" vaddr="0x5_000_000" perms="rw" setvar_vaddr="fb_blue_vaddr" />
        <map mr="fb_green" vaddr="0x6_000_000" perms="rw" setvar_vaddr="fb_green_vaddr" />
    </protection_domain>

    <channel><end pd="domain_red" id="1" /><end pd="compositor" id="1" /></channel>
    <channel><end pd="domain_blue" id="1" /><end pd="compositor" id="2" /></channel>
    <channel><end pd="domain_green" id="1" /><end pd="compositor" id="3" /></channel>
</system>

Key Code Highlight compositor.c

void notified(microkit_channel ch) {
    /* Read all framebuffers and composite */
    composite_region(fb_red_vaddr,   0, 0,   REGION_W, REGION_H);
    composite_region(fb_blue_vaddr,  REGION_W, 0,   REGION_W, REGION_H);
    composite_region(fb_green_vaddr, 0, REGION_H, REGION_W, REGION_H);

    /* Draw trusted border decorations (cannot be spoofed) */
    draw_border(0, 0,   REGION_W, REGION_H, COLOR_RED,   "SECRET");
    draw_border(REGION_W, 0,   REGION_W, REGION_H, COLOR_BLUE,  "OFFICIAL");
    draw_border(0, REGION_H, REGION_W, REGION_H, COLOR_GREEN, "PUBLIC");
}

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 fan-in compositor topology as a choreographic specification with compile-time guarantees on memory isolation and information flow.

Multiple one-way channels — Each domain-to-compositor link expressed as a unidirectional channel in the system declaration
Read-only mappings with security labels — Fiducia's type system will enforce that domains can only write to their own framebuffer
Fan-in composition — The compositor process composes inputs from all domains using parallel composition operators