Sonata Software

This repository contains software, build flows and examples for the Sonata System running on the Sonata PCB.

For a guide on how to get up and running on building software for the sonata board see the getting started guide. After you are all set up, take a look at the hardware access control exercise.

Orientation

You are in the sonata-software repository. This repository wraps the lowrisc/cheriot-rtos, adding some Sonata specific demonstration code on top of the CHERIoT stack. The lowrisc/cheriot-rtos, included in this repository as a submodule, is a fork of the upstream CHERIoT-Platform/cheriot-rtos. CHERIoT-Platform/cheriot-rtos contains the CHERIoT software stack; it is well documented by the CHERIoT Programmer's Guide. The lowrisc/cheriot-rtos fork only exists to hold fresh patches that aren't quite ready to be upstreamed to CHERIoT-Platform/cheriot-rtos but will be.

Other repositories of note:

• sonata-system: holds the Sonata system RTL and bootloader which come together to generate the bitstream.
• sonata-rp2040: The firmware that is running on the Sonata's RP2040 microcontroller and emulates the 'SONATA' drive when you plug it into your computer.
• CHERIoT-Platform/llvm-project: The CHERIoT compiler toolchain.
• cheriot-audit: A tool to explore and verify the relationships between CHERIoT RTOS components.
• CHERIoT-Platform/book: The source of the CHERIoT Programmer's Guide.

For hardware documentation, see the Sonata system book.

License

Unless otherwise noted, everything in the repository is covered by the Apache License, Version 2.0. See the LICENSE file for more information on licensing.

Getting started guide

This guide tells you how to get started with the Sonata board. If you have any issues in following this guide please contact the Sunburst Team at info@lowrisc.org.

The Sonata software build environment can be setup under Windows, macOS and Linux.

We use a tool called Nix to manage the build environment on all platforms. You will install it but don't need to know anything about it to follow these instructions.

You will also need to setup the Sonata board itself with the latest release. Read the updating the sonata system guide for instructions on how to do this. You only need to follow the first two steps listed there. The 'Building examples' step requires the environment setup detailed below.

Only Windows requires specific instructions, Nix handles everything you need on Linux and macOS. So if you're not using Windows jump straight to Installing Nix.

Windows Specific Setup

To obtain a Linux environment on Windows, you can choose to start a virtual machine or use Windows Subsystem for Linux (WSL).

Microsoft provides a detailed guide on how to install WSL. For latest systems this would just be a single command:

wsl --install

You might need to enable virtualisation in the BIOS if it's not enabled by default.

If you are running the command without admin privileges, user account control (UAC) popups will appear a few times asking to allow changes to be made to the device. Click "yes" to approve.

After the command's completion, it should say that Ubuntu is installed. Reboot your machine for the changes to take effect.

After rebooting, Ubuntu should be available in your start menu. Click it to start. For the first time, it prompts you to select a Unix username and password. Follow the Linux (Ubuntu) steps for the rest of this guide.

ℹ️ If you have installed your WSL a long time ago, systemd may not have been enabled by default. It is recommended to enable systemd. See https://learn.microsoft.com/en-us/windows/wsl/systemd.

Installing Nix

The Nix package manager is used to create reproducible builds and consistent development environments. We recommend installing Nix with the Determinate Systems' nix-installer:

curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install

For more in-depth instructions, follow the guide on the zero to nix site.

If you've downloaded Nix through another method, make sure the experimental features "flakes" and "nix-command" are enabled.

To use Nix from the terminal you'll need to open up a new terminal for it to be added to your path.

Setup Cache

To make use of the lowRISC Nix cache, so you don't have to rebuild binaries yourself, you'll need to make sure you're a trusted user. To do this, you will need to add your user to the trusted users in /etc/nix/nix.conf, e.g. trusted-users = root username. You can also add all users from a certain group instead of a single user by using an @ symbol before the group name, e.g. @sudo or @wheel.

ℹ️ For Ubuntu users (including WSL users), this means adding this line to the /etc/nix/nix.conf:

trusted-users = root @sudo

You'll need to restart the nix-daemon afterwards for the change to be picked up.

sudo systemctl restart nix-daemon

ℹ️ For macOS users, this means adding this line to the /etc/nix/nix.conf:

trusted-users = root @admin

You then need to restart your Mac for the changes to take effect.

Enter the CHERIoT development environment

Running the following will put you in a shell environment with all the applications needed to build the CHERIoT RTOS.

# Enter the shell with
nix develop github:lowRISC/sonata-software
# Exit the shell with
exit

These applications are layered on top of your usual environment. You can see what was added with echo $PATH.

do you want to allow configuration setting 'extra-substituters' to be set to 'https://nix-cache.lowrisc.org/public/' (y/N)? y
do you want to permanently mark this value as trusted (y/N)? y
do you want to allow configuration setting 'extra-trusted-public-keys' to be set to 'nix-cache.lowrisc.org-public-1:O6JLD0yXzaJDPiQW1meVu32JIDViuaPtGDfjlOopU7o=' (y/N)? y
do you want to permanently mark this value as trusted (y/N)? y
warning: ignoring untrusted substituter 'https://nix-cache.lowrisc.org/public/', you are not a trusted user.

If you see the warning that substituter is ignored, cancel the process with Ctrl+C and check to see that trusted-users is setup properly. Nix can and will build everything from source if it can't find a cached version, so letting it continue will cause LLVM-Cheriot to be built from scratch on your machine.

Your first build

Clone the sonata software repository, making sure to recursively clone submodules as well, then navigate into it.

git clone --branch v1.0 \
	 --recurse-submodule \
    https://github.com/lowRISC/sonata-software.git
cd sonata-software

Note a particular branch is specified, this must match your release, the release notes will tell you which branch you should use.

Enter the nix development development environment if you haven't already. Note that because we are in the repository we don't need to provide any arguments to nix develop.

nix develop

Then build the examples with the following command.

xmake -P examples

After running this you should see the build run to completion and report success, the critical lines indicating a successful build are:

Converted to uf2, output size: 147968, start address: 0x2000
Wrote 147968 bytes to build/cheriot/cheriot/release/sonata_simple_demo.uf2
[100%]: build ok, spent 6.827s

(Note output size may differ)

If you have got a successful build, congratulations! Your environment is ready to go for Sonata software development. Get in touch with lowRISC on info@lowrisc.org if you have any issues.

For reference the full output (from a build run on a Linux machine) looks like:

$ xmake build -P examples
checking for platform ... cheriot
checking for architecture ... cheriot
generating /home/user/tmp/sonata-software/cheriot-rtos/sdk/firmware.ldscript.in ... ok
generating /home/user/tmp/sonata-software/cheriot-rtos/sdk/firmware.ldscript.in ... ok
generating /home/user/tmp/sonata-software/cheriot-rtos/sdk/firmware.ldscript.in ... ok
generating /home/user/tmp/sonata-software/cheriot-rtos/sdk/firmware.ldscript.in ... ok
generating /home/user/tmp/sonata-software/cheriot-rtos/sdk/firmware.ldscript.in ... ok
generating /home/user/tmp/sonata-software/cheriot-rtos/sdk/firmware.ldscript.in ... ok
[ 24%]: cache compiling.release ../cheriot-rtos/sdk/core/scheduler/main.cc
[ 24%]: cache compiling.release all/proximity_sensor_example.cc
[ 24%]: cache compiling.release ../cheriot-rtos/sdk/core/scheduler/main.cc
[ 24%]: cache compiling.release all/gpiolib.cc
[ 24%]: cache compiling.release snake/snake.cc
[ 24%]: cache compiling.release ../cheriot-rtos/sdk/core/scheduler/main.cc
[ 24%]: cache compiling.release ../cheriot-rtos/sdk/core/scheduler/main.cc
[ 24%]: cache compiling.release ../cheriot-rtos/sdk/core/scheduler/main.cc
[ 24%]: cache compiling.release all/led_walk.cc
[ 24%]: cache compiling.release ../cheriot-rtos/sdk/lib/cxxrt/guard.cc
[ 25%]: cache compiling.release ../cheriot-rtos/sdk/core/scheduler/main.cc
[ 26%]: cache compiling.release ../cheriot-rtos/sdk/lib/crt/cz.c
[ 27%]: cache compiling.release ../cheriot-rtos/sdk/lib/crt/arith64.c
[ 27%]: cache compiling.release ../cheriot-rtos/sdk/lib/atomic/atomic1.cc
[ 29%]: cache compiling.release all/echo.cc
[ 29%]: compiling.release ../cheriot-rtos/sdk/core/switcher/entry.S
[ 30%]: cache compiling.release ../third_party/display_drivers/core/lcd_base.c
[ 30%]: cache compiling.release ../third_party/display_drivers/core/m3x6_16pt.c
[ 31%]: cache compiling.release ../third_party/display_drivers/st7735/lcd_st7735.c
[ 32%]: cache compiling.release ../libraries/lcd.cc
[ 33%]: cache compiling.release all/lcd_test.cc
[ 33%]: cache compiling.release ../cheriot-rtos/sdk/lib/freestanding/memcmp.c
[ 34%]: cache compiling.release ../cheriot-rtos/sdk/lib/freestanding/memcpy.c
[ 35%]: cache compiling.release ../cheriot-rtos/sdk/lib/freestanding/memset.c
[ 36%]: cache compiling.release all/i2c_example.cc
[ 36%]: cache compiling.release ../cheriot-rtos/sdk/lib/debug/debug.cc
[ 38%]: cache compiling.release all/led_walk_raw.cc
[ 38%]: compiling.release ../cheriot-rtos/sdk/core/token_library/token_unseal.S
[ 39%]: cache compiling.release ../cheriot-rtos/sdk/lib/locks/locks.cc
[ 39%]: cache compiling.release ../cheriot-rtos/sdk/lib/locks/semaphore.cc
[ 40%]: cache compiling.release ../cheriot-rtos/sdk/lib/atomic/atomic4.cc
[ 41%]: cache compiling.release ../cheriot-rtos/sdk/core/allocator/main.cc
[ 42%]: cache compiling.release ../cheriot-rtos/sdk/lib/compartment_helpers/claim_fast.cc
[ 42%]: cache compiling.release ../cheriot-rtos/sdk/lib/compartment_helpers/check_pointer.cc
[ 43%]: compiling.release ../cheriot-rtos/sdk/core/loader/boot.S
[ 44%]: cache compiling.release ../cheriot-rtos/sdk/core/loader/boot.cc
[ 51%]: linking compartment led_walk.compartment
[ 51%]: linking library cxxrt.library
[ 51%]: linking library crt.library
[ 52%]: linking library lcd.library
[ 51%]: linking library atomic1.library
[ 52%]: linking privileged library cheriot.token_library.library
[ 52%]: linking library atomic4.library
[ 52%]: linking library debug.library
[ 52%]: linking compartment echo.compartment
[ 52%]: linking library freestanding.library
[ 59%]: linking library compartment_helpers.library
[ 69%]: linking compartment gpiolib.compartment
[ 69%]: linking compartment lcd_test.compartment
[ 69%]: linking compartment led_walk_raw.compartment
[ 69%]: linking compartment i2c_example.compartment
[ 69%]: linking compartment proximity_sensor_example.compartment
[ 69%]: linking compartment snake.compartment
[ 69%]: linking library locks.library
[ 80%]: linking privileged compartment sonata_demo_everything.scheduler.compartment
[ 80%]: linking privileged compartment cheriot.allocator.compartment
[ 80%]: linking privileged compartment sonata_led_demo.scheduler.compartment
[ 80%]: linking privileged compartment proximity_test.scheduler.compartment
[ 80%]: linking privileged compartment snake_demo.scheduler.compartment
[ 80%]: linking privileged compartment sonata_simple_demo.scheduler.compartment
[ 80%]: linking privileged compartment sonata_proximity_demo.scheduler.compartment
[ 90%]: linking firmware ../build/cheriot/cheriot/release/sonata_demo_everything
[ 90%]: linking firmware ../build/cheriot/cheriot/release/snake_demo
[ 90%]: linking firmware ../build/cheriot/cheriot/release/sonata_led_demo
[ 90%]: linking firmware ../build/cheriot/cheriot/release/sonata_proximity_demo
[ 90%]: linking firmware ../build/cheriot/cheriot/release/proximity_test
[ 90%]: linking firmware ../build/cheriot/cheriot/release/sonata_simple_demo
[ 90%]: Creating firmware report ../build/cheriot/cheriot/release/sonata_demo_everything.json
[ 90%]: Creating firmware dump ../build/cheriot/cheriot/release/sonata_demo_everything.dump
[ 90%]: Creating firmware report ../build/cheriot/cheriot/release/snake_demo.json
[ 90%]: Creating firmware dump ../build/cheriot/cheriot/release/snake_demo.dump
[ 90%]: Creating firmware report ../build/cheriot/cheriot/release/sonata_led_demo.json
[ 90%]: Creating firmware dump ../build/cheriot/cheriot/release/sonata_led_demo.dump
[ 90%]: Creating firmware report ../build/cheriot/cheriot/release/sonata_proximity_demo.json
[ 90%]: Creating firmware dump ../build/cheriot/cheriot/release/sonata_proximity_demo.dump
[ 90%]: Creating firmware report ../build/cheriot/cheriot/release/proximity_test.json
[ 90%]: Creating firmware dump ../build/cheriot/cheriot/release/proximity_test.dump
[ 90%]: Creating firmware report ../build/cheriot/cheriot/release/sonata_simple_demo.json
[ 90%]: Creating firmware dump ../build/cheriot/cheriot/release/sonata_simple_demo.dump
Converted to uf2, output size: 112128, start address: 0x2000
Wrote 112128 bytes to ../build/cheriot/cheriot/release/snake_demo.uf2
Converted to uf2, output size: 92160, start address: 0x2000
Wrote 92160 bytes to ../build/cheriot/cheriot/release/sonata_led_demo.uf2
Converted to uf2, output size: 152576, start address: 0x2000
Wrote 152576 bytes to ../build/cheriot/cheriot/release/sonata_demo_everything.uf2
Converted to uf2, output size: 152576, start address: 0x2000
Wrote 152576 bytes to ../build/cheriot/cheriot/release/sonata_proximity_demo.uf2
Converted to uf2, output size: 89088, start address: 0x2000
Wrote 89088 bytes to ../build/cheriot/cheriot/release/proximity_test.uf2
Converted to uf2, output size: 147968, start address: 0x2000
Wrote 147968 bytes to ../build/cheriot/cheriot/release/sonata_simple_demo.uf2
[100%]: build ok, spent 11.816s
warning: ./cheriot-rtos/sdk/xmake.lua:116: unknown language value 'c2x', it may be 'c89'
warning: add -v for getting more warnings ..

