Project 8: seL4 Tutorial Completion

Complete the official seL4 tutorials and build systems with verified primitives.

Quick Reference

Attribute Value
Difficulty Advanced
Time Estimate 3-4 weeks
Language C
Prerequisites IPC + capability concepts
Key Topics Capabilities, untyped memory, CAmkES

1. Learning Objectives

By completing this project, you will:

  1. Build and run the seL4 tutorial environment.
  2. Use capabilities to create endpoints, threads, and memory objects.
  3. Implement IPC patterns with seL4 APIs.
  4. Build a component system using CAmkES.

2. Theoretical Foundation

2.1 Core Concepts

  • Capabilities: seL4’s explicit access control model.
  • Untyped Memory: Raw memory that must be retyped into objects.
  • CNodes/CSpaces: Capability storage and lookup.
  • CAmkES: Component-based system assembly.

2.2 Why This Matters

seL4 is the gold standard for verified microkernels. Completing the tutorials is the fastest way to learn its architecture and constraints.

2.3 Historical Context / Background

seL4 emerged from the L4 family and pioneered formal verification of a microkernel. Its memory model is designed for verifiability.

2.4 Common Misconceptions

  • “seL4 allocates memory itself.” It does not; you provide untyped memory.
  • “Capabilities are just permissions.” They are explicit references with rights.

3. Project Specification

3.1 What You Will Build

A series of tutorial exercises that create threads, map memory, and send messages using seL4’s official APIs. You will also build a small CAmkES system.

3.2 Functional Requirements

  1. Environment setup: Build and run the tutorial VM.
  2. Capability usage: Create endpoints and TCBs.
  3. Memory management: Retype untyped memory and map pages.
  4. IPC demo: Implement a ping-pong example.
  5. CAmkES component: Define and run a component graph.

3.3 Non-Functional Requirements

  • Reproducible builds: Document the build steps.
  • Correctness: All tutorial steps pass.

3.4 Example Usage / Output

$ repo init -u https://github.com/seL4/sel4-tutorials-manifest
$ repo sync
$ ./init --tutorial hello-world
$ ninja && ./simulate
hello world

3.5 Real World Outcome

$ ./simulate
Booting all finished, dropped to user space
hello world
[ipc] ping -> pong
[camkes] component graph started

4. Solution Architecture

4.1 High-Level Design

┌──────────────┐  caps   ┌──────────────┐
│  App Thread  │ ─────▶  │   seL4       │
└──────────────┘ ◀─────  │ IPC, sched   │
                          └──────────────┘

4.2 Key Components

Component Responsibility Key Decisions
CSpace Capability storage Slot layout
Untyped memory Raw allocation Retype strategy
IPC endpoint Message transfer Endpoint rights
CAmkES Component wiring Interface design

4.3 Data Structures

seL4_CPtr ep = simple_get_endpoint(&simple);
seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 0, 1);
seL4_SetMR(0, 0x1234);
seL4_Send(ep, info);

4.4 Algorithm Overview

Key Algorithm: seL4 IPC Send

  1. Set message registers.
  2. Invoke seL4_Send with endpoint capability.
  3. Receiver waits with seL4_Recv.

Complexity Analysis:

  • Time: O(1) per IPC in the fast path
  • Space: O(N) for capability slots

5. Implementation Guide

5.1 Development Environment Setup

repo init -u https://github.com/seL4/sel4-tutorials-manifest
repo sync
./init --tutorial hello-world

5.2 Project Structure

sel4-tutorials/
├── projects/
│   ├── hello-world/
│   ├── ipc/
│   ├── untyped/
│   └── camkes/
└── tools/

5.3 The Core Question You’re Answering

“How do you build systems when the kernel gives you only minimal, verified primitives?”

5.4 Concepts You Must Understand First

Stop and research these before coding:

  1. CNodes and CSpaces
  2. Untyped memory retyping
  3. TCBs and scheduling contexts
  4. Capability rights and transfer

5.5 Questions to Guide Your Design

  1. How will you allocate memory without malloc in the kernel?
  2. How will you wire components in CAmkES?
  3. How do you avoid capability leaks?

5.6 Thinking Exercise

Map a Page by Hand

