9. Auditing firmware images

As mentioned in Section 4.13. Building software capabilities with sealing, the CHERIoT link phase emits a linker report at the same time as the final image. This is a JSON document that contains a record of the code identity for every compartment (hashes of every section before and after linking) and every way that a compartment can interact with the world outside of its private state.

The CHERIoT ABI is designed to make this all explicit. A trivial compartment has a code region that is reachable from its pcc and a globals region reachable from its cgp. Any code running in the compartment (unless explicitly constrained) has read-execute access to the former and read-write access to the latter. Any access outside of this region requires an explicit capability to be provided to the compartment's import table by the loader. The loader, in turn, will provide such a capability if, and only if, the linker has created metadata instructing it to. This means that the system fails closed. The linker creates the audit report and also creates the instructions for the loader. If these instructions are omitted, the loader will not provide the compartment with a capability and so, even if the compartment gains knowledge of some address, it does not gain rights to access any memory.

There are a lot of different kinds of capabilities that can end up in a compartment's import table. These include:

• Memory-mapped I/O regions, for direct device access.
• Pre-shared objects.
• Static sealed objects implementing software-defined capabilities (see Section 4.13. Building software capabilities with sealing)
• Local function pointers that change interrupt state.
• Imported functions from other compartments.
• Imported functions from shared libraries.

The audit report contains all of this, along with metadata such as whether functions run with interrupts disabled, whether capabilities to pre-shared objects or memory-mapped I/O regions have write access, and so on.

When you are building a compartmentalised firmware image, you can use this report in two different ways. First, you can introspect over the shape of the compartment to explore what can happen, for example determining which compartments call a specific entry point or have direct access to a device. Second, you can write policies that make sure that you have respected the principle of least privilege.

The cheriot-audit tool is intended to work with both of these approaches. It runs a Rego program over the input. Rego is a language from the OpenPolicyAgent project that is designed for writing policies over JSON documents. It inherits some ideas from JavaScript, Python, and Prolog, but broadly is intended to be a modular language for writing mostly-declarative policies that run over one or more JSON documents. Most commonly, a Rego policy is a program that evaluates to true if the policy holds.

Rego programs run by cheriot-audit can also produce longer output. Rather than simply telling you that a policy has been matched, they can create a JSON output that describes some properties of a firmware image.

9.1. Running cheriot-audit

The cheriot-audit command takes three mandatory inputs, provided as command-line arguments:

The audit report.

This is provided with the --firmware-report (or -j) flag. You will find it in the build directory, with the same name as the firmware image but a .json extension. This provides all of the information about the linked image.

The board description file.

This is provided with the --board (or -b) flag and normally in found the boards directory in the SDK, but may alternatively be provided by some other board support package. This describes the memory layout and allows policies to map from the numerical addresses in the audit report to device names.

The query to run.

This is the Rego query to run.

Rego is modular and you can also provide additional modules with --module (or -m).

To make sure that everything is working, try running a trivial query (true) against the RTOS repository's hello-world example:

$ cheriot-audit \
	--board ../../sdk/boards/sail.json \
	--firmware-report build/cheriot/cheriot/release/hello_world.json \
	-q 'true'
true

The query true simply evaluates to true as a JSON expression. This is not very interesting, but it checks that the command is working and can find all of the relevant files. You can now try running more complex examples.

Most policies will refer to one or more of the inputs, though often indirectly. You can try writing these directly as queries. If the query is input then you should see the entire audit report. If the query is data.board then you should see the board-description file.

In the rest of this chapter, we'll explore how to write more interesting queries.

9.2. Using the default cheriot-audit modules

The cheriot-audit tool has two built-in modules. The compartment module contains helper rules that are common to the compartment model. The rtos module contains helpers that specific to the CHERIoT RTOS.

Rego modules all show up in the data. namespace, like the board-description file. If you want to invoke a rule from the compartment module, it will be written as data.compartment.{rule name}.

9.3. Exploring a firmware image

Now that we can run cheriot-audit on the hello-world example, let's try to learn a bit about it. This example has no compartmentalisation and so the UART device is directly accessible in the single user-provided compartment in the example. Try this query, to see what compartments or libraries have access to the UART:

data.compartment.compartments_with_mmio_import(data.board.devices.uart)

This uses a rule from the compartments package to find any import that matches the address range provided by the board description file's uart device. If everything is built correctly (and, in particular, if you're using the correct board description file) then you should see output like this:

[
  "debug"
]

This tells us that the debug library is directly accessing the UART. Remember that CHERIoT shared libraries do not (unless they are carefully written assembly) protect their state against callers and so this means that any compartment that calls any of the entry points in that library should be assumed to be able to access the UART. Ask cheriot-audit which compartments call functions in the debug library with this query:

data.compartment.compartments_calling("debug")

This should, hopefully, tell you that only the 'hello' compartment can:

[
  "hello"
]

If you've built the firmware image with allocator or scheduler debugging enabled, the answer will be different. This is the kind of thing that's useful to capture in a policy. You might want to build firmware images where the scheduler has access to a debugging feature for testing, but you wouldn't want to sign those images for widespread deployment.

Now try running the same query against the third example from the RTOS, 03.hello_safe_compartment. This example moves UART access out to a 'uart' compartment so that the 'hello' compartment can be untrusted and just provide strings to print. You might therefore be surprised that the result of the query looks like this:

[
  "hello",
  "uart"
]

This tells you that the compartmentalisation objective—removing UART access from the hello compartment—has not been met. The hello compartment still has access to the UART via the debug library.

This is because the example prefers to give useful error messages in case of failure and includes the fail-simulator-on-error.h header. This header provides an error handler (see Section 4.10. Writing rich error handlers) that logs a message to the UART and exits the simulator if a CHERI exception occurs. If you comment out that header, the example will meet its compartmentalisation objective. Again, this is the kind of thing that's useful to have in a policy. It's useful to includes this kind of feature in debug builds, but you want to make sure that you don't leave them enabled in builds that you deploy to end users.

9.4. Decoding software-defined capabilities

CHERIoT builds a software capability model on top of the hardware capability model provided by CHERI. Software capabilities are implemented as objects that are passed around as sealed capabilities. Some of these are dynamically allocated, others are baked into the firmware image. Unless you have the sealing capability that permits unsealing a given type, these are just opaque pointers.

Sealed objects that are baked into the firmware are accessible to one compartment as an opque pointer but can be unsealed by another compartment to access their contents. The compartment that unseals them will trust their contents. You can make them trustworthy by auditing their contents at link time.

The RTOS uses software-defined capabilities to authorise memory allocation (which, in turn, is required for creating dynamically allocated sealed objects, among other things). These will show up in the audit report looking something like this:

{
  "contents": "00040000 00000000 00000000 00000000 00000000 00000000",
  "kind": "SealedObject",
  "sealing_type": {
    "compartment": "alloc",
    "key": "MallocKey",
    "provided_by": "build/cheriot/cheriot/release/cheriot.allocator.compartment",
    "symbol": "__export.sealing_type.alloc.MallocKey"
  }
}

The contents is a hex string with one block per 32-bit word. The kind identifies them as sealed objects. The sealing type tells you the compartment and the sealing key that are used to seal the object (i.e. the compartment that can unseal them and the name it gives to the key that it uses).

In the rtos package, there is a Rego rule that matches imports that are sealed with the correct value:

is_allocator_capability(capability) {
	capability.kind == "SealedObject"
	capability.sealing_type.compartment == "allocator"
	capability.sealing_type.key == "MallocKey"
}

This matches every import that refers to a sealed object that is sealed with the correct key, independent of its contents. The contents remains an opaque blob. These capabilities are 24-byte objects, where the first four bytes represent the quota and the remainder is reserved for future use (including internal use by the allocator) and must be initialised to zero. The rtos package uses the following rule to decode them:

decode_allocator_capability(capability) = decoded {
	is_allocator_capability(capability)
	some quota
	quota = integer_from_hex_string(capability.contents, 0, 4)
	# Remaining words are all zero
	integer_from_hex_string(capability.contents, 4, 4) == 0
	integer_from_hex_string(capability.contents, 8, 4) == 0
	integer_from_hex_string(capability.contents, 12, 4) == 0
	integer_from_hex_string(capability.contents, 16, 4) == 0
	integer_from_hex_string(capability.contents, 20, 4) == 0
	decoded := { "quota": quota }
}

This uses the earlier rule to check the sealing kind. If the argument is not a sealed object of the correct kind, this fails and so will any rule that tries to use the result. The quota is decoded with a built-in function provided by cheriot-audit called integer_from_hex_string. This takes the contents string, a start offset, and a width as arguments. The rule uses this to get the first word and assign it to the quota variable and then make sure that all of the others are zero.

Rego rules written like this are conjunctions. Every statement in the rule must be true. If any of the statements is not true, the rule fails. This means that, by the time we reach the end where decoded is set, the rule has checked that this is a valid allocator capability and returns a JSON object with a single field called quota containing the extracted quota. If any of the rules is false, this is not a valid allocator capability. You can use this later in policies to make sure that everything that is a sealed allocator capability is a valid allocator capability.

Most of the time, you'll use this kind of rule with a Rego comprehension. Comprehensions take some input array, filter it based on a predicate, and then use the filtered versions to construct a new array or set. For example, the following comprehension starts with every import for every compartment. For each import, the import is assigned to c and the owner of the import to owner. It then uses the is_allocator_capability predicate to filter out imports that are not allocator capabilities. Finally, for each entry that is valid it will construct a new JSON object capturing the name of the compartment that owns this capability and the decoded capability.

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

Try running this query (on the command line, you will need to remove line breaks) on a firmware image. Here's the output of running it on one of the network stack examples:

[
  {
    "capability": {
      "quota": 4096
    },
    "owner": "Firewall"
  },
  {
    "capability": {
      "quota": 16384
    },
    "owner": "SNTP"
  },
  {
    "capability": {
      "quota": 65536
    },
    "owner": "TCPIP"
  }
]

This shows that (in this specific build) the TCP/IP compartment can allocate 64 KiB of heap memory, the Firewall compartment 4 KiB and the SNTP compartment 16 KiB. Importantly, nothing else can allocate memory. You might care about what the maximum amount of heap space that all compartments are able to allocate is. A similar comprehnesion can extract the quota field from the decoded capabilities and then the built-in sum function can add all of these together:

sum([ data.rtos.decode_allocator_capability(c).quota |
    c = input.compartments[_].imports[_] ;
    data.rtos.is_allocator_capability(c) ])

In many cases, you'll be happy with quotas adding up to more than 100In other cases, you may want to make sure that a particular set of compartments can't allocate more than a fixed amount of heap space, to ensure that a certain amount is available for other uses.

9.5. Writing a policy

Rego policies for cheriot-audit will combine a lot of the building blocks that we've seen so far, as well as some helpers. The compartment module includes some helpers for defining allow lists. These are built using comprehensions similar to the ones that we looked at earlier to collect the set of compartments that can do something and then ensure that this is a subset of a provided set.

The rtos module exposes a rule called valid that performs a set of integrity checks on the RTOS. This can be used in a firmware-specific image, or parts of it can reused. It's also a good reference for the kinds of things that may appear in policies.

The RTOS policy starts with a check that all of the allocator capabilities are valid:

all_sealed_allocator_capabilities_are_valid

This uses a helper that looks similar to some of the introspection code that we've already looked at:

all_sealed_allocator_capabilities_are_valid {
	some allocatorCapabilities
	allocatorCapabilities = [ c |
		c = input.compartments[_].imports[_] ;
		is_allocator_capability(c)
	]
	every c in allocatorCapabilities {
		decode_allocator_capability(c)
	}
}

This uses a list comprehneison to collect everything that claims to be an allocator capability (i.e. everything sealed with the correct type). It then asserts that everything in this list must be a valid allocator capability by using the fact that the decode_allocator_capability rule fails if given an invalid allocator capability. If anything is sealed as an allocator capability but is not a 24-byte object where the last 20 bytes are zero, this will fail.

Next, the policy uses some allow lists to make sure that certain devices are reserved for core components:

	# Only the allocator may access the revoker.
	data.compartment.mmio_allow_list("revoker",
	                                 {"allocator"})
	# Only the scheduler may access the
	# interrupt controllers.
	data.compartment.mmio_allow_list("clint",
	                                 {"scheduler"})
	data.compartment.mmio_allow_list("plic",
	                                 {"scheduler"})

The interface to the revoker (the hardware component that invalidates capabilities to freed memory, allowing reuse) is reserved for the allocator. The core-local and platform-level interrupt controllers (CLIC and PLIC) are both reserved for the scheduler: nothing else should directly handle interrupts, the scheduler exposes APIs for other compartments to wait for or acknowledge interrupts.

Finally, it checks the access to some pre-shared objects:

	# Only the allocator may access the
	# hazard list (the switcher can
	# as well via another mechanism)
	data.compartment.shared_object_allow_list(
		"allocator_hazard_pointers",
		{"allocator"})
	# Only the allocator may write to the epoch.
	# Currently, only the compartment-helpers library
	# reads the epoch, but it isn't a security problem
	# if anything else does.
	data.compartment.shared_object_writeable_allow_list(
		"allocator_epoch",
		{"allocator"})
	# Size of hazard list and allocator epoch.
	some hazardList
	hazardList = data.compartment.shared_object(
		"allocator_hazard_pointers")
	# Two hazard pointers per thread.
	hazardList.end - hazardList.start =
		 count(input.threads) * 2 * 8
	some epoch
	epoch = data.compartment.shared_object(
		"allocator_epoch")
	# 32-bit epoch
	epoch.end - epoch.start = 4

The hazard-pointer list is used to implement the ephemeral claims mechanism described in Section 6.8. Ensuring that heap objects are not deallocated. The allocator is the only thing that should have access to it (the switcher also exposes a write-only view of a part of it for the current thread).

Concurrent access to this is mediated via a 32-bit epoch variable that is incremented when the allocator starts and finishes reading the list. This means that it is safe to write to if the value is even, and that value is safely stored if the epoch is unchanged before and after writing. This is safe for anything to read, but only the allocator should access it.

Finally, the rule checks that these are the expected size.

Together, this provides a policy that checks that the properties that the core RTOS expects hold. There are some omissions here. For example, in a release version, this policy may add checks the core RTOS components are the code expected as part of a reproducible build chain. This is not part of the core policy because it would be violated every time the toolchain changed.