With a successful software build you can now try running software

Debug logs

If you want debug logs from the RTOS, configure your build with the following additional options.

rm -rf build .xmake
xmake config -P examples
    --debug-scheduler=y --debug-locks=y \
    --debug-cxxrt=y --debug-loader=y \
    --debug-token_library=y --debug-allocator=y
xmake -P examples

Reconfiguring doesn't always work reliably, so often you will want to delete the build and .xmake directories when changing the configuration.

Running Sonata Software

You can either run software on the sonata FPGA board or in the sonata simulator. We recommend you focus on the FPGA as you get started and return to the simulator if you think you would find it useful later.

Running on the Sonata FPGA

Before running the FPGA, you may need to put the latest RP2040 firmware and bitstream on your board, which you can do by following the instructions on the sonata-system release page.

Any builds of software in this repository will also produce a UF2 file containing the built firmware. When the Sonata FPGA is plugged into the computer, it should show up as a drive called 'SONATA'. On my computer, it can be found at /run/media/$USER/SONATA. You can copy the built UF2 file into this drive for the firmware to be loaded and run.

cp build/cheriot/cheriot/release/sonata_simple_demo.uf2 "/run/media/$USER/SONATA/"
sync # This `sync` command is rarely necessary.

On Windows it's likely easier to use the file explorer to copy the UF2 to the SONATA drive. Look for the Linux section below This PC.

To see the UART console logs, attach to /dev/ttyUSB2 at a Baud rate of 921,600 with your favourite terminal.

picocom /dev/ttyUSB2 -b 921600 --imap lfcrlf

On Windows, we recommend to use PuTTY to connect to serial ports. Select "Serial" as "Connection type", put the COM port in the "Serial line" text field, and set "Speed" to 921600. To find out what serial ports are available, you can open Device Manager and all connected serial ports are listed under "Ports (COM & LPT)" section. To fix the line feeds you may want to go into configuration and under "Terminal" select "implicit CR in every LF".

When running the sonata_simple_demo.uf2, you should see the following console output as well as some flashing LEDs and LCD activity. This UART output only gets printed once, so you may need to press the reset button (SW5) to see the output if you attach your console after programming.

bootloader: Loading software from flash...
bootloader: Booting into program, hopefully.
Led Walk Raw: Look pretty LEDs!

Running in the simulator

In the getting started guide, you entered the default environment with nix develop. Because you now want to use the simulator, you need to enter the environment that includes the simulator:

nix develop .#env-with-sim

This will pull the simulator into your path as sonata-simulator. There's a convenience script, scripts/run_sim.sh, for calling the simulator. You simply point the script to a built ELF file and it will run the firmware in the simulator. The ELF file is the build artefact with the same name as the firmware image and no extension. Note, the simulator will never terminate, so you will have to Ctrl+C to terminate the simulator.

./scripts/run_sim.sh build/cheriot/cheriot/release/sonata_simple_demo

UART output can be seen in the uart0.log file, which should appear in the directory the simulator was run from. This can be observed using tail -f which will monitor the file and output as soon as something is written to the UART. Note with the simulator running in the foreground this will need to be run in another terminal:

tail -f uart0.log

Using Sonata IO

Overview

The v1.0 Sonata System contains the following peripheral blocks for general purpose use:

• 5x SPI (2 dedicated and 3 muxable)
• 3x UART (1 dedicated and 2 muxable)
• 2x I2C (both muxable)
• GPIO (LEDs and Switches on the board plus GPIO for all headers other than mikroBUS)
• PWM (6 muxable channels, 1 dedicated channel)
• ADC (6 dedicated channels)
• 1x USB Device (dedicated)

Sonata contains a pinmux which allows you to chose which block is connected to a particular physical IO pin. Each pin has its own unique selection of blocks it can be attached to. The 'muxable' in the list refers to the blocks that can connect to multiple pins. Some of the blocks are dedicated, they connect to specific IO, e.g. there is a dedicated SPI block for the Ethernet controller.

Pinmux Usage

The pinmux has two kinds of selectors:

• Output selectors - One per pin, chooses which block I/O outputs to that pin
• Input selectors - One per block IO, chooses which pin inputs to that block IO

A pinmux driver is available to allow you to manipulate these selectors. Note there are defined constants for the selectors themselves but not the options within the selectors. E.g. PMOD0 pin 2 has output selector constant OutputPin::pmod0_2 but a raw number is used to choose which block I/O is connected to. The pinmux documentation provides the possible inputs and outputs for each selector.

For example say you wished to connect the PMOD0 SPI to SPI block 1; there are 4 selectors to set.

• PMOD 0 CS (pin 1), COPI (pin 2) and SCK (pin 4) output selectors
• SPI Block 1 CIPO input selector

The code below shows how to use the pinmux driver to do this:

#include <platform-pinmux.hh>

...

auto pinmux = SonataPinmux();
pinmux.output_pin_select(SonataPinmux::OutputPin::pmod0_1, 2);
pinmux.block_input_select(SonataPinmux::BlockInput::spi_1_cipo, 3);
pinmux.output_pin_select(SonataPinmux::OutputPin::pmod0_2, 2);
pinmux.output_pin_select(SonataPinmux::OutputPin::pmod0_4, 2);

Following this you can then use the spi1 SPI instance to communicate with whatever SPI device is plugged into PMOD0.

Driver Usage

The various drivers work with a capability that points to the relevant device address range in the memory map. CHERIoT RTOS provides the MMIO_CAPABILITY macro to easily get a driver instance for a particular device. The compiler, build system and runtime handle setting up the required capability and providing it to the compartment.

An example usage of the I2C driver can be see in sonata-software/examples/all/i2c_example.cc. The relevant line that creates the driver instance is:

auto i2c0 = MMIO_CAPABILITY(OpenTitanI2c, i2c0);

Similar code can be used to instantiate a driver for all of the peripheral instances and types.

Pinouts

To determine the mapping between the pin names in the pinmux documentation and the physical headers on the Sonata PCB there are a few pinout diagrams you can use.

• Arduino Shield - pin names have the form ah_tmpioN where N is the Arduino digital pin number. This is the number in light pink on the linked diagram and labeled as DN on the Sonata PCB silkscreen. This matches the numbering seen on Arduino boards on the digital side of the header. The analog pins (A0 - A5) are fixed and connect directly to the ADC.
• Raspberry PI HAT - pin names have the form rph_gN where N is the GPIO number provided on the pinout diagram. Note this is different to the physical pin number, which relates to the physical pin position and is the number written on the Sonata PCB. The physical pin number is the one immediately next to the header in the pinout diagram. For instance rph_g0 is physical pin 27.
• PMOD - pin names have the form pmodX_Y where X is the PMOD header (0 on the left, 1 on the right) and Y is the pin in the header. The Y pin number is the physical pin number (corresponding to the 'Pin' column of the various interface type tables in the linked specification). Note there are no pmodX_5 and pmodX_6 pins seen in the pinmux documentation as these are ground and power pins.
• PMOD C - These are the 6 pins in the middle of the large PMOD header, they have the form pmodc_N where N corresponds to the physical pin number. 1, 2 and 3 are the top pins. pmodc_1 is the top right pin.
• mikroBUS - pin names have the form mbN where N is the physical pin number. The mikroBUS specification does not specify specific pin numbers. For Sonata mb1 is mikroBUS pin CS, mb4 is mikroBUS pin MOSI, mb5 is mikroBUS pin SDA and mb10 is mikroBUS pin PWM. The others follow from those. mikroBUS does not define any GPIO pins so there is no GPIO block for this header.

Peripheral Device Details

The device names used here are those given the CHERIoT RTOS Sonata board description file found in cheriot-rtos/sdk/boards/sonata-prerelease.json. For each peripheral type details of the instances available and what pins they can mux to are given below along with a link to the driver file used for that peripheral.

SPI

Driver: cheriot-rtos/sdk/include/platform/platform-spi.hh

2 of the SPI blocks are fixed.

• spi_lcd - Connects to the LCD
• spi_ethmac - Connects to the ethernet controller

3 of the SPI instances are muxable.

• spi0 - SPI flash and SD card
• spi1 - RPI HAT SPI0, Arduino SPI, PMOD 0 SPI
• spi2 - RPI HAT SPI1, PMOD 1 SPI, mikroBUS SPI

SPI chip-select (CS)

Each SPI block has 4 chip-select lines which are controlled via the cs register. This can be accessed directly by read/writing to the cs member of the SonataSPI structure. To see which cs bit corresponds to which physical pin consult the pinmux documentation. For example the raspberry PI HAT GPIO 7 pin (rph_g7) can be controlled by bit 1 of the SPI block 1 CS register when that is chosen as the output in the rph_g7 output selector in the pinmux.

UART

Driver: cheriot-rtos/sdk/include/platform/platform-uart.hh

1 UART is fixed:

• uart - The system UART available on the TX/RX0 UART header (P12). Connects to FTDI USB UART when jumpers are connected. Used as debug log, stdout and sterr in CHERIoT RTOS.

The other 2 UARTs are muxable:

• uart1 - TX/RX1 UART header (P12), RPI Hat UART, Arduino UART, mikroBUS UART, PMOD 0 UART
• uart2 - TX/RX1 UART header (P12), PMOD1 UART, RS232, RS485

I2C

Driver: cheriot-rtos/sdk/include/platform/platform-i2c.hh

Both I2C instances are muxable, however they act differently to the other muxable busses. As I2C is a low speed shared bus multiple headers can be muxed onto an I2C instance. So for each i2c blocks it's possible to have all the physical pins driven by it at once.

• i2c0 - qwiic0 & Arduino I2C, RPI Hat EEPROM I2C, PMOD0 I2C
• i2c1 - qwiic1, RPI Hat I2C, mikroBUS I2C, PMOD1 I2C

Note that the qwiic0 & Arduino I2C pins are physically wired together on the PCB.

GPIO

Driver: cheriot-rtos/sdk/include/platform/platform-gpio.hh

All of the GPIO blocks are fixed, in that each are dedicated to a specific set of pins. For many of those pins there's multiple things they can be muxed to (e.g. on the Raspberry Pi HAT header you can choose between using the SPI to drive the SPI pins or switch them to GPIO).

The available GPIO blocks are:

• gpio_board - LEDs and switches on the Sonata PCB
• gpio_rpi - Raspberry PI HAT
• gpio_arduino - Arduino Shield
• gpio_pmod0 - PMOD 0
• gpio_pmod1 - PMOD 1
• gpio_pmodc - PMOD C (the middle 6 pins between PMOD 0 and PMOD 1)

PWM

Driver: cheriot-rtos/sdk/include/platform/platform-pwm.hh

6 PWM channels are muxable, accessible through one RTOS device:

• pwm - Muxable between RPI Hat, Arduino, PMOD and mikroBUS

One channel is fixed, accessible through a separate RTOS device:

• pwm_lcd - Connected to LCD backlight control

ADC

Driver: cheriot-rtos/sdk/include/platform/platform-adc.hh

The ADC uses the FPGA's internal XADC. The XADC is 12-bit with a 1 MSPS sampling rate. It is directly connected to the 6 Arduino analog pins. It can tolerate up to 5v input but the measurable range is 0 - 3v.

USB Device

Driver: cheriot-rtos/sdk/include/platform/platform-usbdev.hh

There is a single fixed USB device:

• usbdev - Connected directly to the User USB on the Sonata PCB.

Currently there is no USB stack or full USB examples available. However there is some test software used for Sonata testing in the sonata-system repository. sonata-system/blob/main/sw/cheri/checks/usbdev_check.cc will connect to a host as a virtual UART sending some text and echoing back received text. sonata-system/blob/main/sw/cheri/common/usbdev-utils.hh (used by usbdev_check) provides some basic USB functionality on top of the driver.

Exploring CHERIoT RTOS

CHERIoT RTOS Orientation

All the software in this repository runs on the CHERIoT RTOS, which is pulled in at the root of this repository as a submodule named cheriot-rtos. The CHERIoT Programmer's Guide contains most of what a programmer would need to know to use the RTOS.

The different boards supported can be found in cheriot-rtos/sdk/boards/, of particular interest will be the Sonata's description in sonata.json. More on board descriptions can be found in cheriot-rtos/docs/BoardDescriptions.md. The drivers (structures that map onto a peripherals' MMIO) add functionality can be found in cheriot-rtos/sdk/include/platform/; the Sonata/Sunburst specific peripherals can be found in sunburst/ within the aforementioned directory.

To explore the various utility libraries available, look through cheriot-rtos/sdk/include/. When first starting to explore capabilities, the CHERI::Capability class is useful for pointer introspection.

Build System

The CHERIoT RTOS uses xmake as it's build system. The main rules you'll use are compartment and library, for creating compartments and libraries, as well as the firmware rule for creating a firmware image. Documentation on these can be found in the CHERIoT RTOS' readme under 'building firmware images'. For examples of using these rules, look at a root xmake.lua file, such as examples/xmake.lua, and in the subdirectories it includes with the includes function. Note, we run an additional convert_to_uf2 function on our firmware images to create UF2 files in this repository.

Building an upstream CHERIoT RTOS example

The examples in cheriot-rtos/examples provide a nice tour of the different ways compartments can interact. These can be built by pointing xmake to the example one wants to build, as shown below:

# Run from the root of the sonata-software repository
xmake -P cheriot-rtos/examples/05.sealing/

Where's my UF2?

If you've followed the 'running software on the FPGA' guide, you'll expect UF2 files as part of the build artefacts but these aren't automatically created in the cheriot-rtos repository. Thankfully, this repository includes a ./scripts/elf-to-uf2.sh script that converts an ELF into a firmware a UF2 file.

