seL4: The Formally Verified Microkernel - Complete Deep Dive

Part 1: History & Evolution

Origins (2006-2009)

The Problem: In the early 2000s, operating system kernels had millions of lines of code with thousands of bugs. Security-critical systems (military, aerospace, medical) needed something better than “testing and hoping.”

The Vision: What if you could mathematically prove that an OS kernel has no bugs? Not just test it, but prove it’s correct using mathematics.

The Birth:

  • 2006: Project started at NICTA (National ICT Australia), now part of CSIRO’s Data61

  • Led by Professor Gernot Heiser and team

  • Goal: Create the world’s first OS kernel with a complete formal proof of correctness

The Challenge: Previous attempts at formal verification had failed because:

  • Kernels were too complex to verify

  • Verification tools weren’t powerful enough

  • Gap between verified model and actual implementation

Major Milestones

2009 - First Formal Verification:

  • seL4’s functional correctness proven

  • 8,700 lines of C code

  • 200,000 lines of Isabelle/HOL proof

  • Proved: Implementation matches specification

  • Proved: No buffer overflows, null pointer dereferences, arithmetic errors

  • Paper published at SOSP 2009 (top OS conference)

  • Revolutionary: First OS kernel with end-to-end proof

2011 - Information Flow Security:

  • Proved no information leakage between components

  • Critical for security: prevents covert channels

  • Means malware in one partition can’t spy on another

2013 - Binary Verification:

  • Proved compiled binary matches source code

  • Closes the “compiler bug” hole

  • Now proved from C code → ARM machine code

2014 - Open Source Release:

  • seL4 made open source (GPL v2)

  • Opened for commercial and research use

  • Community could now contribute

2016 - seL4 Foundation:

  • Non-profit established

  • Manages trademark and ecosystem

  • Members: HENSOLDT Cyber, Cog, DornerWorks, UNSW, etc.

2018 - RISC-V Port:

  • Official RISC-V support added

  • Perfect match: open hardware + verified software

  • Growing importance for secure systems

2020 - Multicore Verification:

  • MCS (Mixed Criticality System) extensions

  • Multicore support verified

  • Real-time guarantees proven

2021-2023 - Commercial Adoption:

  • Adopted in defense systems (classified projects)

  • Automotive safety systems

  • Aerospace applications

  • Medical devices

  • Network routers/switches

2024-Present - Ecosystem Growth:

  • Better tooling and developer experience

  • More language bindings (Rust!)

  • Growing community

  • Industrial deployments increasing

Part 2: What is Formal Verification?

Traditional Software Development:

Write code → Test → Find bugs → Fix → Repeat

Problem: Testing can only show presence of bugs, not absence

Formal Verification:

Write specification → Write code → Mathematical proof → Guaranteed correct

Three Layers of Proof in seL4:

1. Functional Correctness:

Specification (what it should do)
        ↓
    [PROOF]
        ↓
Implementation (C code - what it does)

Guarantee: The C code does exactly what the specification says, nothing more, nothing less.

2. Security Properties:

  • Authority Confinement: Process can only affect what it’s authorized to

  • Integrity: Data can’t be corrupted without permission

  • Confidentiality: Information can’t leak between components

3. Binary Verification:

C Code → Compiler → ARM Binary
        ↓              ↓
     [PROOF]      [PROOF]
        ↓              ↓
   Behaves correctly

What’s Actually Proven?

Guaranteed NOT present in seL4:

  • Buffer overflows

  • Null pointer dereferences

  • Pointer errors

  • Arithmetic overflows

  • Use-after-free

  • Double-free

  • Memory leaks (in kernel)

  • Deadlocks

  • Race conditions

  • Undefined behavior

NOT guaranteed (out of scope):

  • Hardware bugs (CPU, memory)

  • Side-channel attacks (spectre, meltdown) - these are hardware issues

  • Bugs in your application code

  • Physical attacks

The Proof Stack:

┌─────────────────────────────────────┐
│   Applications (your code)          │ ← Not verified
├─────────────────────────────────────┤
│   User-level services               │ ← Not verified
├─────────────────────────────────────┤
│   seL4 Microkernel (8,700 LOC)    │ ← VERIFIED ✓
├─────────────────────────────────────┤
│   Hardware                          │ ← Assumed correct
└─────────────────────────────────────┘

Part 3: Microkernel Architecture

Monolithic vs Microkernel

Monolithic Kernel (Linux, Windows):

┌──────────────────────────────────────────┐
│         Kernel Space                      │
│  ┌──────┬──────┬───────┬─────┬────────┐ │
│  │FS    │Net   │Drivers│Sched│Memory  │ │
│  └──────┴──────┴───────┴─────┴────────┘ │
│         All running in kernel mode       │
└──────────────────────────────────────────┘
│         User Space                        │
│  ┌──────────┬──────────┬──────────┐     │
│  │  App 1   │  App 2   │  App 3   │     │
│  └──────────┴──────────┴──────────┘     │
└──────────────────────────────────────────┘

Problem: Bug anywhere in kernel crashes everything

Microkernel (seL4):

┌──────────────────────────────────────────┐
│         User Space                        │
│  ┌───────┬────────┬────────┬──────────┐ │
│  │File   │Network │Drivers │Apps      │ │
│  │Server │Stack   │        │          │ │
│  └───────┴────────┴────────┴──────────┘ │
├──────────────────────────────────────────┤
│  seL4 Microkernel (minimal)              │
│  - IPC (Inter-Process Communication)     │
│  - Threads & Scheduling                  │
│  - Virtual Memory                        │
│  - Capabilities                          │
└──────────────────────────────────────────┘

Benefit: Bug in driver only crashes that driver, not whole system

seL4 Kernel Responsibilities (ONLY):

  1. Threads & Scheduling

  • Create/delete threads

  • Schedule them (round-robin or priority)

  • Very fast context switch (~200 cycles)

  1. Address Spaces

  • Manage virtual memory

  • Map pages between address spaces

  • Memory protection

  1. Inter-Process Communication (IPC)

  • Message passing between threads

  • Very fast (~ microseconds)

  • Synchronous by default

  1. Capabilities

  • Access control mechanism

  • If you have capability, you have permission

  • Cannot be forged

Everything Else is User-Space:

  • File systems

  • Network stacks

  • Device drivers

  • Graphics

  • Applications

Capability-Based Security

Traditional OS:

Process ID 1234 tries to access file X
  → Check ACL: Does user 500 have permission?

Problem: Ambient authority, confused deputy attacks

seL4 Capabilities:

┌──────────────────────────┐
│  Process holds:          │
│  - Cap to memory region  │ → Can read/write this memory
│  - Cap to endpoint       │ → Can send messages here
│  - Cap to another thread │ → Can control that thread
└──────────────────────────┘

Key Properties:

  • Unforgeable: Can’t create fake capabilities

  • Delegable: Can pass capabilities to other processes

  • Revocable: Can take capabilities away

  • Principle of Least Privilege: Only have caps you need

Part 4: Modern seL4 Development

Current Status (2024-2025)

Supported Architectures:

  • ARM: ARMv7, ARMv8 (AArch32/AArch64)

  • x86: 32-bit, 64-bit

  • RISC-V: RV32, RV64 (our focus!)

Verification Status:

  • Fully verified: ARM, x86 (functional correctness)

  • RISC-V: Implementation done, verification ongoing

  • Binary verification: ARM complete

Real-World Deployments:

  • Defense/military systems (classified)

  • Automotive ECUs (safety-critical)

  • Aerospace/avionics

  • Industrial control systems

  • Secure network devices

  • IoT gateways

Key Projects & Frameworks

1. CAmkES (Component Architecture for microkernel-based Embedded Systems)

  • Component-based development framework

  • Like “Lego blocks” for systems

  • Define components, connections, automatically generates glue code

  • Makes building complex systems easier

2. Microkit (formerly seL4 Core Platform)

  • Simpler framework for embedded systems

  • Static system configuration

  • Easier to get started than CAmkES

  • Good for real-time embedded

3. Genode Framework

  • Large OS framework running on seL4

  • Provides POSIX layer, device drivers

  • Can run Linux applications

  • Active community

The seL4 Ecosystem

┌─────────────────────────────────────────────┐
│           Your Application                   │
├─────────────────────────────────────────────┤
│  Frameworks (CAmkES/Microkit/Genode)        │
├─────────────────────────────────────────────┤
│  User-level Services                         │
│  ┌─────────┬──────────┬──────────────────┐ │
│  │File Sys │Networking│Device Drivers     │ │
│  └─────────┴──────────┴──────────────────┘ │
├─────────────────────────────────────────────┤
│  seL4 Microkernel API                       │
│  - libsel4 (C bindings)                     │
│  - sel4-sys (Rust bindings)                 │
├─────────────────────────────────────────────┤
│  seL4 Microkernel                           │ ← VERIFIED
└─────────────────────────────────────────────┘

Part 5: Rust Support for seL4

Why Rust + seL4 is Perfect

seL4’s Guarantees:

  • Kernel is verified (no bugs)

  • Isolation between components

  • Capability-based security

Rust’s Guarantees:

  • Memory safety (no use-after-free, buffer overflows)

  • Thread safety (no data races)

  • Zero-cost abstractions

Combined = Ultra-Secure System:

Verified kernel + Memory-safe applications = 
    Maximum security with minimal TCB

Rust seL4 Projects

1. sel4-sys (Low-level bindings)

  • Raw FFI bindings to seL4 C API

  • Generated from seL4 sources

  • Unsafe, but necessary foundation

