Review exercises docs

exercises/README.md

@@ -16,4 +16,4 @@ xmake -P exercises
 
 ## Exercises
 
-Currently, there is one exercise: [Hardware Access Control](./hardware_access_control/README.md)
+Currently, there is one exercise: [Hardware Access Control](./hardware_access_control/)

exercises/hardware_access_control/README.md

@@ -8,7 +8,7 @@ If you haven't already, pop yourself up to the '[building the exercises][]' sect
 
 [Building the Exercises]: ../README.md#building-the-exercises
 
-This exercise we utilise the compartmentalisation available in CHERIoT RTOS to control access to a hardware peripheral: the very security critical LEDs.
+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.
 
@@ -19,9 +19,7 @@ For this exercise, when the [`xmake.lua`][] build file is mentioned `exercises/h
 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/`][].
-
-[`exercises/hardware_access_control/part_1/`]: ../../exercises/hardware_access_control/part_1/
+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.
@@ -51,15 +49,12 @@ When a compartment seals a capability, it can no longer be dereferenced or modif
 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/`][].*
-
-[`cheriot-rtos/examples/05.sealing/`]: ../../cheriot-rtos/examples/05.sealing/
+*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/`][].
+Take a moment to look at the sources for these compartments in `exercises/hardware_access_control/part_2/`.
 
-[`exercises/hardware_access_control/part_2/`]: ../../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][running on fpga], the following message will pop up.
@@ -98,7 +93,6 @@ hardware_access_control/part_2/led_walk_dynamic.cc:34 Assertion failure in start
 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?
@@ -112,7 +106,7 @@ To automate checking this report, we can use `cheriot-audit` which should alread
 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 `cheriot-audit`'s included compartment package to check only the `gpio_access` compartment has access to the GPIO MMIOs.
+It uses `mmio_allow_list` from the compartment package 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.
 
@@ -147,7 +141,7 @@ check_gpio_access whitelisted_compartments_only \
 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 `cheriot-audit`'s included compartment package in [`cheriot-audit`'s readme][compartment package].
+One can browse the other functions available as part of the compartment package in [`cheriot-audit`'s readme][compartment package].
 
 [compartment package]: https://github.com/CHERIoT-Platform/cheriot-audit/blob/main/README.md#the-compartment-package