xmake -P cheriot-rtos/examples/05.sealing/
./scripts/elf-to-uf2.sh build/cheriot/cheriot/release/sealing

Auditing Firmware

This documentation provides an introduction to CHERIoT Audit, alongside a quick guide on developing auditing policies with Rego. You can find more comprehensive information about these tools in their relevant documentation:

• CHERIoT Audit: the source for cheriot-audit.
• Rego OPA Documentation: documentation for Rego, the policy language used by CHERIoT Audit.
• CHERIoT Programmer's Guide: CHERIoT documentation, which contains some small sections about auditing CHERIoT.

Introduction

When building firmware, the CHERIoT RTOS linker will produce JSON reports that describe the contents and interactions of each compartment. CHERIoT Audit is a tool that takes these less-comprehensible JSON reports, and consumes them via a policy language called Rego by evaluating a query to produce an output.

Rego is a (mostly) declarative programming language which is similar to other logic programming languages like Datalog and Prolog. It can be used by firmware integrators to write policies, which can then be verified automatically after linking firmware with CHERIoT Audit. Making use of effective compartmentalisation alongside CHERIoT Audit can help enhance supply-chain security, enabling safe sharing even if an attacker partially compromises your software. On top of this, it can simultaneously be used to enforce rules on compartments that you develop, to protect against bugs and misconfigurations.

Using CHERIoT Audit

When using CHERIoT Audit, you must specify the following three options:

• -b/--board: the board description JSON file (sonata.json).
• -j/--firmware-report: the JSON report emitted by the CHERIoT RTOS linker.
• -q/--query: the Rego query to run on the report.

First, make sure you have followed the getting started guide to setup your Nix development environment, and then build the examples using the standard build flow. After building the example software, you can query the exports of the echo compartment in the sonata_demo_everything report:

# Run from the root of the sonata-software repository
cheriot-audit --board=cheriot-rtos/sdk/boards/sonata.json \
              --firmware-report=build/cheriot/cheriot/release/sonata_demo_everything.json \
              --query='input.compartments.echo.exports'

This should then output something like this:

[{"export_symbol":"__export_echo__Z11entry_pointv", "exported":true, "interrupt_status":"enabled",
  "kind":"Function", "register_arguments":0, "start_offset":16}]

This output tells us that a single entry point is being exported by the echo compartment, which is a function that runs with interrupts enabled and takes no register arguments.

Developing with Rego

The vscode-opa extension for VSCode and the zed-rego extension for Zed provide syntax highlighting and a language server for linting functionality.

Rego operates using a few key abstractions known as documents:

• input, the input document, is the firmware report JSON files. There are also other input documents such as the board description.
• A set of modules (also known as virtual documents), which process the input documents in order to provide us with views that can then be further interpreted or convey more comprehensible information. You can write your own modules to encapsulate policy for your specific firmware, or use modules created by others. For example, cheriot-audit supports modules for the RTOS and core compartmentalisation abstractions, such as data.rtos.decode_allocator_capability.

These documents are then evaluated over a given Rego query to produce a JSON output. In order to drive automated auditing compliance or signing decisions, this result will be a single value or some Boolean result representing validity.

⚠️ Rego as a language has weakly-typed semantics. Running policies via cheriot-audit will report only some basic semantic errors. For example, accessing a key/attribute that does not exist will not raise an error as you may expect, but will instead result in an undefined decision. CHERIoT Audit currently represents undefined values using an empty output.

It is recommended to create appropriately modular policy code (see below) and test incrementally and often to avoid issues arising.

Creating modules

Writing a policy within a query string quickly becomes untenable; a better approach involves creating a Rego module and defining functions and predicates that encapsulate complex policy logic in a modular fashion. These rules can then be easily and programatically invoked via a simple query. For example, you could make a policy file policies/example.rego with the following structure:

package my_example

import future.keywords

example_function_1(arg1, arg2) {
    ...
}

example_function2() {
    ...
}

You might then use cheriot-audit via a command like:

cheriot-audit --board=cheriot-rtos/sdk/boards/sonata.json \
              --firmware-report=build/cheriot/cheriot/release/sonata_demo_everything.json \
              --module=policies/examples.rego \
              --query='data.my_example.example_function1("test", input.compartments)'

Where data.my_example refers to the my_example package declared in your included module. In this fashion, you can define readable and maintainable policies, and easily audit desired properties with a simple query.

A quick introduction to Rego

Rego is a policy language designed similarly to Datalog, which is a declarative logic inference programming language. As such, much of Rego's semantics will be familiar if you already know a logic programming language like Prolog, ASP or Datalog. Otherwise, it may be unfamiliar and unintuitive otherwise. If you have no such prior experience, it is highly recommended to read over the Rego documentation.

In documents you create policies, which are defined by one or more rules. Rules are in turn each composed of an assignment and a condition. A rule with no assignments evaluates to true by default if its condition is satisfied, and a rule with no condition is automatically assigned.

Rules can be written as name := val {condition}, where val can be either a Scalar or Composite value. Composite values are arrays, objects or sets, which are created and accessed using semantics similar to Python, e.g. rect := {"width": 2, "height": 4} and numbers = {1, 7, 19}.

• You can interpret the rule syntax a := b {c} as meaning a IS b IF c.
• := is the assignment operator. It assigns values to locally scoped variables/rules.
• == is the comparison operator, and checks for JSON equality.
• = is the unification operator. It combines assignment and comparison, with Rego assigning (binding) variables to values that make the comparison true. This lets you declaratively ask for values that make an expression true.

If the body of a rule will never evaluate to true, e.g. v if "a" = "b", then the rule is undefined. This means that any expressions using its value will also be undefined.

ℹ️ There is a notable exception to this rule: the not keyword acts as follows. If the value is true, then not true is false. Otherwise, if the value is anything else, including undefined, then the negation of that value is true.

Each rule can have multiple conditions. Rule bodies, marked by braces, are either delimited by semi-colons, or require you to separate individual expressions with newlines. Note here that Rego has whitespace-dependent semantics.

Variables can be freely used to define rules. For example, t if { a:= 12; b := 34; b > a}. When evaluating rule bodies, OPA searches for any variable bindings that make all of the expressions true - multiple such bindings may exist. This unification strategy is similar to the one found in Prolog, where variables in Rego are existentially quantified by default:

• If we have a := [1, 2, 3]; a[i] = 3, then the query is satisfied if there exists such an i such that all of the query's expressions are simultaneously satisfied. In this case, i=2 (note: arrays are zero-indexed).
• Universal quantification ("for all") can be performed using the syntactic sugar every keyword, or by negating the corresponding existentially quantified negated expression. For those familiar with logic syntax, this uses ∀x: p == ¬(∃x : ¬p).

Compound rule bodies can be understood as the logical conjunction (AND) of each individual expression. If any single condition evaluates to false, then so does the whole rule body. In contrast, any rule with multiple definitions is checked in-order until a matching definition is found. This can be understood as the logical disjunction (OR) of each individual rule.

Rego supports standard list and set operations, as well as comprehensions in the format

{mapped_output | iterator binding ; conditional_filters}

where conditional filtering is optional. For example, consider the list comprehension:

[ { "owner": owner, "capability": data.rtos.decode_allocator_capability(c) } |
c := input.compartments[owner].imports[_] ; data.rtos.is_allocator_capability(c) ]

Thich is analogous to the following Python list comprehension:

[{"owner": owner, "capability": data.rtos.decode_allocator_capability(c)}
 for owner, value in input.compartments.items()
 for c in value.imports
 if data.rtos.is_allocator_capability(c)]

Objects in Rego can be seen as unordered key-value collections, where any type can be used as a key. Attributes can be accessed via the object["attr"] syntax, or using object.attr for string attributes. Back-ticks can be used to create a raw string, which is useful when writing regular expressions for example.

Rego supports functions with the standard function syntax e.g. foo() := { ... } or bar(arg1, arg2) { ... }. These are then invoked like foo() or bar(5, {"x": 3, "y": 4}). Functions may have many inputs, but only one output. Because of Rego's evaluation strategy, function arguments can also be constant terms - for example foo([x, {"bar": y}]) := { ... }. Alongside Rego's existential quantification and unification rules, this can be used in a similar manner to pattern matching in higher-level languages.

Sonata Software Exercises

Building the Exercises

Assuming you've run through the getting started guide, you will have ran xmake -P examples and built the example firmware images. To build all the exercises, simply substitute examples for exercises.

xmake -P exercises

Exercises

Currently, there are two exercises:

• Hardware Access Control
• Firmware Auditing

Hardware Access Control Exercise

If you haven't already, please go to the 'building the exercises' section to see how the exercises are built.

In this exercise we utilise the compartmentalisation available in CHERIoT RTOS to control access to a hardware peripheral: the LEDs.

For this exercise, when the xmake.lua build file is mentioned exercises/hardware_access_control/xmake.lua is being referred to.

Part 1

Let's start with the firmware image called hardware_access_part_1 in the xmake.lua file. This image has two threads running two compartments: blinky_raw and led_walk_raw. blinky_raw simply toggles an LED and led_walk_raw walks through all the LEDs toggling them as it goes. The sources of these compartments can be found in exercises/hardware_access_control/part_1/.

Let's look inside blinky_raw. It uses the RTOS' MMIO_CAPABILITY macro to get the capability that grants it access to the GPIO MMIO region. This magic macro will handle adding the MMIO region to the compartment's imports and mapping it to a type, in this case SonataGpioBoard (from platform-gpio.hh). For more information on this macro, see the drivers section of CHERIoT programmers guide.

This is great! If you build and load the hardware_access_part_1 firmware on the FPGA, you have flashing LEDs! What more could one want?

Well maybe some level of access control. Currently both blinky_raw and led_walk_raw have access to all of the GPIO ports, and neither can trust the other compartment isn't toggling the LED when they are not looking. The keen-eyed among you will have noticed that this is already happening with both toggling user LED 7.

Part 2

Let's introduce some access control for the LEDs. To do this, we can create a new compartment gpio_access with sole access to the GPIO MMIO region. This compartment will arbitrate access to the LED outputs by making use of CHERIoT's sealing mechanism. When a compartment seals a capability, it can no longer be dereferenced or modified until it is unsealed by a compartment with the capability to do so. The gpio_access compartment creates these sealing capabilities as LED handles that it can give to other compartments. These other compartments can't use the handles directly, but can only pass them to gpio_access which can unseal them and use them. In this case, they only point to a LedHandle structure that only holds the index of a LED. They are purely used as a proof of LED ownership. For more information on sealing, see the cheriot-rtos/examples/05.sealing/.

blinky_raw and led_walk_raw have been adapted to use this new compartment and renamed blinky_dynamic and led_walk_dynamic. You'll notice these compartments use add_deps in the xmake.lua file to declare that they depend on gpio_access. Take a moment to look at the sources for these compartments in exercises/hardware_access_control/part_2/.

If you now run the hardware_access_part_2 firmware on the FPGA, you'll notice only blinky_dynamic is toggling it's LED. Looking at the UART console from the FPGA, the following message will pop up.

hardware_access_control/part_2/led_walk_dynamic.cc:19 Assertion failure in start_walking
LED 0x7 couldn't be acquired

led_walk_dynamic was run after blinky_dynamic because it's thread was given a lower priority in the xmake.lua. So when it asked for access to user LED 7, it was denied by gpio_access because this LED had already been allocated to blinky_dynamic.

Now change NumLeds in led_walk_dynamic.cc from 8 to 7, then rebuild. Both compartments should run happily again. Not only will both compartments run happily, but led_walk_dynamic will output the following over the console.

Led Walk Dynamic:           LED 3 Handle: 0x1087d0 (v:1 0x1087d0-0x1087e0 l:0x10 o:0xc p: G RWcgm- -- ---)
Led Walk Dynamic: Destroyed LED 3 Handle: 0x1087d0 (v:1 0x1087d0-0x1087e0 l:0x10 o:0xc p: G RWcgm- -- ---)
Led Walk Dynamic:       New LED 3 Handle: 0x108878 (v:1 0x108878-0x108888 l:0x10 o:0xc p: G RWcgm- -- ---)

These come from some superfluous lines in led_walk_dynamic.cc, which release ownership of user LED 3 only to later reacquire ownership. You can comment out the line that reacquires the LED:

	leds[3] = acquire_led(3).value();

When run led_walk_dynamic will now fail to toggle user LED 3 because it has relinquished ownership of the LED.

hardware_access_control/part_2/led_walk_dynamic.cc:34 Assertion failure in start_walking
Failed to toggle an LED

Part 3

This is great and all, but how do we stop a compartment bypassing gpio_access and using MMIO_CAPABILITY directly? In other words, how do we ensure that only gpio_access has access to the GPIOs?

Luckily the linker has all the information needed to check which compartments can access the GPIO MMIOs. It outputs this information in a JSON report with the rest of the build artefacts. To automate checking this report, we can use cheriot-audit which should already be in your path.

cheriot-audit allows you to query the JSON report and assert certain rules are followed. You do this with a language called Rego, but don't worry you won't have to learn it for this exercise. There are some pre-written rules in the gpio_access.rego module. Let's first look at only_gpio_access_has_access. It uses mmio_allow_list from the compartment package included in cheriot-audit to check that only the gpio_access compartment has access to the GPIO MMIOs. If we run this on the part 2 firmware image's JSON report, it will return true. However, when run against the part 1 firmware image's report it will return false, because the blinky_raw and led_walk_raw are not in the allow list.

# This should return true
cheriot-audit \
    --board cheriot-rtos/sdk/boards/sonata-prerelease.json \
    --module exercises/hardware_access_control/part_3/gpio_access.rego \
    --query "data.gpio_access.only_gpio_access_has_access" \
    --firmware-report "build/cheriot/cheriot/release/hardware_access_part_2.json"
# This should return false
cheriot-audit \
    --board cheriot-rtos/sdk/boards/sonata-prerelease.json \
    --module exercises/hardware_access_control/part_3/gpio_access.rego \
    --query "data.gpio_access.only_gpio_access_has_access" \
    --firmware-report "build/cheriot/cheriot/release/hardware_access_part_1.json"