2. sel4 (Safe Rust bindings)

  • Safe wrappers around sel4-sys

  • Type-safe capability handling

  • Idiomatic Rust API

3. sel4-microkit (Microkit support)

  • Framework for building Microkit systems in Rust

  • High-level abstractions

  • Active development by Auxiliary (formerly Coliber)

4. Ferrous Systems’ Work

  • Commercial Rust support for seL4

  • Training and consulting

  • Contributing to ecosystem

5. seL4 Core Platform (Rust)

  • Building blocks for systems

  • Memory management

  • Device driver framework

Rust seL4 Architecture

// Low level - sel4-sys (unsafe)
unsafe {
    seL4_Send(endpoint, msg_info);
}

// Mid level - sel4 crate (safe wrappers)
endpoint.send(message)?;

// High level - Microkit/Framework
component.send_event(TargetComponent, EventData)?;

Part 6: Learning Resources

Official Documentation

Primary Resources:

  1. seL4 Website: https://sel4.systems/

  • Getting started guides

  • Documentation hub

  • Community info

  1. seL4 Docs: https://docs.sel4.systems/

  • Manual (comprehensive reference)

  • Tutorials

  • API documentation

  1. seL4 GitHub: https://github.com/seL4

  • Source code

  • Example projects

  • Issue tracking

Key Papers (Must Read):

  1. “seL4: Formal Verification of an OS Kernel” (SOSP 2009)

  • The original paper

  • Explains verification approach

  • Foundation of everything

  1. “Comprehensive formal verification of an OS microkernel” (TOCS 2014)

  • Extended verification

  • More detailed methodology

  1. “Translation validation for a verified OS kernel” (PLDI 2013)

  • Binary verification

  • Compiler correctness

Books & Courses

Books:

  1. “The seL4 Reference Manual” (Free online)

  • Official reference

  • Complete API documentation

  1. “Microkernel Operating Systems” (Research papers collection)

  • Background on microkernel design

  • Historical context

Online Courses:

  1. Advanced Operating Systems (UNSW) - Some lectures cover seL4

  2. Trustworthy Systems Group tutorials - On seL4 website

Rust-Specific Resources

Rust + seL4:

  1. sel4-sys crate documentation

  1. sel4 crate documentation

  1. Microkit Rust Tutorial (Upcoming)

  • Check seL4 discourse

  • Auxiliary (Coliber) blog posts

  1. Ferrous Systems Resources

  • Training materials

  • Blog posts on Rust + seL4

Community:

Video Resources

  1. YouTube - seL4 Summit talks (Annual conference)

  2. Gernot Heiser’s talks (Creator of seL4)

  3. RISC-V Summit - seL4 talks

Part 7: Getting Started - Step by Step

Prerequisites

Knowledge:

  • C or Rust programming

  • Basic OS concepts (processes, memory, scheduling)

  • Linux command line

  • (Optional) Assembly language helps

Hardware:

  • Development machine (Linux recommended)

  • RISC-V board (or QEMU for emulation)

Step 1: Environment Setup

Install Dependencies:

# Ubuntu/Debian
sudo apt-get update
sudo apt-get install -y \
    build-essential \
    cmake \
    ninja-build \
    python3 python3-pip \
    git \
    libxml2-utils \
    libncurses-dev \
    curl

# Install repo tool
curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo
chmod a+x ~/bin/repo
export PATH=~/bin:$PATH

# Install Rust
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
source $HOME/.cargo/env

Install RISC-V Toolchain:

# Install prebuilt toolchain
sudo apt-get install gcc-riscv64-unknown-elf

# OR build from source (takes 1-2 hours)
git clone https://github.com/riscv/riscv-gnu-toolchain
cd riscv-gnu-toolchain
./configure --prefix=/opt/riscv --with-arch=rv64imac --with-abi=lp64
sudo make -j$(nproc)
export PATH=/opt/riscv/bin:$PATH

Install QEMU for RISC-V:

sudo apt-get install qemu-system-misc
# Or build latest:
git clone https://github.com/qemu/qemu.git
cd qemu
./configure --target-list=riscv64-softmmu,riscv32-softmmu
make -j$(nproc)
sudo make install

Step 2: Build seL4 for RISC-V (C)

Clone seL4 Test Project:

mkdir ~/sel4-projects
cd ~/sel4-projects

# Clone seL4 test suite
git clone https://github.com/seL4/sel4test-manifest.git
cd sel4test-manifest
repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync

Configure for RISC-V:

mkdir build-riscv64
cd build-riscv64

# Configure with CMake
cmake -DCROSS_COMPILER_PREFIX=riscv64-unknown-elf- \
      -DPLATFORM=spike \
      -DRISCV64=TRUE \
      -G Ninja \
      ../

# Build
ninja