Trace the steps to retype untyped memory into a frame and map it into a VSpace.

5.7 The Interview Questions They’ll Ask

  1. “What is untyped memory in seL4?”
  2. “Why is seL4 verifiable?”
  3. “How does CAmkES structure systems?”

5.8 Hints in Layers

Hint 1: Complete hello-world first Ensure environment works before deeper tutorials.

Hint 2: Use the simple interface It provides boot info and initial caps.

Hint 3: Log every retype call Helps understand object lifetimes.

5.9 Books That Will Help

Topic Book Chapter
seL4 capabilities seL4 Reference Manual Ch. 2
Untyped memory seL4 Reference Manual Ch. 3

5.10 Implementation Phases

Phase 1: Foundation (1 week)

Goals:

  • Build and run tutorial environment

Tasks:

  1. Sync repo and build hello-world.
  2. Run in simulator.

Checkpoint: hello-world prints output.

Phase 2: Core Functionality (2 weeks)

Goals:

  • IPC, untyped memory, mapping

Tasks:

  1. Complete IPC tutorial.
  2. Complete untyped and mapping tutorials.

Checkpoint: Ping-pong works with mapped memory.

Phase 3: Polish & Edge Cases (1 week)

Goals:

  • CAmkES system

Tasks:

  1. Define a simple component graph.
  2. Run it in simulator.

Checkpoint: Component output appears in logs.

5.11 Key Implementation Decisions

Decision Options Recommendation Rationale
Build system Ninja, Make Ninja Official tutorials use it
Component wiring Manual, CAmkES CAmkES Canonical seL4 path

6. Testing Strategy

6.1 Test Categories

Category Purpose Examples
Build Tests Verify toolchain build hello-world
IPC Tests Ping-pong IPC tutorial
Component Tests CAmkES component output

6.2 Critical Test Cases

  1. Untyped retype creates endpoint.
  2. IPC send/recv works.
  3. CAmkES component runs.

6.3 Test Data

Message values: 0x1234, 0xdeadbeef

7. Common Pitfalls & Debugging

7.1 Frequent Mistakes

Pitfall Symptom Solution
Missing repo init Build fails Re-run repo init
Wrong target No output Use ./simulate
Capability slot errors faults Check CSpace layout

7.2 Debugging Strategies

  • Use seL4 fault logs to locate bad caps.
  • Add serial logs in tutorial code.

7.3 Performance Traps

Not a performance project; focus on correctness and understanding.

8. Extensions & Challenges

8.1 Beginner Extensions

  • Add an extra IPC message field.
  • Add a small shared memory buffer.

8.2 Intermediate Extensions

  • Build a multi-component CAmkES app.
  • Implement a simple driver stub.

8.3 Advanced Extensions

  • Map a device frame and handle interrupts.
  • Explore seL4 MCS scheduling.

9. Real-World Connections

9.1 Industry Applications

  • Defense systems: Verified kernels for safety.
  • Automotive: seL4 in EV systems.
  • seL4: https://sel4.systems/

9.3 Interview Relevance

Verified systems and capability models are standout topics.

10. Resources

10.1 Essential Reading

  • seL4 Reference Manual - API and concepts.
  • seL4 Tutorials - Official labs.

10.2 Video Resources

  • seL4 lectures and tutorial walkthroughs.

10.3 Tools & Documentation

  • repo: source sync tool
  • QEMU: simulation environment
  • Project 2: Capabilities foundation.
  • Project 14: Formal IPC verification.

11. Self-Assessment Checklist

11.1 Understanding

  • I can explain untyped memory and retyping.
  • I can describe how capabilities control access.

11.2 Implementation

  • All tutorials build and run.
  • IPC example works.

11.3 Growth

  • I can explain why seL4 is verifiable.

12. Submission / Completion Criteria

Minimum Viable Completion:

  • Hello-world tutorial runs successfully.
  • IPC tutorial completed.

Full Completion:

  • Untyped/mapping tutorials completed.
  • CAmkES component runs.

Excellence (Going Above & Beyond):

  • Multi-component system with custom interface.
  • Explore seL4 MCS features.

This guide was generated from LEARN_MICROKERNELS.md. For the complete learning path, see the parent directory.