diff --git a/doc/auditing-firmware.md b/doc/auditing-firmware.md new file mode 100644 index 0000000..0a00087 --- /dev/null +++ b/doc/auditing-firmware.md @@ -0,0 +1,174 @@ +# 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**](https://github.com/CHERIoT-Platform/cheriot-audit/blob/main/README.md): the source for `cheriot-audit`. + - [**Rego OPA Documentation**](https://www.openpolicyagent.org/docs/latest/policy-language/): documentation for Rego, the policy language used by CHERIoT Audit. + - [**CHERIoT Programmer's Guide**](https://cheriot.org/book/): 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]: https://www.openpolicyagent.org/docs/latest/policy-language/ + +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: + +[getting started guide]: ../doc/getting-started.md +[standard build flow]: ../doc/exploring-cheriot-rtos.md#build-system + +```sh +# 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: +```json +[{"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`](https://www.openpolicyagent.org/integrations/vscode-opa/) extension for VSCode and the [`zed-rego`][] extension for Zed provide syntax highlighting and a language server for linting functionality. + +[`vscode-opa`]: https://www.openpolicyagent.org/integrations/vscode-opa/ +[`zed-rego`]: https://github.com/StyraInc/zed-rego + +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: + +```python # This is Rego, not Python, but we at least get a tiny bit of highlighting +package my_example + +import future.keywords + +example_function_1(arg1, arg2) { + ... +} + +example_function2() { + ... +} +``` +You might then use `cheriot-audit` via a command like: +```sh +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][]. + +[Rego documentation]: https://www.openpolicyagent.org/docs/latest/policy-language/ + +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)`. + +[Prolog]: https://www.dai.ed.ac.uk/groups/ssp/bookpages/quickprolog/node12.html + +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: +```python # This is Rego, not python, but it gives us some syntax highlighting +[ { "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: +```python +[{"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. diff --git a/exercises/README.md b/exercises/README.md index f70d492..8b49286 100644 --- a/exercises/README.md +++ b/exercises/README.md @@ -16,4 +16,6 @@ xmake -P exercises ## Exercises -Currently, there is one exercise: [Hardware Access Control](./hardware_access_control/) +Currently, there are two exercises: + - [Hardware Access Control](./hardware_access_control/) + - [Firmware Auditing](./firmware_auditing/) diff --git a/exercises/firmware_auditing/README.md b/exercises/firmware_auditing/README.md new file mode 100644 index 0000000..a1b58b8 --- /dev/null +++ b/exercises/firmware_auditing/README.md @@ -0,0 +1,249 @@ + +# 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. + +[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. +If you find yourself confused whilst going through this exercise, it might be helpful to read over the [introduction to Rego][] in the documentation. + +[introduction to Rego]: ../../doc/auditing-firmware.md#a-quick-introduction-to-rego + +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. + +[`no_sealed_capabilities.rego`]: ../../exercises/firmware_auditing/part_1/no_sealed_capabilities.rego +[`xmake.lua`]: ../../exercises/firmware_auditing/xmake.lua +[`sealed_capability.cc`]: ../../exercises/firmware_auditing/part_1/sealed_capability.cc + +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-in`count` 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: + +```sh +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`. + +[`sealed_capability.cc`]: ../../exercises/firmware_auditing/part_1/sealed_capability.cc + +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: + +```json +[{"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`][]. + +[`interrupt_disables.rego`]: ../../exercises/firmware_auditing/part_2/interrupt_disables.rego +[`xmake.lua`]: ../../exercises/firmware_auditing/xmake.lua +[`disable_interrupts.cc`]: ../../exercises/firmware_auditing/part_2/disable_interrupts.cc +[`bad_disable_interrupts.cc`]: ../../exercises/firmware_auditing/part_2/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. + +[CHERIoT Programmer's Guide]: https://cheriot.org/book/language_extensions.html#_interrupt_state_control + +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: +```sh +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. + +[`malloc_check.rego`]: ../../exercises/firmware_auditing/part_3/malloc_check.rego +[`xmake.lua`]: ../../exercises/firmware_auditing/xmake.lua +[`malloc1024.cc`]: ../../exercises/firmware_auditing/part_3/malloc1024.cc +[`malloc2048.cc`]: ../../exercises/firmware_auditing/part_3/malloc2048.cc +[`malloc4096.cc`]: ../../exercises/firmware_auditing/part_3/malloc4096.cc +[`malloc_many.cc`]: ../../exercises/firmware_auditing/part_3/malloc_many.cc + +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: +```sh +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](https://en.wikipedia.org/wiki/Software_supply_chain) 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. + +[hardware access control]: ../hardware_access_control/README.md#part-3 + +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. diff --git a/exercises/firmware_auditing/part_1/no_sealed_capabilities.rego b/exercises/firmware_auditing/part_1/no_sealed_capabilities.rego new file mode 100644 index 0000000..da67026 --- /dev/null +++ b/exercises/firmware_auditing/part_1/no_sealed_capabilities.rego @@ -0,0 +1,26 @@ +# Copyright lowRISC Contributors. +# SPDX-License-Identifier: Apache-2.0 +package no_seal + +is_sealed_capability(capability) { + capability.kind == "SealedObject" +} + +no_sealed_capabilities_exist { + sealedCapabilities := [ cap | cap = input.compartments[_].imports[_] ; is_sealed_capability(cap) ] + count(sealedCapabilities) == 0 +} + +sealed_capability_info := [ + {"contents": cap.contents, + "key": cap.sealing_type.key, + "compartment": cap.sealing_type.compartment, + "owner": owner + } | cap = input.compartments[owner].imports[_] + ; data.no_seal.is_sealed_capability(cap) +] + +default valid = false +valid = true { + no_sealed_capabilities_exist +} diff --git a/exercises/firmware_auditing/part_1/sealed_capability.cc b/exercises/firmware_auditing/part_1/sealed_capability.cc new file mode 100644 index 0000000..921ebec --- /dev/null +++ b/exercises/firmware_auditing/part_1/sealed_capability.cc @@ -0,0 +1,30 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#include +#include +#include + +static constexpr uint32_t LedIdx = 7; +static constexpr size_t ArrSize = 32; + +void __cheri_compartment("sealed_capability") do_things() +{ + auto gpio = MMIO_CAPABILITY(SonataGPIO, gpio); + + uint32_t arr[ArrSize]; + // Comment the above line and uncomment the below line to allocate on the + // heap! + // uint32_t *arr = new uint32_t[ArrSize]; + + for (size_t i = 0; i < ArrSize; i++) + { + arr[i] = i; + } + + while (true) + { + gpio->led_toggle(LedIdx); + thread_millisecond_wait(500); + } +} diff --git a/exercises/firmware_auditing/part_2/bad_disable_interrupts.cc b/exercises/firmware_auditing/part_2/bad_disable_interrupts.cc new file mode 100644 index 0000000..4d5aef6 --- /dev/null +++ b/exercises/firmware_auditing/part_2/bad_disable_interrupts.cc @@ -0,0 +1,27 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#include + +[[cheri::interrupt_state(disabled)]] int not_allowed() +{ + int x = 0; + x += 1; + return x; +} + +[[gnu::noinline]] int other_function() +{ + return 1000000; +} + +/// Thread entry point. +void __cheri_compartment("bad_disable_interrupts") entry_point() +{ + int y = not_allowed(); + other_function(); + while (y < other_function()) + { + y += 1; + } +} diff --git a/exercises/firmware_auditing/part_2/disable_interrupts.cc b/exercises/firmware_auditing/part_2/disable_interrupts.cc new file mode 100644 index 0000000..b7ad2ee --- /dev/null +++ b/exercises/firmware_auditing/part_2/disable_interrupts.cc @@ -0,0 +1,41 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#include + +[[gnu::noinline]] [[cheri::interrupt_state(disabled)]] int +run_without_interrupts(int x) +{ + return x + 1; +} + +[[gnu::noinline]] [[cheri::interrupt_state(disabled)]] void +also_without_interrupts(int *x) +{ + *x = 1; +} + +[[gnu::noinline]] void other_function_one() +{ + int x = 3; +} + +[[gnu::noinline]] int other_function_two() +{ + return 3; +} + +[[gnu::noinline]] int other_function_three(int arg1, int arg2) +{ + return arg1 + arg2; +} + +/// Thread entry point. +void __cheri_compartment("disable_interrupts") entry_point() +{ + other_function_one(); + int y = other_function_two(); + y = run_without_interrupts(3); + y += other_function_three(4, 7); + also_without_interrupts(&y); +} diff --git a/exercises/firmware_auditing/part_2/interrupt_disables.rego b/exercises/firmware_auditing/part_2/interrupt_disables.rego new file mode 100644 index 0000000..ee4e1e2 --- /dev/null +++ b/exercises/firmware_auditing/part_2/interrupt_disables.rego @@ -0,0 +1,66 @@ +# Copyright lowRISC Contributors. +# SPDX-License-Identifier: Apache-2.0 +package interrupts + +import future.keywords + +# Note - Any compartment not in this array is not checked by default, +# and so are allowed to have disabled interrupts. +required_disabled_interrupts := [ + { + "compartment": "disable_interrupts", + "functions": {"run_without_interrupts(int)", "also_without_interrupts(int*)"} + }, { + "compartment": "bad_disable_interrupts", + "functions": {} + # Uncomment the below line (and comment the above line) to allow the disallowed + # function to be run with interrupts disabled + #"functions": {"not_allowed()"} + } +] +required_compartments := {x.compartment | x = required_disabled_interrupts[_]} + +all_exports := [ + {"owner": owner, "export": export} | export = input.compartments[owner].exports[_] +] + +all_required_compartments_present { + compartments := {name | input.compartments[name]} + required_compartments == required_compartments & compartments +} + +exports_with_interrupt_status(status) := [ + export | export = all_exports[_] ; export["export"]["interrupt_status"] = status +] + +patched_export_entry_demangle(compartment, export_symbol) := demangled { + startswith(export_symbol, "__library_export_") + modified_export = concat("", ["__export_", substring(export_symbol, 17, -1)]) + demangled := export_entry_demangle(compartment, modified_export) +} +patched_export_entry_demangle(compartment, export_symbol) := demangled { + not startswith(export_symbol, "__library_export_") + demangled := export_entry_demangle(compartment, export_symbol) +} + +compartment_only_required_disabled_interrupts(compartment) { + symbols := { + patched_export_entry_demangle(e["owner"], e["export"]["export_symbol"]) | + e = exports_with_interrupt_status("disabled")[_] ; + e["owner"] = compartment["compartment"] + } + required := {func | _ = compartment["functions"][func]} + symbols == required +} + +only_required_disabled_interrupts_present { + every compartment in required_disabled_interrupts { + compartment_only_required_disabled_interrupts(compartment) + } +} + +default valid := false +valid { + all_required_compartments_present + only_required_disabled_interrupts_present +} diff --git a/exercises/firmware_auditing/part_3/malloc1024.cc b/exercises/firmware_auditing/part_3/malloc1024.cc new file mode 100644 index 0000000..029243e --- /dev/null +++ b/exercises/firmware_auditing/part_3/malloc1024.cc @@ -0,0 +1,19 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#define MALLOC_QUOTA 1024 // Quota of 1 KiB + +#include + +/// Thread entry point. +[[noreturn]] void __cheri_compartment("malloc1024") entry_point() +{ + void *mem = malloc(1024 * sizeof(char)); + free(mem); + + int x = 0; + while (true) + { + x = x + 1; + }; +} diff --git a/exercises/firmware_auditing/part_3/malloc2048.cc b/exercises/firmware_auditing/part_3/malloc2048.cc new file mode 100644 index 0000000..2e32cb2 --- /dev/null +++ b/exercises/firmware_auditing/part_3/malloc2048.cc @@ -0,0 +1,19 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#define MALLOC_QUOTA 2048 // Quota of 2 KiB + +#include + +/// Thread entry point. +[[noreturn]] void __cheri_compartment("malloc2048") entry_point() +{ + void *mem = malloc(2048 * sizeof(char)); + free(mem); + + int x = 0; + while (true) + { + x = x + 1; + }; +} diff --git a/exercises/firmware_auditing/part_3/malloc4096.cc b/exercises/firmware_auditing/part_3/malloc4096.cc new file mode 100644 index 0000000..6edafea --- /dev/null +++ b/exercises/firmware_auditing/part_3/malloc4096.cc @@ -0,0 +1,19 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#define MALLOC_QUOTA 4096 // Quota of 4 KiB + +#include + +/// Thread entry point. +[[noreturn]] void __cheri_compartment("malloc4096") entry_point() +{ + void *mem = malloc(4096 * sizeof(char)); + free(mem); + + int x = 0; + while (true) + { + x = x + 1; + }; +} diff --git a/exercises/firmware_auditing/part_3/malloc_check.rego b/exercises/firmware_auditing/part_3/malloc_check.rego new file mode 100644 index 0000000..32caa23 --- /dev/null +++ b/exercises/firmware_auditing/part_3/malloc_check.rego @@ -0,0 +1,51 @@ +# Copyright lowRISC Contributors. +# SPDX-License-Identifier: Apache-2.0 +package malloc_check + +import future.keywords + +allocator_capabilities := [ + {"owner": owner, "capability": data.rtos.decode_allocator_capability(cap)} | + cap = input.compartments[owner].imports[_] ; + data.rtos.is_allocator_capability(cap) +] + +all_allocations_leq(limit) { + every cap in allocator_capabilities { + cap.capability.quota <= limit + } +} + +unique_allocator_compartments contains owner if { + some {"owner": owner} in allocator_capabilities +} + +total_quota_per_compartment[owner] = quota if { + some owner in unique_allocator_compartments + quota := sum([cap.capability.quota | cap = allocator_capabilities[_]; cap.owner == owner]) +} + +all_compartments_allocate_leq(limit) { + some quotas + quotas = [ quota | quota = total_quota_per_compartment[_] ] + every quota in quotas { + quota <= limit + } +} + +total_quota := sum([cap.capability.quota | cap = allocator_capabilities[_]]) + +total_allocation_leq(limit) { + total_quota <= limit +} + +default valid := false +valid { + data.rtos.all_sealed_allocator_capabilities_are_valid + # No individual allocation should be able to allocate more than 20 KiB at one time + all_allocations_leq(20480) + # No individual compartment should be able to allocate more than 40 KiB simultaneously + all_compartments_allocate_leq(40960) + # The entire firmware image cannot allocate more than 100 KiB simultaneously + total_allocation_leq(102400) +} diff --git a/exercises/firmware_auditing/part_3/malloc_many.cc b/exercises/firmware_auditing/part_3/malloc_many.cc new file mode 100644 index 0000000..8974b8c --- /dev/null +++ b/exercises/firmware_auditing/part_3/malloc_many.cc @@ -0,0 +1,58 @@ +// Copyright lowRISC Contributors. +// SPDX-License-Identifier: Apache-2.0 + +#define MALLOC_QUOTA 1024 // Quota of 1 KiB + +#include + +DECLARE_AND_DEFINE_ALLOCATOR_CAPABILITY(__second_malloc_capability, + MALLOC_QUOTA * 2) +DECLARE_AND_DEFINE_ALLOCATOR_CAPABILITY(__third_malloc_capability, + MALLOC_QUOTA * 4) +DECLARE_AND_DEFINE_ALLOCATOR_CAPABILITY(__fourth_malloc_capability, + MALLOC_QUOTA * 8) +DECLARE_AND_DEFINE_ALLOCATOR_CAPABILITY(__fifth_malloc_capability, + MALLOC_QUOTA * 16) +#define MALLOC_CAPABILITY_2 STATIC_SEALED_VALUE(__second_malloc_capability) +#define MALLOC_CAPABILITY_3 STATIC_SEALED_VALUE(__third_malloc_capability) +#define MALLOC_CAPABILITY_4 STATIC_SEALED_VALUE(__fourth_malloc_capability) +#define MALLOC_CAPABILITY_5 STATIC_SEALED_VALUE(__fifth_malloc_capability) + +#define MALLOC_WITH_CAPABILITY_FUNC(name, malloc_num) \ + static inline void *malloc##malloc_num(size_t size) \ + { \ + Timeout t = {0, MALLOC_WAIT_TICKS}; \ + void *ptr = \ + heap_allocate(&t, name, size, AllocateWaitRevocationNeeded); \ + if (!__builtin_cheri_tag_get(ptr)) \ + { \ + ptr = NULL; \ + } \ + return ptr; \ + } + +MALLOC_WITH_CAPABILITY_FUNC(MALLOC_CAPABILITY_2, 2) +MALLOC_WITH_CAPABILITY_FUNC(MALLOC_CAPABILITY_3, 3) +MALLOC_WITH_CAPABILITY_FUNC(MALLOC_CAPABILITY_4, 4) +MALLOC_WITH_CAPABILITY_FUNC(MALLOC_CAPABILITY_5, 5) + +/// Thread entry point. +[[noreturn]] void __cheri_compartment("malloc_many") entry_point() +{ + void *mem = malloc(MALLOC_QUOTA * sizeof(char)); + free(mem); + void *mem2 = malloc2(MALLOC_QUOTA * 2 * sizeof(char)); + free(mem2); + void *mem3 = malloc3(MALLOC_QUOTA * 4 * sizeof(char)); + free(mem3); + void *mem4 = malloc4(MALLOC_QUOTA * 8 * sizeof(char)); + free(mem4); + void *mem5 = malloc5(MALLOC_QUOTA * 16 * sizeof(char)); + free(mem5); + + int x = 0; + while (true) + { + x = x + 1; + }; +} diff --git a/exercises/firmware_auditing/xmake.lua b/exercises/firmware_auditing/xmake.lua new file mode 100644 index 0000000..cd09cf2 --- /dev/null +++ b/exercises/firmware_auditing/xmake.lua @@ -0,0 +1,98 @@ +-- Copyright lowRISC Contributors. +-- SPDX-License-Identifier: Apache-2.0 + +-- Part 1 +compartment("sealed_capability") + add_files("part_1/sealed_capability.cc") + +firmware("firmware_auditing_part_1") + add_deps("freestanding", "sealed_capability") + on_load(function(target) + target:values_set("board", "$(board)") + target:values_set("threads", { + { + compartment = "sealed_capability", + priority = 2, + entry_point = "do_things", + stack_size = 0x200, + trusted_stack_frames = 1 + }, + }, {expand = false}) + end) + after_link(convert_to_uf2) + +-- Part 2 +compartment("disable_interrupts") + add_files("part_2/disable_interrupts.cc") + +compartment("bad_disable_interrupts") + add_files("part_2/bad_disable_interrupts.cc") + +firmware("firmware_auditing_part_2") + add_deps("freestanding", "disable_interrupts", "bad_disable_interrupts") + on_load(function(target) + target:values_set("board", "$(board)") + target:values_set("threads", { + { + compartment = "disable_interrupts", + priority = 1, + entry_point = "entry_point", + stack_size = 0x200, + trusted_stack_frames = 1 + }, { + compartment = "bad_disable_interrupts", + priority = 2, + entry_point = "entry_point", + stack_size = 0x200, + trusted_stack_frames = 1 + } + }, {expand = false}) + end) + after_link(convert_to_uf2) + +-- Part 3 +compartment("malloc1024") + add_files("part_3/malloc1024.cc") + +compartment("malloc2048") + add_files("part_3/malloc2048.cc") + +compartment("malloc4096") + add_files("part_3/malloc4096.cc") + +compartment("malloc_many") + add_files("part_3/malloc_many.cc") + +firmware("firmware_auditing_part_3") + add_deps("freestanding", "malloc1024", "malloc2048", "malloc4096", "malloc_many") + on_load(function(target) + target:values_set("board", "$(board)") + target:values_set("threads", { + { + compartment = "malloc1024", + priority = 4, + entry_point = "entry_point", + stack_size = 0x200, + trusted_stack_frames = 2 + }, { + compartment = "malloc2048", + priority = 3, + entry_point = "entry_point", + stack_size = 0x200, + trusted_stack_frames = 2 + }, { + compartment = "malloc4096", + priority = 2, + entry_point = "entry_point", + stack_size = 0x200, + trusted_stack_frames = 2 + }, { + compartment = "malloc_many", + priority = 1, + entry_point = "entry_point", + stack_size = 0x200, + trusted_stack_frames = 2 + } + }, {expand = false}) + end) + after_link(convert_to_uf2) diff --git a/exercises/xmake.lua b/exercises/xmake.lua index be32a36..8350cda 100644 --- a/exercises/xmake.lua +++ b/exercises/xmake.lua @@ -13,4 +13,4 @@ includes("../common.lua") option("board") set_default("sonata-prerelease") -includes("hardware_access_control") +includes("hardware_access_control", "firmware_auditing")