Run in QEMU/Spike:

# Using Spike (RISC-V ISA simulator)
spike --isa=rv64imafdc images/sel4test-driver-image-riscv64-spike

# Or QEMU
qemu-system-riscv64 \
    -machine virt \
    -bios none \
    -kernel images/sel4test-driver-image-riscv64-spike \
    -nographic

Expected Output:

Booting all finished, dropped to user space
Starting test suite...
<test results>
All tests passed!

Step 3: First seL4 Application (C)

Create Simple IPC Example:

// hello_world.c
#include <sel4/sel4.h>
#include <stdio.h>
#include <utils/util.h>

int main(void) {
    printf("Hello from seL4 on RISC-V!\n");
    
    // Get our thread's TCB capability
    seL4_CPtr tcb = seL4_CapInitThreadTCB;
    
    // Query thread information
    seL4_IPCBuffer *ipc_buffer = seL4_GetIPCBuffer();
    printf("IPC Buffer at: %p\n", ipc_buffer);
    
    // Create an endpoint for IPC
    seL4_Word ep_badge;
    seL4_CPtr endpoint = seL4_CapInitThreadEP;
    
    printf("Thread capabilities working!\n");
    printf("System is verified and running correctly.\n");
    
    return 0;
}

Build Configuration:

# CMakeLists.txt
cmake_minimum_required(VERSION 3.7.2)
project(hello_sel4 C ASM)

find_package(seL4 REQUIRED)
sel4_import_kernel()

add_executable(hello_world hello_world.c)
target_link_libraries(hello_world sel4 muslc utils)

Step 4: Setting Up Rust for seL4

Add Rust RISC-V Target:

rustup target add riscv64gc-unknown-none-elf
rustup component add rust-src

Create Rust seL4 Project:

cargo new --bin sel4-rust-hello
cd sel4-rust-hello

Cargo.toml:

[package]
name = "sel4-rust-hello"
version = "0.1.0"
edition = "2021"

[dependencies]
sel4-sys = "0.2"  # Low-level bindings
sel4 = "0.2"       # Safe wrappers

[profile.release]
lto = true
opt-level = "z"
panic = "abort"

Basic Rust seL4 Code:

// src/main.rs
#![no_std]
#![no_main]

use sel4_sys::*;
use core::panic::PanicInfo;

#[no_mangle]
pub extern "C" fn _start() -> ! {
    // Called by seL4 when thread starts
    main();
    
    // Hang forever
    loop {
        unsafe { 
            core::arch::asm!("wfi"); // Wait for interrupt
        }
    }
}

fn main() {
    // Your seL4 application code here
    unsafe {
        // Example: Get IPC buffer
        let ipc_buf = seL4_GetIPCBuffer();
        
        // Can't use println! (no_std), but you can:
        // - Send IPC messages
        // - Manipulate capabilities
        // - Create threads
        // - Map memory
    }
}

#[panic_handler]
fn panic(_info: &PanicInfo) -> ! {
    loop {}
}

Step 5: Using Microkit with Rust

Clone Microkit:

git clone https://github.com/seL4/microkit.git
cd microkit

Microkit System Description (.system file):

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <memory_region name="uart" size="0x1000" phys_addr="0x10000000" />
    
    <protection_domain name="hello" priority="100">
        <program_image path="hello.elf" />
        <map mr="uart" vaddr="0x2000000" perms="rw" cached="false" />
    </protection_domain>
</system>

Microkit Rust Component:

// hello.rs
#![no_std]
#![no_main]

use sel4_microkit::*;

const UART_BASE: usize = 0x2000000;

#[no_mangle]
pub extern "C" fn init() {
    // Called once at startup
    debug_println!("Hello from Microkit on RISC-V!");
}

#[no_mangle]
pub extern "C" fn notified(channel: Channel) {
    // Called when notification received
    debug_println!("Got notification on channel {}", channel);
}

#[panic_handler]
fn panic(info: &core::panic::PanicInfo) -> ! {
    debug_println!("Panic: {:?}", info);
    loop {}
}

Build with Microkit:

# Build Rust component
cargo build --release --target riscv64gc-unknown-none-elf

# Build system image with Microkit tool
microkit system.system --board qemu_riscv64_virt --output image.elf

# Run
qemu-system-riscv64 -machine virt -nographic -kernel image.elf

Part 8: Advanced RISC-V seL4 Development

Example 1: Multi-Component System

System Architecture:

┌─────────────┐      ┌──────────────┐      ┌─────────────┐
│   Client    │─IPC─→│   Server     │─IPC─→│   Driver    │
│ (Rust)      │←─────│  (Rust)      │←─────│  (Rust)     │
└─────────────┘      └──────────────┘      └─────────────┘
      ↓                     ↓                      ↓
┌─────────────────────────────────────────────────────────┐
│                  seL4 Microkernel                        │
└─────────────────────────────────────────────────────────┘

Client Component:

// client.rs
#![no_std]
#![no_main]

use sel4_microkit::*;

const SERVER_CHANNEL: Channel = 1;

#[no_mangle]
pub extern "C" fn init() {
    debug_println!("Client: Starting");
    
    // Send request to server
    let msg = MessageInfo::new(0, 0, 0, 1);
    protected_notify(SERVER_CHANNEL);
}

#[no_mangle]
pub extern "C" fn notified(channel: Channel) {
    match channel {
        SERVER_CHANNEL => {
            debug_println!("Client: Got response from server");
            // Process response
        }
        _ => {}
    }
}

panic_handler!();

Server Component:

// server.rs
#![no_std]
#![no_main]

use sel4_microkit::*;

const CLIENT_CHANNEL: Channel = 1;
const DRIVER_CHANNEL: Channel = 2;

static mut REQUEST_COUNT: usize = 0;

#[no_mangle]
pub extern "C" fn init() {
    debug_println!("Server: Ready to handle requests");
}

#[no_mangle]
pub extern "C" fn notified(channel: Channel) {
    match channel {
        CLIENT_CHANNEL => {
            unsafe { REQUEST_COUNT += 1; }
            debug_println!("Server: Processing request #{}", 
                          unsafe { REQUEST_COUNT });
            
            // Forward to driver
            protected_notify(DRIVER_CHANNEL);
        }
        DRIVER_CHANNEL => {
            debug_println!("Server: Got driver response");
            // Send back to client
            protected_notify(CLIENT_CHANNEL);
        }
        _ => {}
    }
}

panic_handler!();

Driver Component:

// driver.rs
#![no_std]
#![no_main]

use sel4_microkit::*;

const SERVER_CHANNEL: Channel = 2;
const UART_BASE: *mut u32 = 0x2000000 as *mut u32;

#[no_mangle]
pub extern "C" fn init() {
    debug_println!("Driver: Initializing UART");
    unsafe {
        // Initialize UART hardware
        UART_BASE.write_volatile(0x03); // 8N1
    }
}

#[no_mangle]
pub extern "C" fn notified(channel: Channel) {
    if channel == SERVER_CHANNEL {
        debug_println!("Driver: Handling hardware request");
        
        unsafe {
            // Write to UART
            let tx_reg = UART_BASE.add(0);
            tx_reg.write_volatile(b'O' as u32);
            tx_reg.write_volatile(b'K' as u32);
            tx_reg.write_volatile(b'\n' as u32);
        }
        
        // Notify server we're done
        protected_notify(SERVER_CHANNEL);
    }
}

panic_handler!();

System Definition:

<!-- system.system -->
<?xml version="1.0" encoding="UTF-8"?>
<system>
    <!-- Memory regions -->
    <memory_region name="uart" size="0x1000" phys_addr="0x10000000" />
    <memory_region name="shared_mem" size="0x1000" />
    
    <!-- Client PD -->
    <protection_domain name="client" priority="100">
        <program_image path="client.elf" />
        <map mr="shared_mem" vaddr="0x3000000" perms="rw" />
    </protection_domain>
    
    <!-- Server PD -->
    <protection_domain name="server" priority="100">
        <program_image path="server.elf" />
        <map mr="shared_mem" vaddr="0x3000000" perms="rw" />
    </protection_domain>
    
    <!-- Driver PD -->
    <protection_domain name="driver" priority="100">
        <program_image path="driver.elf" />
        <map mr="uart" vaddr="0x2000000" perms="rw" cached="false" />
    </protection_domain>
    
    <!-- Communication channels -->
    <channel>
        <end pd="client" id="1" />
        <end pd="server" id="1" />
    </channel>
    
    <channel>
        <end pd="server" id="2" />
        <end pd="driver" id="2" />
    </channel>
</system>

Example 2: Shared Memory Communication

Zero-Copy IPC with Shared Memory:

// shared_types.rs (shared between components)
#![no_std]

use core::sync::atomic::{AtomicU32, Ordering};

#[repr(C)]
pub struct SharedBuffer {
    pub write_index: AtomicU32,
    pub read_index: AtomicU32,
    pub data: [u8; 4096],
}

impl SharedBuffer {
    pub fn write(&self, byte: u8) -> Result<(), ()> {
        let write_idx = self.write_index.load(Ordering::Acquire);
        let read_idx = self.read_index.load(Ordering::Acquire);
        
        let next_write = (write_idx + 1) % self.data.len() as u32;
        if next_write == read_idx {
            return Err(()); // Buffer full
        }
        
        self.data[write_idx as usize] = byte;
        self.write_index.store(next_write, Ordering::Release);
        Ok(())
    }
    