There's a second rule, whitelisted_compartments_only, which adds an additional condition that only led_walk_dynamic and blinky_dynamic can use gpio_access. We can use this to restrict which compartments have access to the GPIO via gpio_access.

cheriot-audit \
    --board cheriot-rtos/sdk/boards/sonata-prerelease.json \
    --module exercises/hardware_access_control/part_3/gpio_access.rego \
    --query "data.gpio_access.whitelisted_compartments_only" \
    --firmware-report "build/cheriot/cheriot/release/hardware_access_part_2.json"

The above should return true as both compartments are in the allow list. Try removing one of the compartments from the allow list given to compartment_allow_list in gpio_access.rego and check the result of the above command is no longer true.

One can browse the other functions available as part of the compartment package in cheriot-audit's readme.

Part ∞

Where to go from here...

• There are input devices available through SonataGpioBoard. You could have a go at adding these to the gpio_access compartment.
• The interactions with ledTaken global in the gpio_access compartment aren't thread safe. You could take a look at cheriot-rtos/examples/06.producer-consumer/ to learn how to use a futex to make it thread safe.
• There is a technical interest group for Sunburst and a technology access programme run by UKRI that lowRISC is helping to adjudicate. If you are interested in either of these please reach out to info@lowrisc.org.

Firmware Auditing Exercise

First, make sure to go to the building the exercises section to see how the exercises are built.

You might find it useful to look at the auditing firmware documentation to get a brief introduction to cheriot-audit and the Rego policy language.

In this exercise, we use the cheriot-audit tool to audit the JSON firmware reports produced by the CHERIoT RTOS linker. This will let us assert a properties about our firmware images at link-time, guaranteeing desired safety checks. This exercise explores a set of self-contained policies which audit a variety of properties, to give an idea of what can be achieved using CHERIoT Audit.

For this exercise, when the xmake.lua build file is mentioned, we are referring to exercises/firmware_auditing/xmake.lua.

Part 1 - check that firmware contains no sealed capabilities

Policies are written using the Rego language, which has syntax that may be unfamiliar. If you find yourself confused whilst going through this exercise, it might be helpful to read over the introduction to Rego in the documentation.

The policy for this exercise can be found in the no_sealed_capabilities.rego file. You can either follow along as this exercise explains how the policy works, or try writing your own policy with the same behaviour. The firmware we are auditing is firmware_auditing_part_1, defined in xmake.lua, which contains one compartment based on the C++ file sealed_capability.cc. This is just a toy example, to show off the auditing functionality.

The first thing that this policy does is declares a no_seal package. This is to allow us to include the file as a module when invoking cheriot-audit, so that we can just refer to data.no_seal to call our implemented functions. A very simple function is_sealed_capability is then defined, which takes the JSON representing a given capability, and checks its kind attribute to determine whether it is a sealed capability or not.

Next, we use Rego's functionality to create a rule no_sealed_capabilities_exist, which should evaluate to true only if no sealed capabilities are used in any of the firmware's compartments. To do this, we perform a list comprehension, unifying with a wildcard variable to iterate over and filter all imported capabilities of all compartments in the firmware. We then use the built-incount function to ensure that the resulting array is empty.

Skipping to the end of the file, we can then create a simple Boolean valid rule which corresponds to whether no_sealed_capabilities_exist is defined or not. To convert the undefined value to a Boolean, we use the default keyword, which lets us provide a false asignment as a fall-through if no other rule definitions match.

We can run this policy on our example firmware using the following command:

cheriot-audit --board=cheriot-rtos/sdk/boards/sonata.json \
              --firmware-report=build/cheriot/cheriot/release/firmware_auditing_part_1.json \
              --module=exercises/firmware_auditing/part_1/no_sealed_capabilities.rego \
              --query='data.no_seal.valid'

Because sealed_capability.cc currently doesn't use any sealed capabilities, this policy should evalute to true.

Now, navigate to sealed_capability.cc and comment out or remove the line uint32_t arr[ArrSize];. Then, uncomment or add the line uint32_t *arr = new uint32_t[ArrSize];. This will change the array arr from being allocated on the stack to the heap. Rebuilding the exercises (using xmake -P exercises) and running the same command again should now cause the policy to evaluate to false.

However, it may not immediately be clear why the policy failed. When designing such a policy, you can see that it may be helpful to have a rule that lets us inspect the details of any sealed capabilities. We do this with our final sealed_capability_info rule, which constructs ojects storing the contents, key, and compartment of each sealed capability.

ℹ️ Note the use of unification here. We iterate over input.compartments with the non-defined variable owner, and then map the value that is bound this variable to the owner field of our new object.

Now, run the cheriot-audit command again, but replace data.no_seal.valid with data.no_seal.sealed_capability_info. You should see an output that looks something like this:

[{"compartment":"alloc", "contents":"00100000 00000000 00000000 00000000 00000000 00000000",
  "key":"MallocKey", "owner":"sealed_capability"}]

This tells us where the sealed capabilty in our firmware originates - a static sealed object owned by our sealed_capability compartment, which is used by the RTOS' allocator for authorising memory allocation. Try experimenting by adding more functionality to this toy example! For example, try creating your own sealed capabilities and check the result. You might also try investigating the values of the different rules that we've made, and filtering or auditing other properties of the capabilities.

Part 2 - check only permitted functions have interrupts disabled

The policy for this exercise can be found in the interrupt_disables.rego file. You can either follow along as this exercise explains how the policy works, or try writing your own policy with the same behaviour. The firmware we are auditing is firmware_auditing_part_2, defined in xmake.lua, which contains two compartments based on the C++ files disable_interrupts.cc and bad_disable_interrupts.cc.

As in the last exercise, we first declare an interrupts package, to allow us to use data.interrupts in our queries. We then start by defining which functions in which compartments are allowed to run with interrupts disabled. We do this by using a list, with each item in this list containing the name of the compartment, and a list of the function signatures that can run with interrupts disabled.

We allow two specific functions to run without interrupts in the disable_interrupts compartment, and allow none to run in the bad_disable_interrupts compartment. Despite this, if you check the the source files, not_allowed is actually running with interrupts disabled. In a practical scenario, disable_interrupts might be a trusted library, where bad_disable_interrupts is only allowed to call functions from disable_interrupts, and not disable interrupts itself.

We can then use this list to construct a smaller set containing just the compartments we expect to be present, which will be useful as the first condition that we want to check is that all (and only) the required compartments are present. We make a rule all_required_compartments_present which checks for this, by comparing the set of all present compartments and the set of required compartments. Because we are comparing two sets, == does not work as expected, and so we take the set intersection (using &) and then check its equality.

We then define a helper rule to allow us to retrieve information about all exported symbols, storing the compartment with each export. This information will be useful for demangling the names of export symbols. We then define exports_with_interrupt_status(status), which uses a list comprehension to filter for exports with a given interrupt status. The three possible status values are enabled, disabled and inherit. See section 3.4 of the CHERIoT Programmer's Guide for further information.

At this stage, we can try and query the names of exports with disabled interrupts, by using the following query:

'[x.export.export_symbol | x = data.interrupts.exports_with_interrupt_status("disabled")[_]]'

