Welcome to the Kirsch Handbook!

This is the root of the Kirsch handbook. To get started:

• get familiar with reStructuredText or MarkDown

• write in tutorials/ already

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

• refer to the Sphinx documentation for more information

Development

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

Design

• Cheriette
• Cheriette Development and Debugging
  • Morello
• Example design of some subsystem
• Exception Levels
  • System Permission
• The global logical address space
  • Why is it useful?
  • Who has tried this before?
  • Why retry it now?
  • Deriving the GLAS
• Interrupt Handling
• Related work
• Secure Calls
  • Theory of Operation
  • Related Work
  • CheriOS
  • CompartOS
  • CherIoT
• Tasks

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
• Executing Kirsch
  • ARM Morello FVP
  • CHERI RISC-V 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