    pub fn read(&self) -> Option<u8> {
        let read_idx = self.read_index.load(Ordering::Acquire);
        let write_idx = self.write_index.load(Ordering::Acquire);
        
        if read_idx == write_idx {
            return None; // Buffer empty
        }
        
        let byte = self.data[read_idx as usize];
        let next_read = (read_idx + 1) % self.data.len() as u32;
        self.read_index.store(next_read, Ordering::Release);
        Some(byte)
    }
}

Producer Component:

// producer.rs
#![no_std]
#![no_main]

use sel4_microkit::*;
use shared_types::SharedBuffer;

const SHARED_MEM_ADDR: usize = 0x3000000;
const CONSUMER_CHANNEL: Channel = 1;

#[no_mangle]
pub extern "C" fn init() {
    let buffer = unsafe { 
        &*(SHARED_MEM_ADDR as *const SharedBuffer) 
    };
    
    // Write data
    let message = b"Hello from producer!";
    for &byte in message {
        while buffer.write(byte).is_err() {
            // Buffer full, yield
            protected_notify(CONSUMER_CHANNEL);
        }
    }
    
    // Notify consumer
    protected_notify(CONSUMER_CHANNEL);
}

panic_handler!();

Consumer Component:

// consumer.rs
#![no_std]
#![no_main]

use sel4_microkit::*;
use shared_types::SharedBuffer;

const SHARED_MEM_ADDR: usize = 0x3000000;

#[no_mangle]
pub extern "C" fn notified(_channel: Channel) {
    let buffer = unsafe { 
        &*(SHARED_MEM_ADDR as *const SharedBuffer) 
    };
    
    // Read all available data
    while let Some(byte) = buffer.read() {
        // Process byte
        debug_print!("{}", byte as char);
    }
}

panic_handler!();

Example 3: Device Driver in Rust

SPI Driver for RISC-V:

// spi_driver.rs
#![no_std]
#![no_main]

use sel4_microkit::*;
use core::ptr::{read_volatile, write_volatile};

const SPI_BASE: usize = 0x10040000;

struct SpiRegisters {
    base: usize,
}

impl SpiRegisters {
    unsafe fn new(base: usize) -> Self {
        SpiRegisters { base }
    }
    
    fn sckdiv(&self) -> *mut u32 {
        (self.base + 0x00) as *mut u32
    }
    
    fn sckmode(&self) -> *mut u32 {
        (self.base + 0x04) as *mut u32
    }
    
    fn csid(&self) -> *mut u32 {
        (self.base + 0x10) as *mut u32
    }
    
    fn csdef(&self) -> *mut u32 {
        (self.base + 0x14) as *mut u32
    }
    
    fn csmode(&self) -> *mut u32 {
        (self.base + 0x18) as *mut u32
    }
    
    fn txdata(&self) -> *mut u32 {
        (self.base + 0x48) as *mut u32
    }
    
    fn rxdata(&self) -> *mut u32 {
        (self.base + 0x4C) as *mut u32
    }
}

static mut SPI: Option<SpiRegisters> = None;

#[no_mangle]
pub extern "C" fn init() {
    unsafe {
        SPI = Some(SpiRegisters::new(SPI_BASE));
        
        let spi = SPI.as_ref().unwrap();
        
        // Configure SPI: 1MHz, mode 0
        write_volatile(spi.sckdiv(), 100); // Divide by 100
        write_volatile(spi.sckmode(), 0);  // Mode 0
        write_volatile(spi.csmode(), 0);   // Auto CS
    }
    
    debug_println!("SPI Driver initialized");
}

#[no_mangle]
pub extern "C" fn notified(channel: Channel) {
    const CLIENT_CHANNEL: Channel = 1;
    
    if channel == CLIENT_CHANNEL {
        // Handle SPI transaction request
        unsafe {
            let spi = SPI.as_ref().unwrap();
            
            // Example: transfer one byte
            let tx_data = 0x42;
            
            // Wait for TX FIFO ready
            loop {
                let txdata_val = read_volatile(spi.txdata());
                if (txdata_val & 0x80000000) == 0 {
                    write_volatile(spi.txdata(), tx_data);
                    break;
                }
            }
            
            // Wait for RX data
            let rx_data = loop {
                let rxdata_val = read_volatile(spi.rxdata());
                if (rxdata_val & 0x80000000) == 0 {
                    break rxdata_val & 0xFF;
                }
            };
            
            debug_println!("SPI: TX={:02x}, RX={:02x}", tx_data, rx_data);
        }
        
        // Notify client we're done
        protected_notify(CLIENT_CHANNEL);
    }
}

panic_handler!();

Example 4: Real-Time Scheduling

Priority-Based System:

// high_priority_task.rs
#![no_std]
#![no_main]

use sel4_microkit::*;

const TIMER_IRQ: IRQ = 5;

static mut TICK_COUNT: u64 = 0;

