From 367d09015a2784b38e8c1bcf74420f521140748a Mon Sep 17 00:00:00 2001 From: Alex Jones Date: Wed, 18 Sep 2024 11:32:58 +0100 Subject: [PATCH] Add firmware auditing exercise 2 This commit introduces exercise 2 for using CHERIoT Audit to audit firmware alongside Rego policies. This exercise involves writing a policy to ensure that only specified functions are running with interrupts disabled. --- exercises/firmware_auditing/README.md | 79 +++++++++++++++++++ .../part_2/bad_disable_interrupts.cc | 27 +++++++ .../part_2/disable_interrupts.cc | 41 ++++++++++ .../part_2/interrupt_disables.rego | 66 ++++++++++++++++ exercises/firmware_auditing/xmake.lua | 29 +++++++ 5 files changed, 242 insertions(+) create mode 100644 exercises/firmware_auditing/part_2/bad_disable_interrupts.cc create mode 100644 exercises/firmware_auditing/part_2/disable_interrupts.cc create mode 100644 exercises/firmware_auditing/part_2/interrupt_disables.rego diff --git a/exercises/firmware_auditing/README.md b/exercises/firmware_auditing/README.md index 3251e28..1aa91d1 100644 --- a/exercises/firmware_auditing/README.md +++ b/exercises/firmware_auditing/README.md @@ -84,3 +84,82 @@ This tells us where the sealed capabilty in our firmware originates - a static s 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. 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..458e418 --- /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; + } +} \ No newline at end of file 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..ce664ed --- /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); +} \ No newline at end of file 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..f5bfe5b --- /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 +} \ No newline at end of file diff --git a/exercises/firmware_auditing/xmake.lua b/exercises/firmware_auditing/xmake.lua index d98b5e7..3589618 100644 --- a/exercises/firmware_auditing/xmake.lua +++ b/exercises/firmware_auditing/xmake.lua @@ -20,3 +20,32 @@ firmware("firmware_auditing_part_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)