Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 3 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,8 @@ After you are all set up, take a look at the [exercises][].
## 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.*
This repository wraps the [`cheriot-rtos`][], which is included in this repository as a submodule.
[`cheriot-rtos`][] contains the CHERIoT software stack as well as drivers for using the Sonata board; it is well documented by the [CHERIoT Programmer's Guide][].

Other repositories of note:
- [`sonata-system`][]: holds the Sonata system RTL and bootloader which come together to generate the bitstream.
Expand All @@ -27,8 +25,7 @@ Other repositories of note:
For hardware documentation, see the [Sonata system book][].

[`sonata-software`]: https://github.com/lowRISC/sonata-software
[`lowrisc/cheriot-rtos`]: https://github.com/lowRISC/cheriot-rtos
[`CHERIoT-Platform/cheriot-rtos`]: https://github.com/CHERIoT-Platform/cheriot-rtos
[`cheriot-rtos`]: https://github.com/CHERIoT-Platform/cheriot-rtos
[`sonata-system`]: https://github.com/lowRISC/sonata-system
[`sonata-rp2040`]: https://github.com/newaetech/sonata-rp2040
[`CHERIoT-Platform/llvm-project`]: https://github.com/CHERIoT-Platform/llvm-project
Expand Down
8 changes: 1 addition & 7 deletions exercises/firmware_auditing/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,21 +5,15 @@ SPDX-License-Identifier: Apache-2.0
# Firmware auditing exercise

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

[building the exercises]: ../README.md#building-the-exercises

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.

[building the exercises]: ../README.md#building-the-exercises
[auditing firmware]: ../../doc/auditing-firmware.md

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`][].

[`exercises/firmware_auditing/xmake.lua`]: ../../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.
Expand Down
12 changes: 4 additions & 8 deletions exercises/hardware_access_control/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,9 @@ SPDX-License-Identifier: Apache-2.0
# Hardware access control exercise

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

[Building the Exercises]: ../README.md#building-the-exercises

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.

[`xmake.lua`]: ../../exercises/hardware_access_control/xmake.lua
[Building the Exercises]: ../README.md#building-the-exercises

## Part 1

Expand All @@ -21,6 +16,7 @@ This image has two threads running two compartments: `blinky_raw` and `led_walk_
Compartment `blinky_raw` simply toggles an LED and compartment `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/`][].

[`xmake.lua`]: ../../exercises/hardware_access_control/xmake.lua
[`exercises/hardware_access_control/part_1/`]: https://github.com/lowRISC/sonata-software/tree/main/exercises/hardware_access_control/part_1

Let's look inside [`blinky_raw`][].
Expand Down Expand Up @@ -159,5 +155,5 @@ Where to go from here...
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](mailto:info@lowrisc.org).
- There is a technical interest group run by lowRISC focussing on CHERI technology, and specifically through the [COSMIC project](https://cosmic-project.lowrisc.org/).
If you are interested in joining please reach out to [info@lowrisc.org](mailto:info@lowrisc.org).