#[no_mangle]
pub extern "C" fn init() {
    debug_println!("High Priority Task: Ready");
    // This task has priority 254 (highest user priority)
}

#[no_mangle]
pub extern "C" fn notified(_channel: Channel) {
    unsafe {
        TICK_COUNT += 1;
        
        if TICK_COUNT % 1000 == 0 {
            debug_println!("High Priority: {} ticks", TICK_COUNT);
        }
        
        // Critical real-time processing here
        // This will preempt lower priority tasks
    }
}

panic_handler!();

System with priorities:

<protection_domain name="critical" priority="254">
    <program_image path="high_priority.elf" />
</protection_domain>

<protection_domain name="normal" priority="100">
    <program_image path="normal_priority.elf" />
</protection_domain>

<protection_domain name="background" priority="50">
    <program_image path="low_priority.elf" />
</protection_domain>

Example 5: CAmkES System (Advanced)

CAmkES Component Definition:

// Client.camkes
component Client {
    control;
    uses Echo echo_service;
}

// Server.camkes
component Server {
    provides Echo echo_service;
}

// Echo.idl4
procedure Echo {
    string echo_string(in string input_str);
};

// System composition
assembly {
    composition {
        component Client client;
        component Server server;
        
        connection seL4RPC echo_conn(
            from client.echo_service,
            to server.echo_service
        );
    }
    
    configuration {
        client.priority = 100;
        server.priority = 100;
    }
}

Client Implementation (Rust FFI):

// client_impl.rs
#![no_std]

use cstr_core::CStr;
use core::ffi::c_char;

extern "C" {
    fn echo_service_echo_string(input: *const c_char) -> *const c_char;
}

#[no_mangle]
pub extern "C" fn run() -> i32 {
    let message = "Hello from Rust client!\0";
    
    unsafe {
        let response = echo_service_echo_string(message.as_ptr() as *const c_char);
        let response_str = CStr::from_ptr(response);
        // Process response
    }
    
    0
}

Part 9: Advanced Topics

1. Formal Verification Integration

While you can’t verify your Rust code with seL4’s proofs automatically, you can:

Use Rust’s Type System for Safety:

// Capability wrapper that prevents misuse
pub struct Capability<T> {
    cap: seL4_CPtr,
    _phantom: core::marker::PhantomData<T>,
}

impl<T> Capability<T> {
    // Can only be created through verified paths
    pub(crate) unsafe fn from_raw(cap: seL4_CPtr) -> Self {
        Capability {
            cap,
            _phantom: core::marker::PhantomData,
        }
    }
    
    // Type-safe operations
    pub fn invoke(&self, /* ... */) -> Result<(), Error> {
        // ...
    }
}

// Cannot forge capabilities - compiler enforces this

Static Analysis Tools:

  • MIRI: Rust’s interpreter for detecting undefined behavior

  • Kani: Formal verification for Rust (AWS)

  • Prusti: Verification with Viper

2. Security Patterns

Principle of Least Privilege:

// Only grant necessary capabilities
pub struct RestrictedDriver {
    uart_mmio: Capability<MmioRegion>,
    // NO access to other memory
    // NO access to other devices
}

impl RestrictedDriver {
    pub fn write_byte(&self, byte: u8) {
        // Can only access UART, nothing else
        unsafe {
            self.uart_mmio.write(0, byte as u32);
        }
    }
}

Compartmentalization:

┌────────────────────────────────────┐
│  Crypto Component                  │
│  - Isolated memory                 │
│  - No network access               │
│  - Only IPC to specific components │
└────────────────────────────────────┘
         ↓ (IPC only)
┌────────────────────────────────────┐
│  Network Stack                     │
│  - No access to crypto keys        │
│  - Only packet buffers             │
└────────────────────────────────────┘

3. Performance Optimization

Fast Path IPC:

// seL4's fastpath IPC is ~200 cycles on modern CPUs
// To use it:
// 1. Use seL4_Call/seL4_Reply_Recv
// 2. Keep message small (4 words)
// 3. No caps transfer in message

#[inline(always)]
pub fn fast_ipc_call(ep: seL4_CPtr, msg: u32) -> u32 {
    let mut reply = 0u32;
    unsafe {
        let info = seL4_MessageInfo::new(0, 0, 0, 1);
        seL4_SetMR(0, msg);
        let reply_info = seL4_Call(ep, info);
        reply = seL4_GetMR(0);
    }
    reply
}

Zero-Copy Transfers:

// Map same physical memory into multiple address spaces
// No copying needed!

// In producer:
const SHARED_PHYS: PhysAddr = 0x80100000;
let shared_region = map_device_memory(SHARED_PHYS, 0x1000)?;

// In consumer (different address space):
let shared_region = map_device_memory(SHARED_PHYS, 0x1000)?;

// Both see same memory - zero copy!

