Auditing compartments

This example shows a simple use of the auditing tool. The code in this is very simple:

• A caesar compartment exposes interfaces to encrypt and decrypt data using a Caesar cypher.
• A producer compartment uses this to encrypt a value using a key held in a software capability.
• An entry compartment receives this encrypted data and forwards it to a consumer compartment.
• The consumer compartment receives the data and invokes the caesar compartment to decrypt it.

This is a fairly contrived example but it provides a simple structure for exploring cheriot-audit. This tool applies Rego policies to CHERIoT firmware images.

Note: For all of the cheriot-audit examples, we‘ll assume that you’re running a command something like this:

$ cheriot-audit --board=../../sdk/boards/sail.json --firmware-report=build/cheriot/cheriot/release/caesar_example.json --module=caesar.rego  --query '{query}' | jq

You may need to specify a full path to cheriot-audit (it is in /cheriot-tools/bin in the dev container). The query will be shown before the results. Piping the output to jq is optional, but will give pretty-printed output for valid JSON (remove it for places where you get an error: undefined is not rendered by jq).

The --board argument is the same as the board JSON file that you identified with the --board argument you passed to xmake (if you didn't pass a path to that, it will look in sdk/boards). The --firmware is the JSON file produced during the final firmware link step. The --module argument is the caesar.rego file that contains the policy written for this example. Finally, the --query argument is the Rego query to run.

Validating our Caesar capabilities

The capabilities for the Caesar cypher (defined in caesar_cypher.h) contain three single-byte fields:

• A permit-encrypt permission.
• A permit-decrypt permission.
• A shift value (Caesar cypher is a simple substitution cypher that rotates the alphabet, and so the ‘key’ is the amount that each letter is shifted).

These are all static sealed objects that are held by the compartment that can authorise encryption or decryption. To encrypt a message, you call the encrypt function exposed by the caesar compartment and pass it one of these capabilities. The compartment will dynamically check that it is the right kind of capability and that it permits sealing, then encrypt with the embedded shift amount.

This has the property that any compartment that holds an authorising capability can request encryption or decryption, but does not itself know the key.

To validate the properties of our keys, let's start by defining a rule that identifies whether an import is a Caesar capability:

# Check if an import is sealed with the Caesar capability type
is_sealed_caesar_capability(capability) {
    capability.kind = "SealedObject"
    capability.sealing_type.compartment = "caesar"
    capability.sealing_type.key = "CaesarCapabilityType"
}

This is a unary rule (it takes one argument). Rego rules are similar to Prolog predicates. They are not functions that return true or false, they are logical expressions that either hold or don't. This distinction rarely matters, but it can be confusing because a failure will be reported in Rego as undefined instead of false.

This rule holds (is true) if all of the rules listed on the lines between braces hold. The = operator in Rego is unification, not assignment. This means that it will try to find values on the left and right sides that allow the equality to hold.

In English, this says that the argument is a sealed Caesar capability if (and only if) its kind if SealedObject, the compartment that owns the sealing type is caesar and the sealing type is the one that this compartment exports as CaesarCapabilityType.

We can see how this works by using it with a Rego comprehension. Try running this query:

[ c | c = input.compartments[_].imports[_] ; data.caesar.is_sealed_caesar_capability(c) ]

This will evaluate to an array of values of c, where c is every import from any compartment, filtered by the rule that we've just written. The underscores are distinct anonymous variables. Because we never constrain these, they can be any value, and so this will find any compartment, and any import in that compartment, and then filter them.

Note that we refer to our rule with a data.caesar prefix. All Rego modules are imported into the data namespace with the module name as the second-level namespace.

The output should look something like this:

[
  {
    "contents": "00015f00",
    "kind": "SealedObject",
    "sealing_type": {
      "compartment": "caesar",
      "key": "CaesarCapabilityType",
      "provided_by": "build/cheriot/cheriot/release/caesar.compartment",
      "symbol": "__export.sealing_type.caesar.CaesarCapabilityType"
    }
  },
  {
    "contents": "01005f00",
    "kind": "SealedObject",
    "sealing_type": {
      "compartment": "caesar",
      "key": "CaesarCapabilityType",
      "provided_by": "build/cheriot/cheriot/release/caesar.compartment",
      "symbol": "__export.sealing_type.caesar.CaesarCapabilityType"
    }
  }
]

This has found the two capabilities that we expected to find looking for.

Decoding our Caesar capabilities

Seeing something like "contents": "01005f00" in the above example isn't that informative. Is this a valid set of values? The next step is to write something to decode these.

We'll start with a helper to convert integers into C booleans:

value_as_boolean(value) = output {
    value = 1
    output = true
}

value_as_boolean(value) = output {
    value = 0
    output = false
}

This is a Rego rule that has two definitions. The first will hold if the value is 1, and will set the result to true. The second will hold if the value is 0, and will set the result to false. If the value is anything other than 0 or 1, this rule will not hold.

Try this with the following two queries:

data.caesar.value_as_boolean(1)
data.caesar.value_as_boolean(2)

These should give true and undefined, respectively. Rego reports unification failure as undefined and this propagates upwards. Any rule that depends on a rule that is undefined will also be undefined. We can use this to make sure that the boolean values that we want are canonical true and false values, as well as decoding them.

With these defined, let's move on to the Rego rule that decodes one of these capabilities:

decode_user_key_capability(capability) = decoded {
    # Fail if this is not sealed with the Caesar capability type
    is_sealed_caesar_capability(capability)
    some permitEncrypt, permitDecrypt, shift

    # Extract the values.  Each of these will fail if the value is not as expected.
    # permitEncrypt is a (single-byte) boolean value at offset 0.
    permitEncrypt = value_as_boolean(integer_from_hex_string(capability.contents, 0, 1))

    # permitDecrypt is a (single-byte) boolean value at offset 1.
    permitDecrypt = value_as_boolean(integer_from_hex_string(capability.contents, 1, 1))

    # shift is a single-byte integer value at offset 2.
    shift = integer_from_hex_string(capability.contents, 2, 1)
    decoded = {
        "permitEncrypt": permitEncrypt,
        "permitDecrypt": permitDecrypt,
        "shift": shift,
    }
}

This starts by depending on the rule that we defined first, which will cause this to fail for anything that isn‘t a capability of the expected type. Next, we define three local variables to hold the three fields that we expect. We’ll extract each of these using integer_from_hex_string, a built-in function provided by cheriot-audit. This takes a string, an offset, and a length and will decode a little-endian integer from the hex string provided. We‘re extracting three one-byte integers at offsets 0, 1, and 2. We’re then converting the first two to booleans.

Finally, if all of that worked, we‘re returning a new object that mirrors the C structure that represents our capability. We can use this with another comprehension to extract and decode all valid capabilities. This is sufficiently useful that we’ll define a new rule for it:

all_valid_caesar_capabilities = [{"owner": owner, "capability": decode_user_key_capability(c)} | c = input.compartments[owner].imports[_];         is_sealed_caesar_capability(c)]

This is a slightly more complex comprehension. The result is defining a new object with both the owner and the decoded capability. Try running this:

data.caesar.all_valid_caesar_capabilities

You should see something like this:

[
  {
    "capability": {
      "permitDecrypt": true,
      "permitEncrypt": false,
      "shift": 95
    },
    "owner": "consumer"
  },
  {
    "capability": {
      "permitDecrypt": false,
      "permitEncrypt": true,
      "shift": 95
    },
    "owner": "producer"
  }
]

Check these values with the ones declared in the source code (in producer.cc and consumer.cc).

Defining our requirements

Now that we have all of the helpers that let us inspect the linked image, let‘s define a valid rule that defines the policy for our linked compartment. We’ll start here by depending on the valid rule from the RTOS itself:

    data.rtos.valid

This performs some sanity checking on the RTOS core, such as ensuring that only the allocator can read hazard-pointer slots, that allocator capabilities are all valid, and so on.

Next, we'll make sure that we have the right number of Caesar capabilities and that the number of valid Caesar capabilities is the same:

    # There are two things sealed with the Caesar capability type
    count([c | c = input.compartments[owner].imports[_]; is_sealed_caesar_capability(c)]) = 2

    # Both of them are valid Caesar capabilities
    count(all_valid_caesar_capabilities) = 2

The first of these will find everything that is sealed as a Caesar capability, the second will find only ones that decode correctly. We know that only the producer and consumer compartments should hold these capabilities, so we check that the number found is two.

Having done that, we extract the two capabilities that we expect to exist:

    some producerCapability, consumerCapability
    producerCapability = [c | c = all_valid_caesar_capabilities[_]; c.owner = "producer"][0].capability
    consumerCapability = [c | c = all_valid_caesar_capabilities[_]; c.owner = "consumer"][0].capability

Each of these starts with a comprehension that filters the set of all Caesar capabilities to find the ones with the named owner and then extracts the capability. Note that, in this case, we can assume that there is a single value here and so hard code array index 0. If that assumption is incorrect then either our previous assertion that there are two capabilities in total, or a later assertion where we inspect properties of the capabilities, will fail.

Now that we have these, ensure that the producer is permitted to encrypt and the consumer to decrypt, but not vice versa.

    producerCapability.permitEncrypt = true
    producerCapability.permitDecrypt = false
    consumerCapability.permitEncrypt = false
    consumerCapability.permitDecrypt = true

We expect the consumer to be able to decrypt things encrypted by the producer, so let's also make sure that their shift values are the same:

producerCapability.shift = consumerCapability.shift

Finally, for some defence in depth, let's make sure that the producer is the only caller of the encrypt function and the consumer the only caller of the decrypt function:

    data.compartment.compartment_call_allow_list("caesar", "caesar_encrypt.*", {"producer"})
    data.compartment.compartment_call_allow_list("caesar", "caesar_decrypt.*", {"consumer"})

This is not necessary in theory, because these require an authorising capability and so another compartment calling them should fail. Another compartment trying to call them is definitely a bug though, so it‘s worth checking. Similarly, let’s make sure that the producer and consumer are called only from the entry compartment

    data.compartment.compartment_call_allow_list("producer", "produce_message.*", {"entry"})
    data.compartment.compartment_call_allow_list("consumer", "consume_message.*", {"entry"})

Putting this all together, we can now run a very simple query:

data.caesar.valid

If this all worked, the result should be simply true.

A policy like this can be included in CI to make sure that everything that you commit meets the policy. It can drive key release for code signing, so that you never sign a firmware image that doesn't meet your policy. Along the way to writing the final policy, we built a set of tools for introspection on the firmware image, so you can query properties.

Note on cryptography

This example uses a Caesar Cypher. This was chosen because it is easy to implement, not because it is secure. Post-quantum encryption algorithms are designed to be robust against hypothetical quantum computers. Modern classical encryption algorithms are robust against attacks by large classical computers. The Caesar Cypher is not robust against a person with a pen and paper.

Under no circumstances should you copy the encryption portion of this code into anything that needs to be robust in the presence of an adversary with ten minutes and a piece of paper. Breaking Caesar Cyphers is a fun thing for small children to do, not a challenge for a real cryptanalyst.

All of that said, the same mechanisms used in this example can be used with more sensible encryption schemes to ensure key confidentiality.