Welcome to the Kirsch Handbook!

Kirsch is a project about designing and building operating systems that understand the hardware they run on. To manage the complexity of modern hardware, we formally model hardware and then derive guarantees and configurations from that model.

The Kirsch OS is a collection of kernels and tools. Cheriette is a secure CHERI hardware capability kernel, we use Hubris for small microcontrollers, and seL4 for interoperability and provable guarantees on non-CHERI cores.

More documentation can be found in the Kirsch Project Wiki. In particular, the wiki contains links to other resources that are useful for developing Kirsch.

Design

• Cheriette
• The global logical address space
  • Why is it useful?
  • Who has tried this before?
  • Why retry it now?
  • Deriving the GLAS
• Exception Levels
  • System Permission
• Tasks & Compartments
  • Compartments
  • Tasks
  • Service Model
• Interrupt Handling
• Secure Calls
  • Theory of Operation
  • Linking secure calls
  • Secure calls across exception levels
  • Securing the stack
  • Clearing the Stack upon Return
  • Related Work
  • CheriOS
  • CompartOS
  • CherIoT
• Hardware Management
  • Software
  • Device Classes
• Rights Enforcement
• Build System
• Related work

Development

• CHERI RISC-V Cheatsheet
  • Registers
  • Capability Instructions
  • Capability-Extended Data Instructions
• Cheriette Development and Debugging
  • Morello
• Kirsch Coding Style
  • Documentation Comments
• Methodology
  • Principles
  • Workflows
• Morello Curiosities
  • Branching to capabilities with LSB 0

Tutorials

• Acquiring the Kirsch Toolchain
  • Setting up Docker
  • Pulling the image
  • Running the image
  • Tools included
  • File System Layout
  • Building the Docker Container
• Building Kirsch
  • Generate Ninja build file
  • Building for Morello
  • Building for Virt
  • Clean build files
• Executing Kirsch
  • ARM Morello FVP
  • ARM VIRT QEMU
• Build system
  • Principles
  • How to add a Context
  • How to add a new artifacts
• Souce Structure
• Writing specifications in Sockeye3
  • Checking out the source code
  • Organization of the source tree
  • Reading Sockeye specifications
  • Writing Sockeye specifications
  • Using Sockeye models in practice
  • Generating visualizations
  • Deriving a Global Logical Address Space
• seL4 in GLAS
  • Prerequisite
  • Prepare the workspace
  • Compile the seL4 Microkit
  • Target: wordle_part3
  • Target: virtio_blk
  • Target: vmm_minimal
  • Target: demo
  • Target: clean
  • Tracing

Indices and tables

• Index

• Search Page

Sphinx Tips

• get familiar with reStructuredText or MarkDown

• if you add a new subfolder, record it down in the toctree directive (like design)

• refer to the Sphinx documentation for more information