4. Debugging Techniques

Serial Console Debugging:

// Simple UART debug output
const UART0: *mut u8 = 0x10000000 as *mut u8;

pub fn debug_putc(c: u8) {
    unsafe {
        UART0.write_volatile(c);
    }
}

#[macro_export]
macro_rules! debug_println {
    ($($arg:tt)*) => {{
        use core::fmt::Write;
        let mut writer = UartWriter;
        writeln!(writer, $($arg)*).ok();
    }};
}

GDB Debugging over JTAG:

# Terminal 1: Start OpenOCD
openocd -f interface/ftdi/olimex-arm-usb-ocd-h.cfg \
        -f target/riscv64.cfg

# Terminal 2: GDB
riscv64-unknown-elf-gdb image.elf
(gdb) target remote :3333
(gdb) load
(gdb) break main
(gdb) continue

Microkit Debug Output:

// Microkit provides debug_println! macro
debug_println!("Debug: variable = {}", value);

// Appears on serial console
// Can be disabled in release builds

5. Testing Strategies

Unit Tests (on host):

// Can test pure logic on host
#[cfg(test)]
mod tests {
    use super::*;
    
    #[test]
    fn test_buffer_logic() {
        let buffer = RingBuffer::new();
        buffer.push(42);
        assert_eq!(buffer.pop(), Some(42));
    }
}

Integration Tests (on QEMU):

// Run full system in QEMU
// Check output for expected results
// Automated with pytest or similar

// test_runner.py
def test_system_boots():
    output = run_qemu("system.elf")
    assert "System initialized" in output

Hardware-in-Loop:

┌─────────────┐     ┌──────────────┐     ┌──────────────┐
│   Host PC   │────→│ RISC-V Board │────→│  Test Jig    │
│  (Test     │     │ (DUT)         │     │ (Stimulus)   │
│   Runner)   │←────│               │←────│              │
└─────────────┘     └──────────────┘     └──────────────┘

Part 10: Real-World Project Example

Project: Secure IoT Gateway on RISC-V

System Architecture:

┌─────────────────────────────────────────────────────┐
│              seL4 on RISC-V                         │
├─────────────────────────────────────────────────────┤
│  ┌────────────┐  ┌───────────┐  ┌───────────────┐ │
│  │  Crypto    │  │  Network  │  │  Sensor       │ │
│  │  Service   │  │  Stack    │  │  Interface    │ │
│  │  (Rust)    │  │  (Rust)   │  │  (Rust)       │ │
│  └────────────┘  └───────────┘  └───────────────┘ │
│         ↓              ↓                ↓           │
│  ┌─────────────────────────────────────────────┐  │
│  │        seL4 Microkernel (Verified)          │  │
│  └─────────────────────────────────────────────┘  │
└─────────────────────────────────────────────────────┘

Key Components:

  1. Sensor Interface - Reads from I2C/SPI sensors

  2. Crypto Service - Encrypts data (isolated)

  3. Network Stack - Sends to cloud via Ethernet

  4. Manager - Coordinates everything

Why seL4 + RISC-V?

  • Security: Verified kernel prevents attacks

  • Isolation: Compromise in network doesn’t affect crypto

  • Open: Can audit entire stack

  • Cost: RISC-V reduces licensing

Implementation would include:

  • ~1000 lines Rust per component

  • Microkit configuration

  • Device drivers

  • Integration tests

Conclusion & Next Steps

Learning Path:

Beginner (1-2 months):

  1. ✓ Understand OS concepts

  2. ✓ Learn basic seL4 concepts

  3. ✓ Run seL4 test in QEMU

  4. ✓ Build simple single-component app

Intermediate (3-6 months):

  1. ✓ Multi-component IPC systems

  2. ✓ Device driver development

  3. ✓ Shared memory communication

  4. ✓ Rust seL4 development

Advanced (6+ months):

  1. ✓ CAmkES complex systems

  2. ✓ Real-time scheduling

  3. ✓ Security analysis

  4. ✓ Hardware deployment

Key Resources Recap:

📚 Must-Read:

🛠️ Tools:

💬 Community:

Why This Matters:

seL4 + RISC-V + Rust represents the future of trustworthy computing:

  • seL4: Mathematically proven correct kernel

  • RISC-V: Open, auditable hardware

  • Rust: Memory-safe system programming

This combination enables building systems that are:

  • Secure by construction, not just by testing

  • Fully auditable - no black boxes

  • Independent - no vendor lock-in

  • Future-proof - open standards

Whether you’re building IoT devices, autonomous vehicles, medical equipment, or secure communication systems, this stack provides unprecedented assurance.

The learning curve is steep, but the result is the most secure system software platform available today. Welcome to the world of formally verified systems!​​​​​​​​​​​​​​​​

Previoussaint_token_systemNextVPN Breakdown

Last updated