seL4

Complete Guide to Building a Secure AI Inference System with seL4

Executive Summary

This report provides a comprehensive guide to constructing a secure AI inference system utilizing the seL4 microkernel. The system emphasizes isolation, mathematical proofs of correctness, and minimal attack surfaces to ensure high security and reliability for AI operations. The architecture is built from hardware up to application layers, incorporating key concepts like capabilities, protection domains, and inter-process communication (IPC). The guide includes step-by-step explanations, diagrams, boot sequences, runtime examples, and practical implementation phases.

Part 1: What We're Building

Imagine you're building a highly secure, isolated computer system that runs AI inference. Think of it like a bank vault with separate locked rooms - if someone breaks into one room, they can't access the others, and they definitely can't get to the vault itself.

The Vision: μlnference Stack

Traditional Computer Your Secure System

• Many apps running vs 3 isolated compartments
• Shared memory Each has own memory
• Apps can interfere Apps CANNOT interfere
• One crash = system down One crash = that room only

Part 2: The Architecture (Bottom to Top)

Let's build this from the hardware up to your AI application.

Layer 1: Hardware (The Foundation)

Physical Computer (x86_64/ARM/RISC-V)

• CPU, RAM, Storage, Network

This is your actual computer. Could be a PC, Raspberry Pi, or server.

Layer 2: seL4 Microkernel (The Security Guard)

seL4 Microkernel (~10,000 lines of code)   
Jobs:   
1. Manage memory access (capabilities)   
2. Schedule threads to run   
3. Enable secure communication (IPC)   
4. Handle hardware interrupts   
KEY: Mathematically proven bug-free!

What makes seL4 special:

• It's been mathematically proven to be correct (no other OS can claim this)
• It's tiny - only 10,000 lines vs Linux's $\sim 30$ million lines
• It does ONLY essential things; everything else runs in userspace

Think of it as: A minimalist security guard who:

• Only knows how to check IDs (capabilities)
• Doesn't try to do everyone's job
• Never makes mistakes (proven mathematically)

Layer 3: Protection Domains (PDs) (The Isolated Rooms)

Now here's where it gets interesting. Instead of having one big userspace where all programs run together (like Linux), you have completely separate rooms:

Each Protection Domain (PD) is like a sealed room in a vault:

- Root Task PD - The Manager's Office

。 First room that opens when system starts

• Has authority to create other rooms
  Distributes keys (capabilities) to other rooms
  Cannot be accessed by anyone else

- Inference PD - The AI Processing Room

• Contains your llama2.c code (4,000 lines)
• Loads and runs AI models
• Has memory for model weights
  Isolated: Even if llama2.c crashes or has a bug, it CANNOT affect other rooms

- BusyBox PD - The Control Room

• Contains your shell and utilities
• User interface for the system
• Can request AI inference from Inference PD
• Also isolated from everything else

Part 3: The Key Concepts (How Security Works)

Concept 1: Capabilities – The Unforgettable Keys

In traditional operating systems, security works like this:

if (user == "root") { // Allow access - but this can be faked! }

In seL4, security works with physical keys (capabilities):

Capability  $=$  Unforgettable Digital Key   
You can only do something if you have the key.   
You cannot:   
- Guess the key.   
- Steal the key.   
- Forge a fake key.   
- Use a key you don't have

Real-world analogy: Imagine a hotel:

• Traditional OS: You tell the front desk "I'm in room 301" and they believe you
• seL4: You must present a physical hotel keycard that only works on room 301

Example: Inference PD's Capabilities

Inference PD's Keyring

$\checkmark$ Key to its own memory pages
$\checkmark$ Key to IPC channel
$\checkmark$ Key to its own thread control

X NO key to BusyBox memory
X NO key to Root Task resources
X NO key to hardware devices

This means: Even if Irama2.c has a buffer overflow vulnerability, the attacker cannot access BusyBox's memory because they don't have the capability (key) to it!

Concept 2: CSpace - Your Personal Keyring

Every Protection Domain has a CSpace (Capability Space) - think of it as a keyring that holds all your keys:

CSpace = Array of Capability Slots

Inference PD's CSpace:

0	1	2	3	4	5	6	7
TCB	EP	MEM	MEM	MEM	-	-	-

$\leftarrow$ Slot numbers
← What's in each slot

Explanation:

• Slot 0 (TCB): Key to control your own thread (start/stop/configure)
• Slot 1(EP): Key to an IPC endpoint (communication channel)
• Slots 2-4 (MEM): Keys to memory pages (your code and data)
  • Slots 5-7: Empty (no capabilities here)

Important: You can only use capabilities that are in YOUR CSpace. If BusyBox PD's memory capability isn't in your CSpace, you literally cannot access it - the kernel will block you.

Concept 3: VSpace - Your Isolated Memory View

Each PD has its own VSpace (Virtual Address Space) - its own isolated view of memory:

Inference PD's View	BusyBox PD's View
0x1000: llama2.c	0x1000: shell
code	code
0x2000: Model	0x2000: Command
weights	history
0x3000: Stack	0x3000: Stack
0x4000: Heap	0x4000: Heap

Cannot see → ← Cannot see
BusyBox's	Inference's
memory	memory

Key point: Even though both might use address $0 \times 1000$ , they're seeing completely different physical memory. The kernel enforces this separation.

Security benefit: If there's a buffer overflow in llama2.c that tries to write beyond its boundaries, it will:

1. Hit a page boundary
2. Try to access memory it doesn't have a capability for
3. Kernel blocks it immediately
4. Only the Inference PD crashes, not the whole system

Concept 4: IPC - Safe Communication Between Rooms

Since PDs are isolated, how do they talk? Through IPC (Inter-Process Communication) - like a secure intercom system:

Step 1: Inference PD needs input

Step 2: Reply comes back the same way

Properties of IPC:

• Synchronous: Sender waits for reply (like a phone call, not a text)
• Secure: Kernel validates all access
• Fast: Highly optimized, minimal overhead
• Safe: No way to bypass; must use proper endpoint

Concept 5: Untyped Memory - Raw Resources

When your system boots, the kernel gives the Root Task a bunch of Untyped Memory - think of it as raw, unformed clay:

1 MB of Raw Memory (Untyped)

"This is just raw RAM, not shaped yet"

Root Task "shapes" it:

$\downarrow$ Retype operation

TCB

EP

Memory Frames

1KB

16B

(256 × 4KB pages)

Thread

IPC

Usable memory

control chan

for programs

Process:

1. Untyped Memory: Raw physical RAM
2. Retype: Transform into specific object types (TCB, Endpoint, Frame)
3. Distribute: Give capabilities to these objects to PDs
4. Use: PDs can now use these resources

Important rule: Once you retype memory, you can't change it back unless you:

1. Delete all capabilities pointing to it
2. Revoke it back to untyped

This prevents confusion and ensures resource tracking.

Part 4: How Your System Actually Works

Boot Sequence (What Happens When You Turn It On)

1. Power On

↓

2. Bootloader (Limine) loads seL4 kernel

↓

3. seL4 kernel initializes

• Sets up memory protection

• Prepares capability system

• Identifies all physical memory

↓

4. seL4 creates and starts Root Task PD

- Gives it ALL untyped memory
- Gives it authority to create other PDs

5. Root Task runs (your code)  
- Takes inventory of resources  
- Decides how to allocate memory

6. Root Task creates Inference PD  
a) Retype untyped memory  $\rightarrow$  TCB (thread)  
b) Retype untyped memory  $\rightarrow$  Frames (memory pages)  
c) Retype untyped memory  $\rightarrow$  Endpoint (IPC channel)  
d) Create CSpace for Inference PD  
e) Put capabilities into Inference PD's CSpace  
f) Load llama2.c into memory pages  
g) Configure page tables (VSpace)  
h) Start Inference PD thread  
↓

7. Root Task creates BusyBox PD (Same process as Inference PD)

8. System is running!

Runtime Example: Running an Inference

Let's trace what happens when a user asks "What is machine learning?"

Step 1: User types command in BusyBox

BusyBox PD User:"ask llama 'What is ML?'' Shell sees this is an AI command IPC: Send message to Inference PD Message:"Run inference:"What is ML?" Kernel Validates: BusyBox has endpoint capability? Message fits in IPC buffer? Inference PD ready to receive?

Security throughout:

• Inference PD never touches BusyBox's memory directly
• All communication goes through kernel-validated IPC
• If llama2.c crashes during inference, only Inference PD dies
• BusyBox and system keep running

Part 5: The Complete Picture with Microkit

Now, instead of manually coding all this capability management, you use Microkit - a framework that simplifies seL4 development.

System Description File (SDF)

You describe your system in XML, and Microkit generates all the capability setup code:

<system>  
<!-- Root Task: The System Manager -->  
<protection_domain name="root_task" priority="255">  
<program_image>root_task elf</program_image>  
<!-- Give it access to untyped memory -->  
<map mr="untyped_memory" vaddr="0x10000000"  
perms="rw" cached="true"/>  
</protection_domain>  
<!-- Inference PD: Runs llama2.c -->  
<protection_domain name="inference" priority="200">  
<program_image>llama2 elf</program_image>  
<!-- Allocate memory for model and inference -->  
<map mr="inference_memory" vaddr="0x20000000"  
perms="rw" cached="true" size="512MB"/>  
</protection_domain>  
<!-- BusyBox PD: User interface -->  
<protection_domain name="busybox" priority="100">  
<program_image>busybox elf</program_image>  
<map mr="busybox_memory" vaddr="0x30000000"  
perms="rw" cached="true" size="64MB"/>  
</protection_domain>  
<!-- Define communication channels -->  
<channel>  
    <end pd="inference" id="1"/>  
    <end pd="busybox" id="2"/>  
</channel>  
<channel>  
    <end pd="root_task" id="3"/>  
    <end pd="inference" id="4"/>  
</channel>  
</system>

What this file means:

1. protection_domain: Each is an isolated compartment

name: What you call it
o priority : Higher number = more important (root_task is highest)
o program_image : The compiled binary to run

2. map: Defines memory regions

• mr (memory region): Name of the memory region
o vaddr : Virtual address where PD sees this memory
perms:Permissions(read/write/execute)
size: How much memory

3. channel: Creates IPC connection between two PDs

Each end is one side of the communication

Microkit takes this file and:

• Creates all the CSpaces
• Generates all the capabilities
• Sets up all the VSpaces
• Configures IPC endpoints
• Generates startup code

How Components Talk

Example: BusyBox wants inference result

1. BusyBox calls:

seL4CALL(endpoint_cap，message)

2. Kernel receives call:

• Checks: Does BusyBox have endpoint_cap? ✓
• Validates message format
• Switches to Inference PD's context

3. Inference PD receives:

• Wakes up from seL4_Recv()
• Processes message
• Runs inference
• Calls seL4_Reply(result)

4. Kernel delivers reply:

• Switches back to BusyBox context
• BusyBox's seL4_Call() returns with result
• BusyBox displays output

Part 6: Complete System Overview

The Full Stack (Bottom to Top)

User Interaction (Commands entered in BusyBox)

↑

Protection Domain: BusyBox PD

Shell, utilities (BusyBox)

Handles user commands

Issues IPC calls to other PDs

CSpace: [TCB|EP|MEM|MEM|...]

VSpace: Shell code, command history, stack

IPC

Protection Domain: Inference PD

llama2.c (4,000 LOC)

Model weights loaded in memory

Inference computation

CSpace: [TCB|EP|MEM|MEM|MEM|...]

VSpace: llama2.c code, model data, buffers

IIPC

Protection Domain: Root Task PD

System initialization

Resource allocation

PD creation and management

CSpace: [Untyped|CNode|TCB|...]

VSpace: Root task code, management data

seL4 Microkernel (~10K LOC)

Capability system enforcement

Memory management

Thread scheduling

IPC handling

Hardware abstraction

Hardware Layer

CPU, RAM, Storage, Peripherals

Memory Layout

Physical Memory (example: 2GB system)

0x00000000	seL4 Kernel	~500KB
0x00080000	Root Task PD	10MB
0x00A80000	BusyBox PD	64MB
0x04A80000	Inference PD	512MB
0x24A80000	Model Weights	1GB
0x64A80000	Untyped (Free)	~400MB
0x80000000

Each PD sees its own virtual address space:

• BusyBox thinks it starts at 0x30000000
• Inference thinks it starts at 0x20000000
• Kernel maps these virtual addresses to different physical pages

Part 7: Why This Design Matters

Security Benefits

- Isolation is Absolute

• Buffer overflow in llama2.c? Only crashes Inference PD
  o Bug in BusyBox? Cannot access Al model memory
  o Compromised PD? Cannot escalate to kernel

- Minimal Attack Surface

• Kernel is only 10,000 lines (vs 30 million in Linux)
  Mathematically proven correct
  Less code = fewer bugs = fewer vulnerabilities

- Principle of Least Privilege

Each PD has ONLY the capabilities it needs
No "root" user with unlimited power

• Even if attacker takes over a PD, damage is contained

Reliability Benefits

- Component Crashes are Isolated

One PD crashes? Others keep running
o Restart crashed PD without rebooting system

- Predictable Behavior

• Priority-based scheduling (no surprises)
  Real-time guarantees possible
  No kernel bugs causing mysterious crashes

Performance Benefits

- Minimal Overhead

o Kernel does only essential tasks
Fast IPC (optimized fastpath)
No bloated syscall interface

- Cache Efficiency

• Small kernel fits in cache
  Less context switching overhead

Part 8: Practical Implementation Steps

Phase 1: Environment Setup

Install seL4 SDK and Microkit

1. Download seL4 SDK
2. Install build tools (CMake, cross-compiler)
3. Get Microkit framework
4. Set up QEMU for testing

Phase 2: Hello World System

Goal: Get 3 PDs running and communicating

1. Create SDF with 3 protection domains
2. Write simple Root Task that prints "Root running"
3. Write simple Inference PD that prints "Inference ready"
4. Write simple BusyBox PD that prints "Shell ready"
5. Build and run in QEMU
6. Verify all 3 PDs start successfully

Phase 3: Add IPC

Goal: Make PDs talk to each other

1. BusyBox sends "Hello" to Inference PD
2. Inference PD replies "Hello back"
3. Print messages to verify communication works

Phase 4: Integrate llama.cpp or Candle

Goal: Run actual AI inference

1. Compile llama.cpp or Candle for seL4

Remove filesystem dependencies
Use in-memory model loading
o Replace standard library calls with seL4 equivalents

2. Load model into Inference PD memory

Embed model in binary, or
Load from ramdisk

3. Test inference:

BusyBox: "What is AI?"
$\rightarrow$ IPC to Inference PD
$\rightarrow$ Ilama.cpp or Candle generates response

$\rightarrow$ IPC back to BusyBox
$\rightarrow$ Display result

Phase 5: Polish and Optimize

1. Add proper error handling
2. Optimize IPC buffer sizes
3. Tune memory allocation
4. Add logging/debugging
5. Performance profiling

Part 9: Comparison - Before and After

Your Original Stack

llama2.c (inference)

BusyBox (shell)

musl libc

Linux Kernel (huge)

Bootloader

\  
|  
| All in one  
| shared memory  
| space  
/  
Many millions of LOC  
Complex, many features

Risks:

• Any bug can affect anything
• Kernel has millions of lines to attack
• One crash kills everything

Your New seL4 Stack

Inference PD (isolated)

BusyBox PD (isolated)

Root Task PD (isolated)

Can't touch BusyBox

Can't touch Inference

Manages resources only

seL4 Kernel (minimal)

10,000 LOC, proven correct

Bootloader

Benefits:

• Isolation prevents bugs from spreading
• Minimal kernel = minimal attack surface
• Crash in one PD? Others keep running
• Mathematically proven security

Key Takeaways

• Protection Domains (PDs) are completely isolated containers for code. Think: Separate locked rooms in a vault
• Capabilities are unforgettable keys that grant access. Think: Physical keycards you can't fake
• CSpace is your keyring holding all your capabilities. Think: Your personal key collection
• VSpace is each PD's isolated memory view. Think: Each room has its own address system
  IPC is secure communication between PDs. Think: Secure intercombs between rooms
• Untyped Memory is raw resources shaped into objects. Think: Clay molded into specific tools
• seL4 Kernel enforces all this security. Think: Vault security system that's mathematically perfect
• Microkit simplifies building seL4 systems. Think: Blueprint system for designing your vault

This architecture gives you military-grade security for your AI inference system, with mathematical guarantees that bugs in one component cannot compromise another. It's more complex to set up than Linux, but provides security and reliability that no traditional OS can match.