You should see that we get a lot of symbols that look something like __library_export_disable_interrupts__Z22run_without_interruptsi. This function name has been mangled during the compilation process, and can no longer be easily checked against our list. It is not always trivial to manually demangle these symbols.

Luckily for us, the libstdc++ cross-vendor C++ ABI defines a function abi::__cxa_demangle to help demangle these names, and cheriot-audit wraps and exposes this through the built-in export_entry_demangle function. This function takes the compartment name and export symbol as its two arguments.

ℹ️ The next rule patched_export_entry_demangle is not relevant to this example. It simply manually adds support for an additional library export name mangling prefix that is not currently checked for. However, it is a useful example of string operations in Rego, as well as another case of rules with multiple definitions. We have one rule for export symbols that start with __library_export_, converting this to an __export_ prefix, and otherwise we simply pass the symbol to export_entry_demangle.

Now that we have a method to filter for exported symbols with disabled interrupts, and the means to demangle names, we can create a rule to check that a compartment only has the specified disabled interrupts. When given a compartment, we search for exports with interrupts disabled that have an "owner" which corresponds to that compartment. We then map this through our export entry demangling function, to retrieve the original signatures. We compare this to the list of required signatures for the compartment - if it matches, then we assign true.

We can now easily express our final condition - for every compartment we have provided, it must contain exactly the list of functions with disabled interrupts that we specified. This uses the every keyword from the futures.keyword import to perform universal quantification.

Finally, we create a simple Boolean valid rule which combines our two condition rules all_required_compartments_present and only_required_disabled_interrupts_present, and which is defined to output false by default if either fail to match.

Now, we can audit the firmware for this exercise by using the following command:

cheriot-audit --board=cheriot-rtos/sdk/boards/sonata.json \
              --firmware-report=build/cheriot/cheriot/release/firmware_auditing_part_2.json \
              --module=exercises/firmware_auditing/part_2/interrupt_disables.rego \
              --query='data.interrupts.valid'

You can see that this returns false, because our current firmware does not conform to our policy. You can try changing any of the following:

1. Add not_allowed() to the list of allowed functions in bad_disabled_interrupts in the Rego policy.
2. Change the [[cheri::interrupt_state(disabled)]] tag on the not_allowed() function to enabled and rebuild.
3. Remove the [[cheri::interrupt_state(disabled)]] tag on the not_allowed() function entirely and rebuild. This works because interrupts default to being enabled.

Doing any of these three changes above and auditing should now output true, as the policy now matches the firmware image.

You can now try individually querying some of the helper rules that we have made, and using them to build your own rules. For this exercise, we consider both sufficiency and necessity - there is no way to allow a function to have interrupts disabled but not require it. You can try incorporating this addition to extend the exercise further, making an even more powerful and expressive policy.

Part 3 - audit maximum allocation limits

The policy for this exercise can be found in the malloc_check.rego file. You can either follow along as this exercise explains how the policy works, or try writing your own policy with the same behaviour. The firmware we are auditing is firmware_auditing_part_3, defined in xmake.lua, which contains four compartments based on the C++ files malloc1024.cc, malloc2048.cc, malloc4096.cc and malloc_many.cc. The first 3 files allocate 1024, 2048 and 4096 bytes respectively. The fourth defines a variety of heap allocation functions with varying quotas to emulate more complex firmware.

As in the last exercises, we first declare a malloc_check package, to allow us to use data.malloc_check in our queries.

For the purpose of this exercise, we need a way to check whether a given capability is an allocator capability (i.e. a sealed object, sealed by the compartment alloc, with the key MallocKey). We also need a way to decode such allocator capabilities, mapping their contents to an allocation quota.

Fortunately, cheriot-audit defines two functions that do exactly this! data.rtos.is_allocator_capability(capability) and data.rtos.decode_allocator_capability(capability) perform this functionality as described. There is also a helpful built-in rule data.rtos.all_sealed_capabilities_are_valid which decodes all allocator capabilities to ensure that they are all valid for auditing.

Using these built-in functions, we define a rule allocator_capabilities which filters through the input for allocator capabilities, and augments each with information about their compartment. This lets us define our first condition all_allocations_less_than(limit) as a parameterised function. This rule ensures that no individual allocator capability is greater than a given limit, ensuring that only a certain amount of memory can be allocated in a single malloc.

Next, we can create a rule to extract the list of unique compartments that allocate on the heap. We can do this using Rego's contains keyword and some term-matching syntax to extract the "owner" field. Using this, we now have a construct which we can use to sum all quotas within a given compartment. By using the built-in sum function, allocator_capabilities, and unique_allocator_compartments, we can define an object that maps from a given compartment to its total allocation quota.

Following from this, we can define our second allocation limiting rule: all_compartments_allocate_leq(limit). This function checks that no individual compartment can allocate memory greater than a given limit at one time, across all of its allocator capabilities. This hence ensures that only a certain amount of memory can be used by one compartment at any given time.

For our final allocation limiting rule, we first define a helper rule total_quota which sums up the quota of every allocator capability in the firmware. We use this to construct the final check total_allocation_leq(limit), which ensures that only a certain amount of memory can be used by firmware at any one time. This can be useful information for auditing firmware running on systems with limited memory resources, or with multiple processes running simultaneously.

As in our other examples, we finish by making a valid rule which evaluates to a Boolean, which audits whether our firmware image is valid. Using our 3 functions, we can easily set custom allocation limits. For this exercise, we decide that all sealed allocator capabilities must be valid, all individual allocations must be at most 20 KiB, no compartment must allocate more than 40 KiB at once, and the entire firmware must not allocate more than 100 KiB at once.

We can audit our firmware using the following command:

cheriot-audit --board=cheriot-rtos/sdk/boards/sonata.json \
              --firmware-report=build/cheriot/cheriot/release/firmware_auditing_part_3.json \
              --module=exercises/firmware_auditing/part_3/malloc_check.rego \
              --query='data.malloc_check.valid'

In this instance, the output of this test should be true, as our defined firmware meets these properties. You can check this yourself by looking at the source files and the values of the intermediary rules. To test that the policy is working, you can either change the amount of memory allocated by the firmware (making sure to rebuild), or change the policy itself to enforce lower limits. For example, changing the line

all_allocations_leq(20480)  # 20 KiB

to the new line

all_allocations_leq(10240)  # 10 KiB

should cause the valid rule of the policy to evaluate to false, because the malloc_many compartment contains a capability that permits the allocation of 16 KiB at once, which is greater than our specified limits.

Try playing around with these values to convince yourself that the policy is working as we expect it to.

Beyond these exercises

There are other pieces of information that the linker exposes, which we do not use in this exercise. For example:

• You could check that only certain compartments access certain MMIO capabilities. This is covered in the third part of the hardware access control exercise.
• You could check that only specific compartments call permitted exported functions.
• You could verify that only certain expected functions are being exported from a library.
• You could integrate this policy into SBOM verification, checking that:
  • Specific files are included.
  • The hash and size of these files matches.
  • The hash of linked third-party libraries matches known values.
  • Verify the switcher/scheduler/allocator, so that we know that the CHERIoT RTOS used is secure.

Other ideas might include writing a policy that combines the above exercises, or integrating it into the xmake build system so that a given policy is automatically run when building your firmware image.