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):

Threads & Scheduling

Create/delete threads
Schedule them (round-robin or priority)
Very fast context switch (~200 cycles)

Address Spaces

Manage virtual memory
Map pages between address spaces
Memory protection

Inter-Process Communication (IPC)

Message passing between threads
Very fast (~ microseconds)
Synchronous by default

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:

seL4 Website: https://sel4.systems/

Getting started guides
Documentation hub
Community info

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

Manual (comprehensive reference)
Tutorials
API documentation

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

Source code
Example projects
Issue tracking

Key Papers (Must Read):

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

The original paper
Explains verification approach
Foundation of everything

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

Extended verification
More detailed methodology

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

Binary verification
Compiler correctness

Books & Courses

Books:

“The seL4 Reference Manual” (Free online)

Official reference
Complete API documentation

“Microkernel Operating Systems” (Research papers collection)

Background on microkernel design
Historical context

Online Courses:

Advanced Operating Systems (UNSW) - Some lectures cover seL4
Trustworthy Systems Group tutorials - On seL4 website

Rust-Specific Resources

Rust + seL4:

sel4-sys crate documentation

https://docs.rs/sel4-sys/
Low-level bindings

sel4 crate documentation

https://docs.rs/sel4/
Safe Rust API

Microkit Rust Tutorial (Upcoming)

Check seL4 discourse
Auxiliary (Coliber) blog posts

Ferrous Systems Resources

Training materials
Blog posts on Rust + seL4

Community:

seL4 Discourse: https://sel4.discourse.group/
Rust Embedded Matrix: Chat about embedded Rust
RISC-V + seL4: Growing community

Video Resources

YouTube - seL4 Summit talks (Annual conference)
Gernot Heiser’s talks (Creator of seL4)
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:

Sensor Interface - Reads from I2C/SPI sensors
Crypto Service - Encrypts data (isolated)
Network Stack - Sends to cloud via Ethernet
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):

✓ Understand OS concepts
✓ Learn basic seL4 concepts
✓ Run seL4 test in QEMU
✓ Build simple single-component app

Intermediate (3-6 months):

✓ Multi-component IPC systems
✓ Device driver development
✓ Shared memory communication
✓ Rust seL4 development

Advanced (6+ months):

✓ CAmkES complex systems
✓ Real-time scheduling
✓ Security analysis
✓ Hardware deployment

Key Resources Recap:

📚 Must-Read:

seL4 Manual: https://docs.sel4.systems/
SOSP 2009 Paper
Microkit Tutorial

🛠️ Tools:

seL4 GitHub: https://github.com/seL4
Rust bindings: https://crates.io/crates/sel4
Microkit: https://github.com/seL4/microkit

💬 Community:

Discourse: https://sel4.discourse.group/
Matrix: #seL4:matrix.org
Mailing lists

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!

FilesExpand file tree

seL4_Rust_RISC-V.md

Latest commit

History

seL4_Rust_RISC-V.md

File metadata and controls

seL4: The Formally Verified Microkernel - Complete Deep Dive

Part 1: History & Evolution

Origins (2006-2009)

Major Milestones

Part 2: What is Formal Verification?

Traditional Software Development:

Formal Verification:

What’s Actually Proven?

The Proof Stack:

Part 3: Microkernel Architecture

Monolithic vs Microkernel

seL4 Kernel Responsibilities (ONLY):

Everything Else is User-Space:

Capability-Based Security

Part 4: Modern seL4 Development

Current Status (2024-2025)

Key Projects & Frameworks

The seL4 Ecosystem

Part 5: Rust Support for seL4

Why Rust + seL4 is Perfect

Rust seL4 Projects

Rust seL4 Architecture

Part 6: Learning Resources

Official Documentation

Books & Courses

Rust-Specific Resources

Video Resources

Part 7: Getting Started - Step by Step

Prerequisites

Step 1: Environment Setup

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

Step 3: First seL4 Application (C)

Step 4: Setting Up Rust for seL4

Step 5: Using Microkit with Rust

Part 8: Advanced RISC-V seL4 Development

Example 1: Multi-Component System

Example 2: Shared Memory Communication

Example 3: Device Driver in Rust

Example 4: Real-Time Scheduling

Example 5: CAmkES System (Advanced)

Part 9: Advanced Topics

1. Formal Verification Integration

2. Security Patterns

3. Performance Optimization

4. Debugging Techniques

5. Testing Strategies

Part 10: Real-World Project Example

Project: Secure IoT Gateway on RISC-V

Conclusion & Next Steps

Learning Path:

Key Resources Recap:

Why This Matters: