diff --git a/.clang-tidy b/.clang-tidy
index 43eb5ff..9c44d7f 100644
--- a/.clang-tidy
+++ b/.clang-tidy
@@ -1,4 +1,4 @@
-Checks:          'clang-diagnostic-*,-clang-diagnostic-error,google-readability-casting,readability-else-after-return,performance-unnecessary-copy-initialization,bugprone-use-after-move,modernize-use-nullptr,modernize-redundant-void-arg,modernize-return-braced-init-list,modernize-use-default-member-init,modernize-use-equals-default,modernize-use-equals-delete,modernize-use-nodiscard,modernize-use-override,cppcoreguidelines-avoid-goto,misc-unconventional-assign-operator,cppcoreguidelines-narrowing-conversions,bugprone-assert-side-effect,bugprone-bool-pointer-implicit-conversion,bugprone-copy-constructor-init,bugprone-forwarding-reference-overload,bugprone-macro-parentheses,bugprone-macro-repeated-side-effects,bugprone-move-forwarding-reference,bugprone-misplaced-widening-cast,bugprone-swapped-arguments,bugprone-undelegated-constructor,bugprone-unused-raii,cert-dcl21-cpp,llvm-namespace-comment,misc-static-assert,misc-redundant-expression,modernize-loop-convert,readability-non-const-parameter,readability-identifier-naming'
+Checks: 'clang-diagnostic-*,-clang-diagnostic-error,google-readability-casting,readability-else-after-return,performance-unnecessary-copy-initialization,bugprone-use-after-move,modernize-use-nullptr,modernize-redundant-void-arg,modernize-return-braced-init-list,modernize-use-default-member-init,modernize-use-equals-default,modernize-use-equals-delete,modernize-use-nodiscard,modernize-use-override,cppcoreguidelines-avoid-goto,misc-unconventional-assign-operator,cppcoreguidelines-narrowing-conversions,bugprone-assert-side-effect,bugprone-bool-pointer-implicit-conversion,bugprone-copy-constructor-init,bugprone-forwarding-reference-overload,bugprone-macro-parentheses,bugprone-macro-repeated-side-effects,bugprone-move-forwarding-reference,bugprone-misplaced-widening-cast,bugprone-swapped-arguments,bugprone-undelegated-constructor,bugprone-unused-raii,cert-dcl21-cpp,llvm-namespace-comment,misc-static-assert,misc-redundant-expression,modernize-loop-convert,readability-non-const-parameter,readability-identifier-naming,readability-braces-around-statements'
 FormatStyle: file
 UseColor: true
 WarningsAsErrors: false
diff --git a/.github/workflows/test-new-xmake-nightly.yml b/.github/workflows/test-new-xmake-nightly.yml
new file mode 100644
index 0000000..eac04ab
--- /dev/null
+++ b/.github/workflows/test-new-xmake-nightly.yml
@@ -0,0 +1,41 @@
+name: Nightly xmake test
+
+on:
+  schedule:
+    - cron: '0 0 * * *'
+  workflow_dispatch:
+
+jobs:
+  run-tests:
+    strategy:
+      fail-fast: false
+    runs-on: ubuntu-latest
+    container:
+      image: ghcr.io/cheriot-platform/devcontainer:latest
+      options: --user 1001
+    steps:
+    - name: Checkout repository and submodules
+      uses: actions/checkout@v3
+      with:
+        submodules: recursive
+    - name: Build latest xmake
+      run: |
+        xmake update dev
+        sudo apt remove -y xmake
+        echo ~/.xmake/profile
+        . ~/.xmake/profile
+    - name: Build tests
+      run: |
+        pwd
+        echo ~/.xmake/profile
+        which xmake
+        xmake --version
+        cd tests
+        xmake f --board=${{ matrix.board }} --sdk=/cheriot-tools/ ${{ matrix.build-flags }}
+        xmake
+    - name: Run tests
+      run: |
+        . ~/.xmake/profile
+        xmake --version
+        cd tests
+        xmake run
diff --git a/docs/GettingStarted.md b/docs/GettingStarted.md
index d97e2b0..f601025 100644
--- a/docs/GettingStarted.md
+++ b/docs/GettingStarted.md
@@ -79,7 +79,7 @@
  - The LLVM-based toolchain with CHERIoT support
  - The emulator generated from the Sail formal model of the CHERIoT ISA
  - The xmake build tool
- - [Sonata only] u2futils to create images that Sonata's loader can boot
+ - [Sonata only] uf2utils to create images that Sonata's loader can boot
 
 Building LLVM is fairly simple, but requires a fast machine and several GiBs of disk space.
 Building the executable model requires a working ocaml installation.
@@ -224,7 +224,7 @@
 # apt install xmake
 ```
 
-### Installing u2futils
+### Installing uf2utils
 
 If you are working with Sonata, you will need to convert the ELF files that the linker produces to [USB Flashing Format (UF2)](https://github.com/microsoft/uf2).
 The firmware on the RPi 2040 on the Sonata board can then load these files onto the CHERIoT Ibex and run them.
diff --git a/examples/06.producer-consumer/producer.cc b/examples/06.producer-consumer/producer.cc
index a4ea318..417505a 100644
--- a/examples/06.producer-consumer/producer.cc
+++ b/examples/06.producer-consumer/producer.cc
@@ -16,17 +16,16 @@
 void __cheri_compartment("producer") run()
 {
 	// Allocate the queue
-	SObj sendHandle;
-	SObj receiveHandle;
+	SObj queue;
 	non_blocking<queue_create_sealed>(
-	  MALLOC_CAPABILITY, &sendHandle, &receiveHandle, sizeof(int), 16);
+	  MALLOC_CAPABILITY, &queue, sizeof(int), 16);
 	// Pass the queue handle to the consumer.
-	set_queue(receiveHandle);
+	set_queue(queue);
 	Debug::log("Starting producer loop");
 	// Loop, sending some numbers to the other thread.
 	for (int i = 1; i < 200; i++)
 	{
-		int ret = blocking_forever<queue_send_sealed>(sendHandle, &i);
+		int ret = blocking_forever<queue_send_sealed>(queue, &i);
 		// Abort if the queue send errors.
 		Debug::Invariant(ret == 0, "Queue send failed {}", ret);
 	}
diff --git a/examples/10.audit/README.md b/examples/10.audit/README.md
new file mode 100644
index 0000000..cd8d379
--- /dev/null
+++ b/examples/10.audit/README.md
@@ -0,0 +1,313 @@
+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`](https://github.com/CHERIoT-Platform/cheriot-audit).
+This tool applies [Rego](https://www.openpolicyagent.org/docs/latest/policy-language/) 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:
+
+```sh
+$ 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`](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`](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:
+
+```rego
+# 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:
+
+```rego
+[ 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:
+
+```json
+[
+  {
+    "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:
+
+```rego
+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:
+
+```rego
+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:
+
+```rego
+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:
+
+```rego
+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:
+
+```rego
+data.caesar.all_valid_caesar_capabilities
+```
+
+You should see something like this:
+
+```rego
+[
+  {
+    "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`](producer.cc) and [`consumer.cc`](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:
+
+```rego
+    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:
+
+```rego
+    # 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:
+
+```rego
+    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.
+
+```rego
+    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:
+
+```rego
+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:
+
+```rego
+    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
+
+```rego
+    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:
+
+```rego
+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.
diff --git a/examples/10.audit/caesar.rego b/examples/10.audit/caesar.rego
new file mode 100644
index 0000000..d310288
--- /dev/null
+++ b/examples/10.audit/caesar.rego
@@ -0,0 +1,77 @@
+package caesar
+
+# 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"
+}
+
+# Helpers for converting C integers to booleans.
+# These fail if the input is not either 1 or 0
+value_as_boolean(value) = output {
+	value = 1
+	output = true
+}
+
+value_as_boolean(value) = output {
+	value = 0
+	output = false
+}
+
+decode_caesar_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,
+	}
+}
+
+# Helper to extract all valid Caesar capabilities in the firmware image
+all_valid_caesar_capabilities = [{"owner": owner, "capability": decode_caesar_capability(c)} | c = input.compartments[owner].imports[_]; is_sealed_caesar_capability(c)]
+
+# Helper predicate to check that this is valid.
+valid {
+	# Make sure that the RTOS configuration is valid.
+	data.rtos.valid
+
+	# 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
+
+	# Extract the producer and consumer's capabilities
+	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
+
+	# Check permissions
+	producerCapability.permitEncrypt = true
+	producerCapability.permitDecrypt = false
+	consumerCapability.permitEncrypt = false
+	consumerCapability.permitDecrypt = true
+
+	# Make sure that the shift (encryption keys) are the same.
+	producerCapability.shift = consumerCapability.shift
+
+	# Make sure that only the producer and consumer compartments call the encrypt and decrypt functions
+	data.compartment.compartment_call_allow_list("caesar", "caesar_encrypt.*", {"producer"})
+	data.compartment.compartment_call_allow_list("caesar", "caesar_decrypt.*", {"consumer"})
+	# Make sure that only the entry compartment calls the produce and consume functions
+	data.compartment.compartment_call_allow_list("producer", "produce_message.*", {"entry"})
+	data.compartment.compartment_call_allow_list("consumer", "consume_message.*", {"entry"})
+}
diff --git a/examples/10.audit/caesar_cypher.cc b/examples/10.audit/caesar_cypher.cc
new file mode 100644
index 0000000..fd87dac
--- /dev/null
+++ b/examples/10.audit/caesar_cypher.cc
@@ -0,0 +1,72 @@
+#include "caesar_cypher.h"
+#include <compartment-macros.h>
+#include <debug.hh>
+#include <errno.h>
+
+using Debug = ConditionalDebug<true, "Caesar">;
+
+int caesar_encrypt(SObj        capability,
+                   const char *input,
+                   char       *output,
+                   size_t      length)
+{
+	auto *cypherState = token_unseal<CaesarCapability>(
+	  STATIC_SEALING_TYPE(CaesarCapabilityType), capability);
+	if (cypherState == nullptr)
+	{
+		return -EINVAL;
+	}
+	if (!cypherState->permitEncrypt)
+	{
+		return -EPERM;
+	}
+	for (int i = 0; i < length; i++)
+	{
+		uint8_t c = input[i];
+		// Replace control characters with 'X'
+		if ((c < 32) || (c >= 127))
+		{
+			c = 'X';
+		}
+		// Reset the base to 0.
+		c -= 32;
+		// Perform the encryption
+		c += cypherState->shift;
+		if (c > 94)
+		{
+			c -= 94;
+		}
+		c += 32;
+		output[i] = c;
+	}
+	return 0;
+}
+
+int caesar_decrypt(SObj        capability,
+                   const char *input,
+                   char       *output,
+                   size_t      length)
+{
+	auto *cypherState = token_unseal<CaesarCapability>(
+	  STATIC_SEALING_TYPE(CaesarCapabilityType), capability);
+	if (cypherState == nullptr)
+	{
+		return -EINVAL;
+	}
+	if (!cypherState->permitDecrypt)
+	{
+		return -EPERM;
+	}
+	for (int i = 0; i < length; i++)
+	{
+		int c = input[i];
+		// Perform the encryption
+		c -= cypherState->shift;
+		if (c < 32)
+		{
+			c += 94;
+		}
+		output[i] = c;
+	}
+	return 0;
+}
diff --git a/examples/10.audit/caesar_cypher.h b/examples/10.audit/caesar_cypher.h
new file mode 100644
index 0000000..1692c73
--- /dev/null
+++ b/examples/10.audit/caesar_cypher.h
@@ -0,0 +1,29 @@
+#include <token.h>
+
+struct CaesarCapability
+{
+	bool    permitEncrypt;
+	bool    permitDecrypt;
+	uint8_t shift;
+};
+
+#define DECLARE_AND_DEFINE_CAESAR_CAPABILITY(                                  \
+  name, permitEncrypt, permitDecrypt, shift)                                   \
+	DECLARE_AND_DEFINE_STATIC_SEALED_VALUE(struct CaesarCapability,            \
+	                                       caesar,                             \
+	                                       CaesarCapabilityType,               \
+	                                       name,                               \
+	                                       permitEncrypt,                      \
+	                                       permitDecrypt,                      \
+	                                       shift)
+
+int __cheri_compartment("caesar")
+  caesar_encrypt(SObj capability, const char *input, char *output, size_t len);
+
+int __cheri_compartment("caesar")
+  caesar_decrypt(SObj capability, const char *input, char *output, size_t len);
+
+ssize_t __cheri_compartment("producer")
+  produce_message(char *buffer, size_t length);
+void __cheri_compartment("consumer")
+  consume_message(const char *buffer, size_t length);
diff --git a/examples/10.audit/consumer.cc b/examples/10.audit/consumer.cc
new file mode 100644
index 0000000..29f8bb8
--- /dev/null
+++ b/examples/10.audit/consumer.cc
@@ -0,0 +1,19 @@
+// Copyright Microsoft and CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#include "caesar_cypher.h"
+#include <debug.hh>
+#include <errno.h>
+
+using Debug = ConditionalDebug<true, "Consumer">;
+
+DECLARE_AND_DEFINE_CAESAR_CAPABILITY(encrypt, false, true, 95);
+
+void consume_message(const char *buffer, size_t length)
+{
+	std::string decrypted;
+	decrypted.resize(length);
+	caesar_decrypt(
+	  STATIC_SEALED_VALUE(encrypt), buffer, decrypted.data(), length);
+	Debug::log("Decrypted message: '{}'", decrypted);
+}
diff --git a/examples/10.audit/entry.cc b/examples/10.audit/entry.cc
new file mode 100644
index 0000000..ae15563
--- /dev/null
+++ b/examples/10.audit/entry.cc
@@ -0,0 +1,24 @@
+// Copyright Microsoft and CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#include "caesar_cypher.h"
+#include <debug.hh>
+
+using Debug = ConditionalDebug<true, "Entry compartment">;
+
+char buffer[1024];
+
+/// Thread entry point.
+void __cheri_compartment("entry") entry()
+{
+	ssize_t length = produce_message(buffer, sizeof(buffer));
+	if (length < 0)
+	{
+		Debug::log("Failed to get encrypted message");
+		return;
+	}
+	Debug::log("Received encrypted message: '{}' ({} bytes)",
+	           std::string_view{buffer, static_cast<size_t>(length)},
+	           length);
+	consume_message(buffer, length);
+}
diff --git a/examples/10.audit/producer.cc b/examples/10.audit/producer.cc
new file mode 100644
index 0000000..fbafc45
--- /dev/null
+++ b/examples/10.audit/producer.cc
@@ -0,0 +1,27 @@
+// Copyright Microsoft and CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#include "caesar_cypher.h"
+#include <debug.hh>
+#include <errno.h>
+
+using Debug = ConditionalDebug<true, "Producer">;
+
+DECLARE_AND_DEFINE_CAESAR_CAPABILITY(encrypt, true, false, 95);
+
+ssize_t produce_message(char *buffer, size_t length)
+{
+	const std::string_view Plaintext = "Hello, World!";
+	if (length < Plaintext.size())
+	{
+		return -ENOMEM;
+	}
+	Debug::log("Encrypting message '{}'", Plaintext);
+	int ret = caesar_encrypt(
+	  STATIC_SEALED_VALUE(encrypt), Plaintext.data(), buffer, Plaintext.size());
+	if (ret < 0)
+	{
+		return ret;
+	}
+	return Plaintext.size();
+}
diff --git a/examples/10.audit/xmake.lua b/examples/10.audit/xmake.lua
new file mode 100644
index 0000000..71cb288
--- /dev/null
+++ b/examples/10.audit/xmake.lua
@@ -0,0 +1,42 @@
+-- Copyright Microsoft and CHERIoT Contributors.
+-- SPDX-License-Identifier: MIT
+
+set_project("CHERIoT Compartmentalised hello world (more secure)")
+sdkdir = "../../sdk"
+includes(sdkdir)
+set_toolchains("cheriot-clang")
+
+option("board")
+    set_default("sail")
+
+compartment("caesar")
+    -- This compartment uses C++ thread-safe static initialisation and so
+    -- depends on the C++ runtime.
+    add_files("caesar_cypher.cc")
+
+compartment("entry")
+    add_files("entry.cc")
+
+compartment("producer")
+    add_files("producer.cc")
+compartment("consumer")
+    add_files("consumer.cc")
+
+-- Firmware image for the example.
+firmware("caesar_example")
+    -- Both compartments require memcpy
+    add_deps("freestanding", "debug", "string")
+    add_deps("entry", "caesar")
+    add_deps("producer", "consumer")
+    on_load(function(target)
+        target:values_set("board", "$(board)")
+        target:values_set("threads", {
+            {
+                compartment = "entry",
+                priority = 1,
+                entry_point = "entry",
+                stack_size = 0x400,
+                trusted_stack_frames = 3
+            }
+        }, {expand = false})
+    end)
diff --git a/sdk/boards/sonata-0.2.json b/sdk/boards/sonata-0.2.json
index 6faa442..308904a 100644
--- a/sdk/boards/sonata-0.2.json
+++ b/sdk/boards/sonata-0.2.json
@@ -71,6 +71,7 @@
         "SUNBURST",
         "SUNBURST_SHADOW_BASE=0x30000000",
         "SUNBURST_SHADOW_SIZE=0x4000",
+        "DEFAULT_UART_BAUD_RATE=115200",
         "ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM=1",
         "ipconfigDRIVER_INCLUDED_TX_IP_CHECKSUM=1"
     ],
diff --git a/sdk/compartment.ldscript b/sdk/compartment.ldscript
index ba46ec4..9a602da 100644
--- a/sdk/compartment.ldscript
+++ b/sdk/compartment.ldscript
@@ -36,7 +36,7 @@
 		# If there is a compartment error handler, make sure that it is before
 		# anything that can have linker relaxations so that its displacement
 		# from __compartment_code_start is a constant.
-		*(.compartment_error_handler_stackless));
+		*(.compartment_error_handler_stackless);
 		*(.compartment_error_handler);
 		*(.text .text.*);
 	}
diff --git a/sdk/core/allocator/alloc.h b/sdk/core/allocator/alloc.h
index 1e890ea..8ab0c09 100644
--- a/sdk/core/allocator/alloc.h
+++ b/sdk/core/allocator/alloc.h
@@ -746,7 +746,9 @@
 	TChunk *leftmost_child()
 	{
 		if (child[0] != nullptr)
+		{
 			return child[0];
+		}
 		return child[1];
 	}
 
diff --git a/sdk/core/allocator/main.cc b/sdk/core/allocator/main.cc
index 8568af9..b5336ce 100644
--- a/sdk/core/allocator/main.cc
+++ b/sdk/core/allocator/main.cc
@@ -17,6 +17,17 @@
 #include <token.h>
 #include <utils.hh>
 
+/**
+ * The sealing key for dynamically allocated software-sealed objects.
+ */
+__attribute__((section(".sealing_key1"))) void *allocatorSealingKey;
+
+/**
+ * The root for the software sealing key.
+ */
+__attribute__((section(".sealing_key2"))) Capability<SKeyStruct>
+  softwareSealingKey;
+
 using namespace CHERI;
 
 Revocation::Revoker revoker;
@@ -1021,19 +1032,6 @@
 	uint32_t nextSealingType = std::numeric_limits<uint32_t>::max();
 
 	/**
-	 * Returns the root for the software sealing key.
-	 */
-	__always_inline Capability<SKeyStruct> software_sealing_key()
-	{
-		SKeyStruct *ret;
-		__asm("1:   "
-		      " auipcc      %0, %%cheriot_compartment_hi(__sealingkey2)\n"
-		      " clc         %0, %%cheriot_compartment_lo_i(1b)(%0)\n"
-		      : "=C"(ret));
-		return {ret};
-	}
-
-	/**
 	 * Helper that unseals `in` if it is a valid sealed capability sealed with
 	 * our hardware sealing key.  Returns the unsealed pointer, `nullptr` if it
 	 * cannot be helped.
@@ -1044,8 +1042,7 @@
 		// FIXME: At the moment the ISA is still shuffling types around, but
 		// eventually we want to know the type statically and don't need dynamic
 		// instructions.
-		Capability key{SEALING_CAP()};
-		in.unseal(key);
+		in.unseal(allocatorSealingKey);
 		return in.is_valid() ? in : SealedAllocation{nullptr};
 	}
 
@@ -1126,7 +1123,7 @@
 
 		obj->type   = key.address();
 		auto sealed = obj;
-		sealed.seal(SEALING_CAP());
+		sealed.seal(allocatorSealingKey);
 		obj.address() += ObjHdrSize; // Exclude the header.
 		obj.bounds() = obj.top() - obj.address();
 		Debug::Assert(
@@ -1141,7 +1138,7 @@
 	// structures and so can have its own lock.
 	static FlagLock tokenLock;
 	LockGuard       g{tokenLock};
-	auto            keyRoot = software_sealing_key();
+	auto            keyRoot = softwareSealingKey;
 	// For now, strip the user permissions.  We might want to use them for
 	// permit-allocate and permit-free.
 	keyRoot.permissions() &=
diff --git a/sdk/core/allocator/token.h b/sdk/core/allocator/token.h
index e9ce8f7..42c7343 100644
--- a/sdk/core/allocator/token.h
+++ b/sdk/core/allocator/token.h
@@ -92,3 +92,5 @@
 
 EXPORT_ASSEMBLY_OFFSET(TokenSObj, type, 0);
 EXPORT_ASSEMBLY_OFFSET(TokenSObj, data, 8);
+EXPORT_ASSEMBLY_NAME(CheriSealTypeAllocator, 11);
+EXPORT_ASSEMBLY_NAME(CheriSealTypeStaticToken, 12);
diff --git a/sdk/core/loader/boot.cc b/sdk/core/loader/boot.cc
index a72541f..e41038a 100644
--- a/sdk/core/loader/boot.cc
+++ b/sdk/core/loader/boot.cc
@@ -16,6 +16,7 @@
 #include "defines.h"
 #include "types.h"
 #include <cheri.hh>
+#include <compartment.h>
 #include <platform-uart.hh>
 #include <priv/riscv.h>
 #include <riscvreg.h>
@@ -49,6 +50,11 @@
 	// It must also be aligned sufficiently for trusted stacks, so ensure that
 	// we've captured that requirement above.
 	static_assert(alignof(TrustedStack) <= 16);
+
+	static_assert(sizeof(ErrorState) == offsetof(TrustedStack, hazardPointers));
+	static_assert(offsetof(ErrorState, pcc) == offsetof(TrustedStack, mepcc));
+	static_assert(offsetof(ErrorState, registers) ==
+	              offsetof(TrustedStack, cra));
 	__END_DECLS
 
 	static_assert(
@@ -62,12 +68,12 @@
 		/**
 		 * 0 represents unsealed.
 		 */
-		Unsealed = 0,
+		Unsealed = CheriSealTypeUnsealed,
 
 		/**
 		 * Sentry that inherits interrupt status.
 		 */
-		SentryInheriting,
+		SentryInheriting = CheriSealTypeSentryInheriting,
 
 		/// Alternative name: the default sentry type.
 		Sentry = SentryInheriting,
@@ -75,22 +81,32 @@
 		/**
 		 * Sentry that disables interrupts on calls.
 		 */
-		SentryDisabling,
+		SentryDisabling = CheriSealTypeSentryDisabling,
 
 		/**
 		 * Sentry that enables interrupts on calls.
 		 */
-		SentryEnabling,
+		SentryEnabling = CheriSealTypeSentryEnabling,
+
+		/**
+		 * Return sentry that disables interrupts on return
+		 */
+		ReturnSentryDisabling = CheriSealTypeReturnSentryDisabling,
+
+		/**
+		 * Return sentry that enables interrupts on return
+		 */
+		ReturnSentryEnabling = CheriSealTypeReturnSentryEnabling,
 
 		/**
 		 * Marker for the first sealing type that's valid for data capabilities.
 		 */
-		FirstDataSealingType = 9,
+		FirstDataSealingType = CheriSealTypeFirstDataSealingType,
 
 		/**
 		 * The sealing type used for sealed export table entries.
 		 */
-		SealedImportTableEntries = FirstDataSealingType,
+		SealedImportTableEntries = CheriSealTypeSealedImportTableEntries,
 
 		/**
 		 * The compartment switcher has a sealing type for the trusted stack.
@@ -98,38 +114,74 @@
 		 * This must be the second data sealing type so that we can also permit
 		 * the switcher to unseal sentries and export table entries.
 		 */
-		SealedTrustedStacks,
+		SealedTrustedStacks = CheriSealTypeSealedTrustedStacks,
 
 		/**
-		 * The scheduler has a sealing type for waitable objects.
+		 * The allocator has a sealing type for the software sealing mechanism
+		 * with dynamically allocated objects.
 		 */
-		Scheduler,
+		Allocator = CheriSealTypeAllocator,
 
 		/**
-		 * The allocator has a sealing type for the software sealing mechanism.
+		 * The loader reserves a sealing type for the software sealing
+		 * mechanism.  The permit-unseal capability for this is destroyed after
+		 * the loader has run, which guarantees that anything sealed with this
+		 * type was present in the original firmware image.  The token library
+		 * has the only permit-unseal capability for this type.
 		 */
-		Allocator,
+		StaticToken = CheriSealTypeStaticToken,
 
 		/**
 		 * The first sealing key that is reserved for use by the allocator's
 		 * software sealing mechanism and used for static sealing types,
 		 */
-		FirstStaticSoftware = 16,
+		FirstStaticSoftware = CheriSealTypeFirstStaticSoftware,
 
 		/**
 		 * The first sealing key in the space that the allocator will
 		 * dynamically allocate for sealing types.
 		 */
-		FirstDynamicSoftware = 0x1000000,
+		FirstDynamicSoftware = CheriSealTypeFirstDynamicSoftware,
 	};
 
+	// The switcher assembly includes the types of import table entries and
+	// trusted stacks.  This enumeration and the assembly must be kept in sync.
+	// This will fail if the enumeration value changes.
+	static_assert(int(SealedImportTableEntries) == 9,
+	              "If this fails, update switcher/entry.S to the new value");
+	static_assert(int(SealedTrustedStacks) == 10,
+	              "If this fails, update switcher/entry.S to the new value");
+
+	// The allocator and static sealing types must be contiguous so that the
+	// token library can hold a permit-unseal capability for both.
+	static_assert(int(Allocator) + 1 == int(StaticToken),
+	              "Allocator and StaticToken must be consecutive");
+
+	// The token library includes the types for allocator and statically sealed
+	// objects.  This enumeration and the assembly must be kept in sync.  This
+	// will fail if the enumeration value changes.
+	static_assert(int(Allocator) == 11,
+	              "If this fails, update token_unseal.S to the new value");
+
 	// We currently have a 3-bit hardware otype, with different sealing spaces
 	// for code and data capabilities, giving the range 0-0xf reserved for
 	// hardware use. Assert that we're not using more than we need (two in the
 	// enum are outside of the hardware space).
-	static_assert(magic_enum::enum_count<SealingType>() <= 10,
+	static_assert(magic_enum::enum_count<SealingType>() <= 12,
 	              "Too many sealing types reserved for a 3-bit otype field");
 
+} // namespace
+
+/*
+ * Unusually late, include this where we have access to the above enum
+ * SealingType, but early enough that the constants defined herein are available
+ * to the rest of the code.
+ */
+#include "../switcher/misc-assembly.h"
+
+namespace
+{
+
 	constexpr auto StoreLPerm = Root::Permissions<Root::Type::RWStoreL>;
 	/// PCC permissions for the switcher.
 	constexpr auto SwitcherPccPermissions =
@@ -306,6 +358,23 @@
 		return ptr.seal(key);
 	}
 
+	template<InterruptStatus Status, typename T>
+	T *seal_return(Capability<T> ptr)
+	{
+		static_assert((Status == InterruptStatus::Enabled) ||
+		              (Status == InterruptStatus::Disabled));
+
+#pragma clang diagnostic push
+#pragma clang diagnostic ignored "-Wc99-designator"
+		constexpr SealingType Sentries[] = {
+		  [int(InterruptStatus::Enabled)]  = ReturnSentryEnabling,
+		  [int(InterruptStatus::Disabled)] = ReturnSentryDisabling};
+#pragma clang diagnostic pop
+		size_t otype = size_t{Sentries[int(Status)]};
+		void  *key   = build<void, Root::Type::Seal>(otype, 1);
+		return ptr.seal(key);
+	}
+
 	/**
 	 * Helper to determine whether an object, given by a start address and size,
 	 * is completely contained within a specified range.
@@ -582,12 +651,6 @@
 				        Root::Type::RWGlobal,
 				        PermissionSet{Permission::Load, Permission::Store}>(
 				    entry.address);
-				// Is the software sealing type owned by the scheduler?  If so,
-				// we're going to seal the object with the scheduler's sealing
-				// type, not the allocator's.  This lets the scheduler export
-				// software-defined capabilities without adding the allocator
-				// to the TCB for availability.
-				bool isSchedulerObject = false;
 				// TODO: This currently places a restriction that data memory
 				// can't be in the low 64 KiB of the address space.  That may be
 				// too restrictive. If we haven't visited this sealed object
@@ -613,11 +676,7 @@
                         return false;
 					};
 					bool found = findExport(image.allocator());
-					if (!found && findExport(image.scheduler()))
-					{
-						found             = true;
-						isSchedulerObject = true;
-					}
+					found |= findExport(image.scheduler());
 					for (auto &compartment : image.compartments())
 					{
 						if (found)
@@ -632,8 +691,8 @@
 				}
 				Capability sealedObject = build(entry.address, entry.size());
 				// Seal with the allocator's sealing key
-				sealedObject.seal(build<void, Root::Type::Seal>(
-				  isSchedulerObject ? Scheduler : Allocator, 1));
+				sealedObject.seal(
+				  build<void, Root::Type::Seal>(StaticToken, 1));
 				Debug::log("Static sealed object: {}", sealedObject);
 				return sealedObject;
 			}
@@ -784,6 +843,21 @@
 		// Space per thread for hazard pointers.
 		static constexpr size_t HazardPointerSpace =
 		  HazardPointersPerThread * sizeof(void *);
+
+		/*
+		 * Construct a return sentry with which to populate initial thread
+		 * register files, as if they had been entered by the switcher rather
+		 * than by fiat of initial construction.  The switcher will detect the
+		 * trusted stack underflow and will signal the scheduler that the thread
+		 * has exited and should not be brought back on core.
+		 */
+		auto threadInitialReturn =
+		  build<void, Root::Type::Execute, SwitcherPccPermissions>(
+		    image.switcher.code);
+		threadInitialReturn.address() += image.switcher.crossCallReturnEntry;
+		threadInitialReturn =
+		  seal_return<InterruptStatus::Disabled>(threadInitialReturn);
+
 		for (size_t i = 0; const auto &config : image.threads())
 		{
 			Debug::log("Creating thread {}", i);
@@ -819,6 +893,7 @@
 			        false>(config.trustedStack);
 			threadTStack->mepcc = pcc;
 			threadTStack->cgp   = cgp;
+			threadTStack->cra   = threadInitialReturn;
 			// Stacks have store-local but not global permission.
 			auto stack =
 			  build<void,
@@ -1184,11 +1259,10 @@
 	trustedStackKey.bounds()  = 1;
 	switcherKey.address()     = SealedImportTableEntries;
 	switcherKey.bounds()      = 1;
-	setSealingKey(imgHdr.scheduler(), Scheduler);
 	setSealingKey(imgHdr.allocator(), Allocator);
 	setSealingKey(imgHdr.token_library(),
 	              Allocator,
-	              1,
+	              2, // Allocator and StaticToken
 	              0,
 	              PermissionSet{Permission::Global, Permission::Unseal});
 	constexpr size_t DynamicSealingLength =
diff --git a/sdk/core/loader/types.h b/sdk/core/loader/types.h
index ec488c9..7a29847 100644
--- a/sdk/core/loader/types.h
+++ b/sdk/core/loader/types.h
@@ -363,6 +363,12 @@
 			AddressRange code;
 
 			/**
+			 * The PCC-relative location of the cross-compartment call return
+			 * path, used to build the initial return addresses for threads.
+			 */
+			uint16_t crossCallReturnEntry;
+
+			/**
 			 * The PCC-relative location of the sealing key, which the
 			 * compartment switcher will use to unseal import table entries.
 			 */
@@ -447,7 +453,7 @@
 			 * The distance from the start of the code region to the end of the
 			 * import table.
 			 */
-			uint16_t importTableSize;
+			AddressRange importTable;
 
 			/**
 			 * The export table for the scheduler.
@@ -465,11 +471,7 @@
 			 */
 			[[nodiscard]] AddressRange import_table() const
 			{
-				// Skip the sealing keys
-				const size_t SealingKeysSize = 2 * sizeof(void *);
-				return {
-				  code.start() + SealingKeysSize,
-				  static_cast<uint16_t>(importTableSize - SealingKeysSize)};
+				return importTable;
 			}
 
 			/**
@@ -612,7 +614,7 @@
 			// This is a random 32-bit number and should be changed whenever
 			// the compartment header layout changes to provide some sanity
 			// checking.
-			return magic == 0x6cef3879;
+			return magic == 0xca2b63de;
 		}
 
 		/**
diff --git a/sdk/core/scheduler/common.h b/sdk/core/scheduler/common.h
index 565152d..ea9ccfd 100644
--- a/sdk/core/scheduler/common.h
+++ b/sdk/core/scheduler/common.h
@@ -8,6 +8,7 @@
 #include <cheri.hh>
 #include <debug.hh>
 #include <stdlib.h>
+#include <token.h>
 #include <type_traits>
 
 namespace
@@ -45,57 +46,14 @@
 	StackUsageCheck<StackMode, expected, __PRETTY_FUNCTION__> stackCheck
 
 	/**
-	 * Base class for types that are exported from the scheduler with a common
-	 * sealing type.  Includes an inline type marker.
+	 * Base class for sealed objects that are exported from the scheduler.
+	 *
+	 * Subclasses must implement a static `sealing_type` method that returns
+	 * the sealing key.
 	 */
+	template<bool IsDynamic>
 	struct Handle
 	{
-		protected:
-		/**
-		 * The real type of this subclass.
-		 *
-		 * This must be 32 bits and must be the first word of the class, so that
-		 * we are layout-compatible with the static sealing capabilities.  We
-		 * use low-value numbers for things that we dynamically allocate to
-		 * check types.  Anything that is statically allocated will have this
-		 * field initialised by the loader.
-		 *
-		 * Note that allocator-allocated and static types have a word of
-		 * padding here.  This is necessary to ensure that the base of the sub
-		 * object is capability-aligned.  In cases created with subclassing,
-		 * this is not required - the compiler will insert padding if it needs
-		 * to, but we can also put small fields in this space.  For anything
-		 * statically allocated, we will need to handle this separately.
-		 */
-		enum class Type : uint32_t
-		{
-			Invalid = 0,
-
-			/**
-			 * Multiwaiter type.
-			 */
-			MultiWaiter,
-
-			/**
-			 * Used only as the type marker, not for comparisons.  This
-			 * indicates that the type uses a dynamically allocated type value
-			 * that is provided in the `dynamic_type_marker()` static function.
-			 */
-			Dynamic,
-		} type;
-
-		/**
-		 * Constructor, takes the type of the subclass.
-		 */
-		Handle(Type type) : type(type) {}
-		~Handle()
-		{
-			__clang_ignored_warning_push("-Watomic-alignment") __atomic_store_n(
-			  reinterpret_cast<uint8_t *>(&type), 0, __ATOMIC_RELAXED);
-			__clang_ignored_warning_pop()
-		}
-
-		public:
 		/**
 		 * Unseal `unsafePointer` as a pointer to an object of the specified
 		 * type.  Returns nullptr if `unsafePointer` is not a valid sealed
@@ -106,6 +64,7 @@
 		{
 			return static_cast<Handle *>(unsafePointer)->unseal_as<T>();
 		}
+
 		/**
 		 * Unseal this object as the specified type.  Returns nullptr if this
 		 * is not a valid sealed object of the correct type.
@@ -116,25 +75,18 @@
 			static_assert(std::is_base_of_v<Handle, T>,
 			              "Cannot down-cast something that is not a subclass "
 			              "of Handle");
-			static_assert(offsetof(T, type) == 0,
-			              "Type field must be at the start of the object");
-			auto unsealed = compart_unseal(this);
-			if constexpr (T::TypeMarker == Type::Dynamic)
+			void *result;
+			if constexpr (IsDynamic)
 			{
-				if (unsealed.is_valid() && uint32_t(unsealed->type) ==
-				                             T::dynamic_type_marker().address())
-				{
-					return unsealed.cast<T>();
-				}
+				result = token_obj_unseal_dynamic(T::sealing_type(),
+				                                  reinterpret_cast<SObj>(this));
 			}
 			else
 			{
-				if (unsealed.is_valid() && unsealed->type == T::TypeMarker)
-				{
-					return unsealed.cast<T>();
-				}
+				result = token_obj_unseal_static(T::sealing_type(),
+				                                 reinterpret_cast<SObj>(this));
 			}
-			return nullptr;
+			return static_cast<T *>(result);
 		}
 	};
 
@@ -191,151 +143,4 @@
 	void exception_entry_asm(void);
 	__END_DECLS
 
-	/**
-	 * Wrapper around `std::unique_ptr` for objects allocated with a specific
-	 * heap capability.  The scheduler is not authorised to allocate memory
-	 * except on behalf of callers.
-	 */
-	template<typename T>
-	class HeapObject
-	{
-		/**
-		 * Deleter for use with `std::unique_ptr`, for memory allocated with an
-		 * explicit capability.
-		 */
-		class Deleter
-		{
-			/**
-			 * The capability that should authorise access to the heap.
-			 */
-			struct SObjStruct *heapCapability;
-
-			public:
-			/**
-			 * Constructor, captures the capability to use for deallocation.
-			 */
-			__always_inline Deleter(struct SObjStruct *heapCapability)
-			  : heapCapability(heapCapability)
-			{
-			}
-
-			/**
-			 * Apply function, calls the destructor and cleans up the underlying
-			 * memory.
-			 */
-			__always_inline void operator()(T *object)
-			{
-				object->~T();
-				heap_free(heapCapability, object);
-			}
-		};
-
-		protected:
-		/**
-		 * The underlying unique pointer.
-		 */
-		std::unique_ptr<T, Deleter> pointer = {nullptr, nullptr};
-
-		public:
-		/// Default constructor, creates a null object.
-		HeapObject() = default;
-		/**
-		 * Constructor for use with externally heap-allocated objects and
-		 * placement new.  Takes ownership of `allocatedObject`. The heap
-		 * capability will be used to free the object on destruction.
-		 */
-		HeapObject(struct SObjStruct *heapCapability, T *allocatedObject)
-		  : pointer(allocatedObject, heapCapability)
-		{
-			if (!__builtin_cheri_tag_get(allocatedObject))
-			{
-				pointer = nullptr;
-			}
-		}
-
-		/**
-		 * Attempt to allocate memory for, and construct, an instance of `T`
-		 * with the specified arguments.  If memory allocation fails, this will
-		 * construct an object wrapping a null pointer and not call the
-		 * constructor.  The bool-conversion operator can be used to check for
-		 * success.
-		 */
-		template<typename... Args>
-		HeapObject(Timeout           *timeout,
-		           struct SObjStruct *heapCapability,
-		           Args... args)
-		  : pointer(static_cast<T *>(
-		              heap_allocate(timeout, heapCapability, sizeof(T))),
-		            {heapCapability})
-		{
-			if (__builtin_cheri_tag_get(pointer.raw()))
-			{
-				new (pointer.get()) T(std::forward<Args>(args)...);
-			}
-			else
-			{
-				pointer = nullptr;
-			}
-		}
-
-		/**
-		 * Convert to bool.  Returns true if the unique pointer owns a non-null
-		 * pointer.
-		 */
-		operator bool()
-		{
-			return !!pointer;
-		}
-
-		/**
-		 * Returns the wrapped pointer without transferring ownership.
-		 */
-		T *get()
-		{
-			return pointer.get();
-		}
-
-		/**
-		 * Returns the wrapped pointer, transferring ownership to the caller.
-		 */
-		T *release()
-		{
-			return pointer.release();
-		}
-	};
-
-	/**
-	 * Wrapper for a buffer of a dynamic length, allocated on the heap owned by
-	 * another compartment.
-	 */
-	struct HeapBuffer : public HeapObject<char>
-	{
-		HeapBuffer() = default;
-
-		/**
-		 * Construct an array of `count` elemets, each of which is `size` bytes
-		 * long, using `heapCapability` to authorise allocation.
-		 */
-		HeapBuffer(Timeout           *timeout,
-		           struct SObjStruct *heapCapability,
-		           size_t             size,
-		           size_t             count)
-		  : HeapObject(
-		      heapCapability,
-		      static_cast<char *>(
-		        heap_allocate_array(timeout, heapCapability, size, count)))
-		{
-		}
-
-		/**
-		 * Update the address of the wrapped pointer.
-		 */
-		void set_address(ptraddr_t address)
-		{
-			CHERI::Capability old{pointer.release()};
-			old.address() = address;
-			pointer.reset(old);
-		}
-	};
-
 } // namespace
diff --git a/sdk/core/scheduler/main.cc b/sdk/core/scheduler/main.cc
index 18c0d7b..678c784 100644
--- a/sdk/core/scheduler/main.cc
+++ b/sdk/core/scheduler/main.cc
@@ -247,7 +247,9 @@
 		simulation_exit(1);
 
 		for (;;)
+		{
 			wfi();
+		}
 	}
 
 	[[cheri::interrupt_state(disabled)]] TrustedStack *
@@ -256,6 +258,15 @@
 	                                               size_t        mepc,
 	                                               size_t        mtval)
 	{
+		if constexpr (DebugScheduler)
+		{
+			/* Ensure that we got here from an IRQ-s deferred context */
+			Capability returnAddress{__builtin_return_address(0)};
+			Debug::Assert(
+			  returnAddress.type() == CheriSealTypeReturnSentryDisabling,
+			  "Scheduler exception_entry called from IRQ-enabled context");
+		}
+
 		// The cycle count value the last time the scheduler returned.
 		bool schedNeeded;
 		if constexpr (Accounting)
@@ -348,7 +359,7 @@
 	template<typename T>
 	int typed_op(void *sealed, auto &&fn)
 	{
-		auto *unsealed = Handle::unseal<T>(sealed);
+		auto *unsealed = T::template unseal<T>(sealed);
 		// If we can't unseal the sealed capability and have it be of the
 		// correct type then return an error.
 		if (!unsealed)
@@ -396,29 +407,6 @@
 		});
 	}
 
-	/**
-	 * Return path from `*_create` functions.  Performs a return check with
-	 * interrupts disabled and stores the object managed by `object` via `ret`
-	 * (consuming ownership) if `ret` has valid permissions.  Returns the value
-	 * that the caller should return to the public API.
-	 *
-	 * This function runs with interrupts disabled so that the majority of
-	 * `*_create` can have them enabled.
-	 */
-	template<typename T>
-	[[cheri::interrupt_state(disabled)]] int write_result(void         **ret,
-	                                                      HeapObject<T> &object)
-	{
-		if (!check_pointer<PermissionSet{Permission::Store,
-		                                 Permission::LoadStoreCapability}>(ret))
-		{
-			return -EINVAL;
-		}
-
-		*ret = compart_seal(object.release());
-		return 0;
-	}
-
 } // namespace sched
 
 using namespace sched;
@@ -594,7 +582,12 @@
 		return error;
 	}
 
-	return write_result(reinterpret_cast<void **>(ret), mw);
+	// This can trap, but only if the caller has provided a bad pointer.
+	// In this case, the caller can leak memory, but only memory allocated
+	// against its own quota.
+	*reinterpret_cast<void **>(ret) = mw;
+
+	return 0;
 }
 
 __cheriot_minimum_stack(0x70) int multiwaiter_delete(
@@ -668,30 +661,19 @@
 namespace
 {
 	/**
-	 *
+	 * An interrupt capability.
 	 */
-	struct InterruptCapability : Handle
+	struct InterruptCapability : Handle</*IsDynamic=*/false>
 	{
 		/**
-		 * Type marker used by `Handle`, tells it to use the dynamic path.
+		 * Sealing type used by `Handle`.
 		 */
-		static constexpr auto TypeMarker = Handle::Type::Dynamic;
-
-		/**
-		 * Dynamic type marker used by `Handle`.
-		 */
-		static Capability<void> dynamic_type_marker()
+		static SKey sealing_type()
 		{
 			return STATIC_SEALING_TYPE(InterruptKey);
 		}
 
 		/**
-		 * Padding for compatibility with the token layout.  This can go away
-		 * at some point.
-		 */
-		uint32_t padding;
-
-		/**
 		 * The public structure state.
 		 */
 		InterruptCapabilityState state;
@@ -702,8 +684,9 @@
   0x30) const uint32_t *interrupt_futex_get(struct SObjStruct *sealed)
 {
 	STACK_CHECK(0x30);
-	auto     *interruptCapability = Handle::unseal<InterruptCapability>(sealed);
-	uint32_t *result              = nullptr;
+	auto *interruptCapability =
+	  InterruptCapability::unseal<InterruptCapability>(sealed);
+	uint32_t *result = nullptr;
 	if (interruptCapability && interruptCapability->state.mayWait)
 	{
 		InterruptController::master()
@@ -722,7 +705,8 @@
   0x20) int interrupt_complete(struct SObjStruct *sealed)
 {
 	STACK_CHECK(0x20);
-	auto *interruptCapability = Handle::unseal<InterruptCapability>(sealed);
+	auto *interruptCapability =
+	  InterruptCapability::unseal<InterruptCapability>(sealed);
 	if (interruptCapability && interruptCapability->state.mayComplete)
 	{
 		InterruptController::master().interrupt_complete(
diff --git a/sdk/core/scheduler/multiwait.h b/sdk/core/scheduler/multiwait.h
index 23710dc..e1fdb5f 100644
--- a/sdk/core/scheduler/multiwait.h
+++ b/sdk/core/scheduler/multiwait.h
@@ -101,13 +101,16 @@
 	/**
 	 * Multiwaiter object.  This contains space for all of the triggers.
 	 */
-	class MultiWaiterInternal : public Handle
+	class MultiWaiterInternal : public Handle</*IsDynamic*/ true>
 	{
 		public:
 		/**
-		 * Type marker used for `Handle::unseal_as`.
+		 * Sealing type used by `Handle`.
 		 */
-		static constexpr auto TypeMarker = Handle::Type::MultiWaiter;
+		static SKey sealing_type()
+		{
+			return STATIC_SEALING_TYPE(MultiWaiterKey);
+		}
 
 		private:
 		/**
@@ -176,12 +179,13 @@
 		 * Factory method.  Creates a multiwaiter of the specified size.  On
 		 * failure, sets `error` to the errno constant corresponding to the
 		 * failure reason and return `nullptr`.
+		 *
+		 * The result is a *sealed* multiwaiter handle.
 		 */
-		static HeapObject<MultiWaiterInternal>
-		create(Timeout           *timeout,
-		       struct SObjStruct *heapCapability,
-		       size_t             length,
-		       int               &error)
+		static SObj create(Timeout           *timeout,
+		                   struct SObjStruct *heapCapability,
+		                   size_t             length,
+		                   int               &error)
 		{
 			static_assert(sizeof(MultiWaiterInternal) <= 2 * sizeof(void *),
 			              "Header for event queue is too large");
@@ -190,17 +194,21 @@
 				error = -EINVAL;
 				return {};
 			}
-			void *q = heap_allocate(timeout,
-			                        heapCapability,
-			                        sizeof(MultiWaiterInternal) +
-			                          (length * sizeof(EventWaiter)));
-			if (!__builtin_cheri_tag_get(q))
+			void *memory = nullptr;
+			SObj  sealed = token_sealed_unsealed_alloc(
+			   timeout,
+			   heapCapability,
+			   sealing_type(),
+			   sizeof(MultiWaiterInternal) + (length * sizeof(EventWaiter)),
+			   &memory);
+			if (!memory)
 			{
 				error = -ENOMEM;
-				return {};
+				return nullptr;
 			}
+			new (memory) MultiWaiterInternal(length);
 			error = 0;
-			return {heapCapability, new (q) MultiWaiterInternal(length)};
+			return sealed;
 		}
 
 		/**
@@ -369,9 +377,7 @@
 		/**
 		 * Private constructor, called only from the factory method (`create`).
 		 */
-		MultiWaiterInternal(size_t length) : Handle(TypeMarker), Length(length)
-		{
-		}
+		MultiWaiterInternal(size_t length) : Length(length) {}
 
 		/**
 		 * Priority-sorted wait queue for threads that are blocked on a
diff --git a/sdk/core/switcher/entry.S b/sdk/core/switcher/entry.S
index 8ef9cca..387a2d1 100644
--- a/sdk/core/switcher/entry.S
+++ b/sdk/core/switcher/entry.S
@@ -3,6 +3,7 @@
 
 #include "export-table-assembly.h"
 #include "trusted-stack-assembly.h"
+#include "misc-assembly.h"
 #include <errno.h>
 
 .include "assembly-helpers.s"
@@ -27,6 +28,25 @@
 #define SPILL_SLOT_pcc 24
 #define SPILL_SLOT_SIZE 32
 
+/*
+ * The switcher uniformly speaks of registers using their RISC-V ELF psABI names
+ * and not their raw index, as, broadly speaking, we use registers in a similar
+ * way to C functions.  However, it's probably convenient to have a mapping
+ * readily accessible, so here 'tis:
+ *
+ *  #     x0   x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
+ *  psABI zero ra sp gp tp t0 t1 t2 s0 s1 a0  a1  a2  a3  a4  a5
+ *
+ * When we use the psABI name without a 'c' prefix, we are sometimes meaning to
+ * refer to the address component of the capability.
+ *
+ * Despite the use of psABI names and conformance at the interface (argument
+ * registers used for arguments, return address register used for its canonical
+ * purpose, &c), one should not read too much of the psABI calling convention
+ * into the code here.  Within the switcher, the machine is a raw register
+ * machine and C is a distant, high-level language.
+ */
+
 switcher_code_start:
 
 # Global for the sealing key.  Stored in the switcher's code section.
@@ -164,11 +184,19 @@
 	.p2align 2
 	.type __Z26compartment_switcher_entryz,@function
 __Z26compartment_switcher_entryz:
-	cincoffset        csp, csp, -SPILL_SLOT_SIZE
-	csc               cs0, SPILL_SLOT_cs0(csp)
-	csc               cs1, SPILL_SLOT_cs1(csp)
-	csc               cgp, SPILL_SLOT_cgp(csp)
-	csc               cra, SPILL_SLOT_pcc(csp)
+	/*
+	 * Spill caller-save registers carefully.  If we find ourselves unable to do
+	 * so, we'll return an error to the caller (via the exception path; see
+	 * .Lhandle_error_in_switcher).  The error handling path assumes that the
+	 * first spill is to the lowest address and guaranteed to trap if any would.
+	 */
+	cincoffset        ct2, csp, -SPILL_SLOT_SIZE
+.Lswitcher_entry_first_spill:
+	csc               cs0, SPILL_SLOT_cs0(ct2)
+	csc               cs1, SPILL_SLOT_cs1(ct2)
+	csc               cgp, SPILL_SLOT_cgp(ct2)
+	csc               cra, SPILL_SLOT_pcc(ct2)
+	cmove             csp, ct2
 	// before we access any privileged state, we can verify the
 	// compartment's csp is valid. If not, force unwind.
 	// Note that this check is purely to protect the callee, not the switcher
@@ -207,7 +235,6 @@
 	// table entry on the trusted stack, a fault here will cause a forced
 	// unwind until we set the correct one.
 	csh                s1, TrustedStack_offset_frameoffset(ct2)
-#ifndef CONFIG_NO_SWITCHER_SAFETY
 	// Chop off the stack.
 	cgetaddr           s0, csp
 	cgetbase           s1, csp
@@ -219,25 +246,18 @@
 	// Read the stack high water mark (which is 16-byte aligned)
 	csrr               gp, CSR_MSHWM
 	// Skip zeroing if high water mark >= stack pointer
-	bge                t2, sp, after_zero
+	bge                gp, sp, .Lafter_zero
 	// Use stack high water mark as base address for zeroing.  If this faults
 	// then it will trigger a force unwind.  This can happen only if the caller
 	// is doing something bad.
 	csetaddr           ct2, csp, gp
 #endif
 	zero_stack         t2, s0, gp
-after_zero:
-	// Reserve space for unwind state and so on.
-	cincoffset 	       csp, csp, -STACK_ENTRY_RESERVED_SPACE
-#ifdef CONFIG_MSHWM
-	// store new stack top as stack high water mark
-	csrw               CSR_MSHWM, sp
-#endif
-#endif // CONFIG_NO_SWITCHER_SAFETY
-.Lout:
+.Lafter_zero:
+
 	// Fetch the sealing key
 	LoadCapPCC         cs0, compartment_switcher_sealing_key
-	li                 gp, 9
+	li                 gp, SEAL_TYPE_SealedImportTableEntries
 	csetaddr           cs0, cs0, gp
 	// The target capability is in ct1. Unseal, check tag and load the entry point offset.
 	cunseal            ct1, ct1, cs0
@@ -258,10 +278,25 @@
 	// At this point, we have already truncated the stack and so the length of
 	// the stack is the length that the callee can use.
 	cgetlen            t2, csp
-	// Include the space we reserved for the unwind state.
-	addi               t2, t2, -STACK_ENTRY_RESERVED_SPACE
+	/*
+	 * Include the space we reserved for the unwind state.
+	 *
+	 * tp holds the number of required stack bytes, a value between 0 and 0x7F8
+	 * (the result of an unsigned byte load left shifted by 3).  Given this
+	 * extremely limited range, adding STACK_ENTRY_RESERVED_SPACE will not cause
+	 * overflow (while instead subtracting it from the available length, in t2,
+	 * might underflow).
+	 */
+	addi               tp, tp, STACK_ENTRY_RESERVED_SPACE
 	bgtu               tp, t2, .Lstack_too_small
 
+	// Reserve space for unwind state and so on.
+	cincoffset 	       csp, csp, -STACK_ENTRY_RESERVED_SPACE
+#ifdef CONFIG_MSHWM
+	// store new stack top as stack high water mark
+	csrw               CSR_MSHWM, sp
+#endif
+
 	// Get the flags field into tp
 	clbu               tp, ExportEntry_offset_flags(ct1)
 	cgetbase           s1, ct1
@@ -298,19 +333,75 @@
 	csrsi              mstatus, 0x8
 .Lskip_interrupt_disable:
 	// Registers passed to the callee are:
-	// c1 (ra), c2 (csp), and c3 (cgp) are passed unconditionally.
+	// cra (c1), csp (c2), and cgp (c3) are passed unconditionally.
 	// ca0-ca5 (c10-c15) and ct0 (c5) are either passed as arguments or cleared
 	// above.  This should add up to 10 registers, with the remaining 5 being
 	// cleared now:
 	zeroRegisters      tp, t1, t2, s0, s1
 	cjalr              cra
 
-.Lskip_compartment_call:
+	.globl switcher_skip_compartment_call
+switcher_skip_compartment_call:
 	// If we are doing a forced unwind of the trusted stack then we do almost
 	// exactly the same as a normal unwind.  We will jump here from the
-	// exception path.
-	cjal               .Lpop_trusted_stack_frame
-	cmove              cra, ca2
+	// exception path (.Lforce_unwind)
+
+	/*
+	 * Pop a frame from the trusted stack, leaving all registers in the state
+	 * expected by the caller of a cross-compartment call.  The callee is
+	 * responsible for zeroing argument and temporary registers.
+	 *
+	 * The below should not fault before returning back to the caller. If a
+	 * fault occurs there must be a serious bug elsewhere.
+	 */
+
+	cspecialr          ctp, mtdc
+	clear_hazard_slots ctp, ct2
+	// make sure there is a frame left in the trusted stack
+	clhu               t2, TrustedStack_offset_frameoffset(ctp)
+	li                 tp, TrustedStack_offset_frames
+	// Move to the previous trusted stack frame.
+	addi               t2, t2, -TrustedStackFrame_size
+	// If this is the first trusted stack frame, then the csp that we would be
+	// loading is the csp on entry, which does not have a spilled area.  In
+	// this case, we would fault when loading, so would exit the thread, but we
+	// should instead gracefully exit the thread.
+	bgeu               tp, t2, .Lcommon_defer_irqs_and_thread_exit
+	cspecialr          ctp, mtdc
+	cincoffset         ct1, ctp, t2
+	// Restore the stack pointer.  All other spilled values are spilled there.
+	clc                csp, TrustedStackFrame_offset_csp(ct1)
+	// Update the current frame offset.
+	csh                t2, TrustedStack_offset_frameoffset(ctp)
+	// Do the loads *after* moving the trusted stack pointer.  In theory, the
+	// checks in `check_compartment_stack_integrity` make it impossible for
+	// this to fault, but if we do fault here then we'd end up in an infinite
+	// loop trying repeatedly to pop the same trusted stack frame.  This would
+	// be bad.  Instead, we move the trusted stack pointer *first* and so, if
+	// the accesses to the untrusted stack fault, we will detect a fault in the
+	// switcher, enter the force-unwind path, and pop the frame for the
+	// compartment that gave us a malicious csp.
+	clc                cs0, SPILL_SLOT_cs0(csp)
+	clc                cs1, SPILL_SLOT_cs1(csp)
+	clc                cra, SPILL_SLOT_pcc(csp)
+	clc                cgp, SPILL_SLOT_cgp(csp)
+	cincoffset         csp, csp, SPILL_SLOT_SIZE
+#ifdef CONFIG_MSHWM
+	// read the stack high water mark, which is 16-byte aligned
+	// we will use this as base address for stack clearing
+	// note that it cannot be greater than stack top as we
+	// we set it to stack top when we pushed to trusted stack frame
+	csrr               tp, CSR_MSHWM
+#else
+	cgetbase           tp, csp
+#endif
+	cgetaddr           t1, csp
+	csetaddr           ct2, csp, tp
+	zero_stack         t2, t1, tp
+#ifdef CONFIG_MSHWM
+	csrw               CSR_MSHWM, sp
+#endif
+
 	// Zero all registers apart from RA, GP, SP and return args.
 	// cra, csp and cgp needed for the compartment
 	// cs0 saved and restored on trusted stack
@@ -318,6 +409,7 @@
 	// ca0, used for first return value
 	// ca1, used for second return value
 	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0, a1
+.Ljust_return:
 	cret
 
 	// If the stack is too small, we don't do the call, but to avoid leaking
@@ -327,7 +419,7 @@
 .Lstack_too_small:
 	li                 a0, -ENOTENOUGHSTACK
 	li                 a1, 0
-	j                  .Lskip_compartment_call
+	j                  switcher_skip_compartment_call
 .size compartment_switcher_entry, . - compartment_switcher_entry
 
 	// the entry point of all exceptions and interrupts
@@ -367,8 +459,8 @@
 
 	// csp now points to the save reg frame that we can use.
 	// The guest csp (c2) is now in mtdc. Will be spilled later, but we
-	// spill all other registers now.
-	spillRegisters     c1, cgp, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15
+	// spill all the other 14 registers now.
+	spillRegisters     cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5
 
 	// If a thread has exited then it will set a fake value in the mcause so
 	// that the scheduler knows not to try to resume it.
@@ -398,7 +490,7 @@
 	// If we hit one of the exception conditions that we should let
 	// compartments handle then deliver it to the compartment.
 	// CHERI exception code.
-	li                 a0, 0x1c
+	li                 a0, MCAUSE_CHERI
 	beq                a0, t1, .Lhandle_error
 	// Misaligned instruction, instruction access, illegal instruction,
 	// breakpoint, misaligned load, load fault, misaligned store, and store
@@ -443,7 +535,7 @@
 
 	// Switch onto the new thread's trusted stack
 	LoadCapPCC         ct0, compartment_switcher_sealing_key
-	li                 gp, 10
+	li                 gp, SEAL_TYPE_SealedTrustedStacks
 	csetaddr           ct0, ct0, gp
 	cunseal            csp, ca0, ct0
 	clw                t0, TrustedStack_offset_mcause(csp)
@@ -457,11 +549,11 @@
 	// mret, so reentrancy is no longer a concern.
 	cspecialw          mtdc, csp
 
-	// If mcause is 25, then we will jump into the error handler: another
-	// thread has signalled that this thread should be interrupted.  25 is a
-	// reserved exception number that we repurpose to indicate explicit
-	// interruption.
-	li                 t1, 25
+	// If mcause is MCAUSE_THREAD_INTERRUPT, then we will jump into the error
+	// handler: another thread has signalled that this thread should be
+	// interrupted.  MCAUSE_THREAD_INTERRUPT is a reserved exception number that
+	// we repurpose to indicate explicit interruption.
+	li                 t1, MCAUSE_THREAD_INTERRUPT
 	beq                t0, t1, .Lhandle_injected_error
 
 	// Environment call from M-mode is exception code 11.
@@ -476,36 +568,27 @@
 // ct2 to be the pcc to jump to.  All other registers are in unspecified states
 // and will be overwritten when we install the context.
 .Linstall_context:
-	clw                x1, TrustedStack_offset_mstatus(csp)
-	csrw               mstatus, x1
+	clw                ra, TrustedStack_offset_mstatus(csp)
+	csrw               mstatus, ra
 #ifdef CONFIG_MSHWM
-	clw                x1, TrustedStack_offset_mshwm(csp)
-	csrw               CSR_MSHWM, x1
-	clw                x1, TrustedStack_offset_mshwmb(csp)
-	csrw               CSR_MSHWMB, x1
+	clw                ra, TrustedStack_offset_mshwm(csp)
+	csrw               CSR_MSHWM, ra
+	clw                ra, TrustedStack_offset_mshwmb(csp)
+	csrw               CSR_MSHWMB, ra
 #endif
 	cspecialw          mepcc, ct2
-	// c2 is csp, which will be loaded last and will overwrite the trusted
-	// stack pointer with the thread's stack pointer.
-	reloadRegisters c1, cgp, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, csp
+	// csp (c2) will be loaded last and will overwrite the trusted stack pointer
+	// with the thread's stack pointer.
+	reloadRegisters cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5, csp
 	mret
 
 // We are starting a forced unwind.  This is reached either when we are unable
 // to run an error handler, or when we do run an error handler and it instructs
 // us to return.  This treats all register values as undefined on entry.
 .Lforce_unwind:
-	// Pop the trusted stack frame.
-	cjal               .Lpop_trusted_stack_frame
-	cmove              cra, ca2
-	// Zero all registers apart from RA, GP, SP and return args.
-	// cra, cs0, cs1, and cgp were restored from the compartment's stack
-	// csp restored from the trusted stack.
-	// ca0, used for first return value
-	// ca1, used for second return value
-	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0, a1
 	li                 a0, -ECOMPARTMENTFAIL
 	li                 a1, 0
-	cret
+	j                  switcher_skip_compartment_call
 
 
 // If we have run out of trusted stack, then just restore the caller's state
@@ -554,15 +637,15 @@
 	auipcc             ct0, 0
 	clc                ct1, TrustedStack_offset_mepcc(csp)
 	cgetbase           t0, ct0
-	cgetbase           t1, ct1
-	beq                t0, t1, .Lforce_unwind
+	cgetbase           tp, ct1
+	beq                t0, tp, .Lhandle_error_in_switcher
 
 	// Load the interrupted thread's stack pointer into ct0
 	clc                ct0, TrustedStack_offset_csp(csp)
 	// See if we can find a handler:
 	clhu               tp, TrustedStack_offset_frameoffset(csp)
 	li                 t1, TrustedStack_offset_frames
-	beq                tp, t1, .Lreset_mepcc_and_install_context
+	beq                tp, t1, .Lset_mcause_and_exit_thread
 	addi               tp, tp, -TrustedStackFrame_size
 
 	// ctp points to the current available trusted stack frame.
@@ -618,22 +701,22 @@
 	// Get the previous trusted stack frame
 
 	// Load the caller's csp
-	clc                ca0, TrustedStackFrame_offset_csp(ctp)
+	clc                ct0, TrustedStackFrame_offset_csp(ctp)
 
 	// If this is the top stack frame, then the csp field is the value on
 	// entry.  If it's any other frame then we need to go to the previous one
 	cincoffset         cs1, csp, TrustedStack_offset_frames
-	beq                s1, t1, .Lrecovered_stack
+	beq                s1, tp, .Lrecovered_stack
 
 	// The address of the stack pointer will point to the bottom of the
 	// caller's save area, so we set the bounds to be the base up to the
 	// current address.
-	cgetaddr           a1, ca0
-	cgetbase           a2, ca0
+	cgetaddr           a1, ct0
+	cgetbase           a2, ct0
 	sub                a1, a1, a2
-	csetaddr           ca0, ca0, a2
+	csetaddr           ct0, ct0, a2
 	// The code that installs the context expects csp to be in ct0
-	csetboundsexact    ct0, ca0, a1
+	csetboundsexact    ct0, ct0, a1
 .Lrecovered_stack:
 	li                 a0, 1
 
@@ -682,9 +765,9 @@
 	ccleartag          cs1, cs1
 	csc                cs1, 0(ct0)
 	// Source for context copy.
-	cincoffset         ca2, csp, TrustedStack_offset_c1
+	cincoffset         ca2, csp, TrustedStack_offset_cra
 	// Destination for context copy
-	cincoffset         ca3, ct0, TrustedStack_offset_c1
+	cincoffset         ca3, ct0, TrustedStack_offset_cra
 	copyContext        ca3, ca2, cs1, a4
 
 	// Set up the arguments for the call
@@ -694,6 +777,9 @@
 	cmove              csp, ca0
 
 .Linvoke_error_handler:
+	// Enable interrupts before invoking the handler
+	csrsi              mstatus, 0x8
+
 	// Clear all registers except:
 	// cra is set by cjalr.  csp and cgp are needed for the called compartment.
 	// ca0, used for the register state
@@ -703,6 +789,15 @@
 	// Call the handler.
 	cjalr              cra
 
+	/*
+	 * Now that we're back, defer interrupts again before we do anything that
+	 * manipulates the TrustedStack.
+	 *
+	 * TODO: Eventually we'd like to move this down onto the paths where it
+	 * actually matters and let most of this code run with IRQs enabled.
+	 */
+	csrci              mstatus, 0x8
+
 	// Move the return value to a register that will be cleared in a forced
 	// unwind and zero the return registers.
 	move               s0, a0
@@ -747,9 +842,9 @@
 	csetaddr           ct2, ct0, ra
 	// Now copy everything else from the stack into the saved context
 	// Source
-	cincoffset         ca2, csp, TrustedStack_offset_c1
+	cincoffset         ca2, csp, TrustedStack_offset_cra
 	// Destination
-	cincoffset         ca3, ct1, TrustedStack_offset_c1
+	cincoffset         ca3, ct1, TrustedStack_offset_cra
 	copyContext        ca3, ca2, cs1, a4
 	// Increment the handler invocation count.  We have now returned and
 	// finished touching any data from the error handler that might cause a
@@ -766,84 +861,55 @@
 
 .Lhandle_injected_error:
 #ifdef CONFIG_MSHWM
-	clw                x1, TrustedStack_offset_mshwm(csp)
-	csrw               CSR_MSHWM, x1
-	clw                x1, TrustedStack_offset_mshwmb(csp)
-	csrw               CSR_MSHWMB, x1
+	clw                ra, TrustedStack_offset_mshwm(csp)
+	csrw               CSR_MSHWM, ra
+	clw                ra, TrustedStack_offset_mshwmb(csp)
+	csrw               CSR_MSHWMB, ra
 #endif
 	j                  .Lhandle_error
 
+.Lcommon_defer_irqs_and_thread_exit:
+	csrci               mstatus, 0x8
+	// Fall-through, now that IRQs are off
 
 	// Value 24 is reserved for custom use.
 .Lset_mcause_and_exit_thread:
-	csrw               mcause, 24
+	csrw               mcause, MCAUSE_THREAD_EXIT
+	// The thread exit code expects the trusted stack pointer to be in csp and
+	// the stack pointer to be in mtdc.  After thread exit, we don't need the
+	// stack pointer so just put zero there.
+	zeroOne            sp
+	cspecialrw         csp, mtdc, csp
 	j                  .Lthread_exit
 
-	// The continue-resume path expects the location that we will mret to to be
-	// in ct2.  If we're just resuming, then resume from the stashed link
-	// register value.
-.Lreset_mepcc_and_install_context:
-	clc                ct2, TrustedStack_offset_mepcc(csp)
+	/*
+	 * Some switcher instructions' traps are handled specially, by looking at
+	 * the offset of mepcc.  Otherwise, we're off to a force unwind.
+	 */
+.Lhandle_error_in_switcher:
+	auipcc             ctp, %cheriot_compartment_hi(.Lswitcher_entry_first_spill)
+	cincoffset         ctp, ctp, %cheriot_compartment_lo_i(.Lhandle_error_in_switcher)
+	bne                t1, tp, .Lforce_unwind
+	li                 a0, -ENOTENOUGHSTACK
+	li                 a1, 0
+
+	/*
+	 * Cause the interrupted thread to resume as if a return had just executed.
+	 * We do this by vectoring to a `cjalr ra` (`cret`) instruction through
+	 * `mepcc`; whee!  Overwrites the stored context a0 and a1 with the current
+	 * values of those registers, effectively passing them through
+	 * .Linstall_context.
+	 */
+.Linstall_return_context:
+	auipcc             ct2, %cheriot_compartment_hi(.Ljust_return)
+	cincoffset         ct2, ct2, %cheriot_compartment_lo_i(.Linstall_return_context)
+	csc                ca0, TrustedStack_offset_ca0(csp)
+	csc                ca1, TrustedStack_offset_ca1(csp)
 	j                  .Linstall_context
 
+
 .size exception_entry_asm, . - exception_entry_asm
 
-/**
- * Pops a frame from the trusted stack.  Leaves all registers in the state
- * expected by the caller of a cross-compartment call, except for the return
- * address which is left in ca2.  The callee is responsible for zeroing
- * argument and temporary registers.
- */
-.Lpop_trusted_stack_frame:
-	// The below should not fault before returning back to the caller. If a fault occurs there must
-	// be a serious bug elsewhere.
-	cspecialr          ctp, mtdc
-	clear_hazard_slots ctp, ct2
-	// make sure there is a frame left in the trusted stack
-	clhu               t2, TrustedStack_offset_frameoffset(ctp)
-	li                 tp, TrustedStack_offset_frames
-	bgeu               tp, t2, .Lset_mcause_and_exit_thread
-	cspecialr          ctp, mtdc
-	addi               t2, t2, -TrustedStackFrame_size
-	cincoffset         ct1, ctp, t2
-	// Restore the stack pointer.  All other spilled values are spilled there.
-	clc                csp, TrustedStackFrame_offset_csp(ct1)
-	// Update the current frame offset.
-	csh                t2, TrustedStack_offset_frameoffset(ctp)
-	// Do the loads *after* moving the trusted stack pointer.  In theory, the
-	// checks in `check_compartment_stack_integrity` make it impossible for
-	// this to fault, but if we do fault here then we'd end up in an infinite
-	// loop trying repeatedly to pop the same trusted stack frame.  This would
-	// be bad.  Instead, we move the trusted stack pointer *first* and so, if
-	// the accesses to the untrusted stack fault, we will detect a fault in the
-	// switcher, enter the force-unwind path, and pop the frame for the
-	// compartment that gave us a malicious csp.
-	clc                cs0, SPILL_SLOT_cs0(csp)
-	clc                cs1, SPILL_SLOT_cs1(csp)
-	clc                ca2, SPILL_SLOT_pcc(csp)
-	clc                cgp, SPILL_SLOT_cgp(csp)
-	cincoffset         csp, csp, SPILL_SLOT_SIZE
-#ifndef CONFIG_NO_SWITCHER_SAFETY
-#ifdef CONFIG_MSHWM
-	// read the stack high water mark, which is 16-byte aligned
-	// we will use this as base address for stack clearing
-	// note that it cannot be greater than stack top as we 
-	// we set it to stack top when we pushed to trusted stack frame
-	csrr               tp, CSR_MSHWM
-#else
-	cgetbase           tp, csp
-#endif
-	cgetaddr           t1, csp
-	csetaddr           ct2, csp, tp
-	zero_stack         t2, t1, tp
-#ifdef CONFIG_MSHWM
-	csrw               CSR_MSHWM, sp
-#endif
-#endif // CONFIG_NO_SWITCHER_SAFETY
-	cret
-
-
-
 /*******************************************************************************
  * Switcher-exported library functions.
  *
@@ -914,7 +980,7 @@
 	// Load the unsealing key into a register that we will clobber two
 	// instructions later.
 	LoadCapPCC         ca1, compartment_switcher_sealing_key
-	li                 a2, 10
+	li                 a2, SEAL_TYPE_SealedTrustedStacks
 	csetaddr           ca1, ca1, a2
 	// The target capability is in ct1. Unseal, check tag and load the entry point offset.
 	cunseal            ca1, ca0, ca1
@@ -960,7 +1026,7 @@
 
 	// Mark the thread as interrupted.
 	// Store a magic value in mcause
-	li                 a2, 25
+	li                 a2, MCAUSE_THREAD_INTERRUPT
 	csw                a2, TrustedStack_offset_mcause(ca1)
 	// Return success
 	li                 a0, 1
@@ -973,7 +1039,7 @@
 	.type __Z23switcher_current_threadv,@function
 __Z23switcher_current_threadv:
 	LoadCapPCC         ca0, compartment_switcher_sealing_key
-	li                 a1, 10
+	li                 a1, SEAL_TYPE_SealedTrustedStacks
 	csetaddr           ca0, ca0, a1
 	cspecialr          ca1, mtdc
 	cseal              ca0, ca1, ca0
diff --git a/sdk/core/switcher/misc-assembly.h b/sdk/core/switcher/misc-assembly.h
new file mode 100644
index 0000000..f93293c
--- /dev/null
+++ b/sdk/core/switcher/misc-assembly.h
@@ -0,0 +1,43 @@
+// Copyright CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#pragma once
+#include <assembly-helpers.h>
+
+/*
+ * Constant to represent the raw permissions of the compartment CSP.  We use
+ * this in the switcher, to verify the permissions of the CSP that comes from
+ * the compartment are exactly what we expect.
+ */
+EXPORT_ASSEMBLY_EXPRESSION(COMPARTMENT_STACK_PERMISSIONS,
+                           (CHERI::PermissionSet{
+                             CHERI::Permission::Load,
+                             CHERI::Permission::Store,
+                             CHERI::Permission::LoadStoreCapability,
+                             CHERI::Permission::LoadMutable,
+                             CHERI::Permission::StoreLocal,
+                             CHERI::Permission::LoadGlobal}
+                              .as_raw()),
+                           0x7e)
+
+/**
+ * Space reserved at the top of a stack on entry to the compartment.
+ *
+ * This *must* be a multiple of 16, which is the stack alignment.
+ */
+#define STACK_ENTRY_RESERVED_SPACE 16
+
+#ifdef __cplusplus
+using namespace priv;
+#endif
+
+EXPORT_ASSEMBLY_NAME(MCAUSE_THREAD_EXIT, 24)
+EXPORT_ASSEMBLY_NAME(MCAUSE_THREAD_INTERRUPT, 25)
+EXPORT_ASSEMBLY_NAME(MCAUSE_CHERI, 28)
+
+EXPORT_ASSEMBLY_EXPRESSION(SEAL_TYPE_SealedImportTableEntries,
+                           SealingType::SealedImportTableEntries,
+                           9)
+EXPORT_ASSEMBLY_EXPRESSION(SEAL_TYPE_SealedTrustedStacks,
+                           SealingType::SealedTrustedStacks,
+                           10)
diff --git a/sdk/core/switcher/trusted-stack-assembly.h b/sdk/core/switcher/trusted-stack-assembly.h
index 02fc248..7969662 100644
--- a/sdk/core/switcher/trusted-stack-assembly.h
+++ b/sdk/core/switcher/trusted-stack-assembly.h
@@ -4,21 +4,21 @@
 #pragma once
 #include <assembly-helpers.h>
 EXPORT_ASSEMBLY_OFFSET(TrustedStack, mepcc, 0 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c1, 1 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, cra, 1 * 8)
 EXPORT_ASSEMBLY_OFFSET(TrustedStack, csp, 2 * 8)
 EXPORT_ASSEMBLY_OFFSET(TrustedStack, cgp, 3 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c4, 4 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c5, 5 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c6, 6 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c7, 7 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c8, 8 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c9, 9 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c10, 10 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c11, 11 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c12, 12 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c13, 13 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c14, 14 * 8)
-EXPORT_ASSEMBLY_OFFSET(TrustedStack, c15, 15 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ctp, 4 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ct0, 5 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ct1, 6 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ct2, 7 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, cs0, 8 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, cs1, 9 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ca0, 10 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ca1, 11 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ca2, 12 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ca3, 13 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ca4, 14 * 8)
+EXPORT_ASSEMBLY_OFFSET(TrustedStack, ca5, 15 * 8)
 EXPORT_ASSEMBLY_OFFSET(TrustedStack, hazardPointers, 16 * 8)
 EXPORT_ASSEMBLY_OFFSET(TrustedStack, mstatus, 17 * 8)
 EXPORT_ASSEMBLY_OFFSET(TrustedStack, mcause, (17 * 8) + 4)
@@ -57,18 +57,3 @@
 
 #define TSTACKOFFSET_FIRSTFRAME                                                \
 	(TrustedStack_offset_frameoffset + TSTACK_HEADER_SZ)
-
-/* Constant to represent the raw permissions of the compartment CSP.
- *  We use this in the switcher, to verify the CSP comes from the
- *  compartment is exactly what we expect.
- *  This represents the following permissions:
- *  Load, Store, LoadStoreCapability, LoadMutable StoreLocal and LoadGlobal
- */
-#define COMPARTMENT_STACK_PERMISSIONS 0x7e
-
-/**
- * Space reserved at the top of a stack on entry to the compartment.
- *
- * This *must* be a multiple of 16, which is the stack alignment.
- */
-#define STACK_ENTRY_RESERVED_SPACE 16
diff --git a/sdk/core/switcher/tstack.h b/sdk/core/switcher/tstack.h
index 45af06e..dc8338b 100644
--- a/sdk/core/switcher/tstack.h
+++ b/sdk/core/switcher/tstack.h
@@ -32,21 +32,21 @@
 struct TrustedStackGeneric
 {
 	void  *mepcc;
-	void  *c1;
-	void  *csp;
-	void  *cgp;
-	void  *c4;
-	void  *c5;
-	void  *c6;
-	void  *c7;
-	void  *c8;
-	void  *c9;
-	void  *c10;
-	void  *c11;
-	void  *c12;
-	void  *c13;
-	void  *c14;
-	void  *c15;
+	void  *cra; // c1
+	void  *csp; // c2
+	void  *cgp; // c3
+	void  *ctp; // c4
+	void  *ct0; // c5
+	void  *ct1; // c6
+	void  *ct2; // c7
+	void  *cs0; // c8
+	void  *cs1; // c9
+	void  *ca0; // c10
+	void  *ca1; // c11
+	void  *ca2; // c12
+	void  *ca3; // c13
+	void  *ca4; // c14
+	void  *ca5; // c15
 	void  *hazardPointers;
 	size_t mstatus;
 	size_t mcause;
@@ -77,13 +77,3 @@
 using TrustedStack = TrustedStackGeneric<0>;
 
 #include "trusted-stack-assembly.h"
-
-static_assert(
-  CheckSize<COMPARTMENT_STACK_PERMISSIONS,
-            CHERI::PermissionSet{CHERI::Permission::Load,
-                                 CHERI::Permission::Store,
-                                 CHERI::Permission::LoadStoreCapability,
-                                 CHERI::Permission::LoadMutable,
-                                 CHERI::Permission::StoreLocal,
-                                 CHERI::Permission::LoadGlobal}
-              .as_raw()>::value);
diff --git a/sdk/core/token_library/token_unseal.S b/sdk/core/token_library/token_unseal.S
index 8391902..1dccc04 100644
--- a/sdk/core/token_library/token_unseal.S
+++ b/sdk/core/token_library/token_unseal.S
@@ -2,24 +2,27 @@
 #include <cheri-builtins.h>
 #include "../allocator/token.h"
 
-/*
- * An in-assembler implementation of
+	.hidden __sealingkey
+	.type   __sealingkey,@object
+	.section    .sealing_key1,"aw",@progbits
+	.globl  __sealingkey
+	.p2align    3
+__sealingkey:
+	.chericap   0
+	.size   __sealingkey, 8
+
+
+.section .text,"ax",@progbits
+
+.p2align 1
+
+/**
+ * The core of unsealing:
  *
- * [[cheri::interrupt_state(disabled)]] void *__cheri_libcall
- * token_obj_unseal(struct SKeyStruct *, struct SObjStruct *);
- *
- * The name has been manually mangled as per the C++ rules.
+ *   void *token_unseal_internal(struct SKeyStruct *, struct SObjStruct *, int);
  */
 
-	.section .text._Z16token_obj_unsealP10SKeyStructP10SObjStruct,"axG", \
-		@progbits,_Z16token_obj_unsealP10SKeyStructP10SObjStruct,comdat
-
-	.hidden  _Z16token_obj_unsealP10SKeyStructP10SObjStruct
-	.globl   _Z16token_obj_unsealP10SKeyStructP10SObjStruct
-	.p2align 1
-	.type    _Z16token_obj_unsealP10SKeyStructP10SObjStruct,@function
-
-_Z16token_obj_unsealP10SKeyStructP10SObjStruct:
+.Ltoken_unseal_internal:
   /*
    * Register allocation:
    *
@@ -28,9 +31,11 @@
    *
    *  - ca1 holds the user's sealed object pointer
    *
-   *  - t0/ct0 holds a copy of the user key
+   *  - a2 contains the expected sealing type.
    *
-   *  - t1/ct1 is used within each local computation and never holds secrets
+   *  - t0 holds a copy of the user key's address field (authorized type)
+   *
+   *  - t1 is used within each local computation and never holds secrets
    */
 
   /* Verify key tag */
@@ -48,8 +53,8 @@
   andi     t1, t1, CHERI_PERM_UNSEAL
   beqz     t1, .Lexit_failure
 
-  /* Copy key capability to scratch register */
-  cmove ct0, ca0
+  /* Copy key type to scratch register */
+  cgetaddr t0, ca0
 
   /*
    * Load unsealing root capability, to be clobbered by return value
@@ -59,6 +64,7 @@
 .Lload_sealing_key:
   auipcc ca0, %cheriot_compartment_hi(__sealingkey)
   clc    ca0, %cheriot_compartment_lo_i(.Lload_sealing_key)(ca0)
+  csetaddr ca0, ca0, a2
 
   /* Unseal, clobbering authority */
   cunseal ca0, ca1, ca0
@@ -73,17 +79,12 @@
    */
   clw t1, TokenSObj_offset_type(ca0)
 
-  /*
-   * Verify that the loaded value matches the address of the key (via as-integer
-   * access to capability register ct0).
-   */
+  /* Verify that the loaded value matches the address of the key. */
   bne t0, t1, .Lexit_failure
 
   /* Subset bounds to ->data */
   // Get the top into t1
-  cgetlen         t1, ca0
-  cgetbase        t0, ca0
-  add             t1, t1, t0
+  cgettop         t1, ca0
   // Move the address to the start of the data
   cincoffset      ca0, ca0, TokenSObj_offset_data
   // Subtract the address of the (to-be-returned-unsealed) data from the top to
@@ -101,8 +102,60 @@
   cmove ca0, cnull
   cret
 
+/**
+ * An in-assembler implementation of
+ *
+ * [[cheri::interrupt_state(disabled)]] void *__cheri_libcall
+ * token_obj_unseal(struct SKeyStruct *, struct SObjStruct *);
+ *
+ * The name has been manually mangled as per the C++ rules.
+ */
+	.hidden _Z16token_obj_unsealP10SKeyStructP10SObjStruct
+	.globl  _Z16token_obj_unsealP10SKeyStructP10SObjStruct
+_Z16token_obj_unsealP10SKeyStructP10SObjStruct:
+	cgettype a2, ca1
+	j        .Ltoken_unseal_internal
+
+/**
+ * An in-assembler implementation of
+ *
+ * [[cheri::interrupt_state(disabled)]] void *__cheri_libcall
+ * token_obj_unseal_static(struct SKeyStruct *, struct SObjStruct *);
+ *
+ * The name has been manually mangled as per the C++ rules.
+ */
+	.hidden  _Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct
+	.globl   _Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct
+_Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct:
+	li       a2, CheriSealTypeStaticToken
+	j        .Ltoken_unseal_internal
+
+/**
+ * An in-assembler implementation of
+ *
+ * [[cheri::interrupt_state(disabled)]] void *__cheri_libcall
+ * token_obj_unseal_dynamic(struct SKeyStruct *, struct SObjStruct *);
+ *
+ * The name has been manually mangled as per the C++ rules.
+ */
+	.hidden  _Z16token_obj_unsealP10SKeyStructP10SObjStruct
+	.globl   _Z16token_obj_unsealP10SKeyStructP10SObjStruct
+_Z24token_obj_unseal_dynamicP10SKeyStructP10SObjStruct:
+	li       a2, CheriSealTypeAllocator
+	j        .Ltoken_unseal_internal
+
 /* TODO: Eventually this goes away, when the assembler can generate it for us */
 CHERIOT_EXPORT_LIBCALL \
   _Z16token_obj_unsealP10SKeyStructP10SObjStruct, \
   0 /* No stack usage */, \
   0b00010010 /* IRQs deferred, zero two registers */
+
+CHERIOT_EXPORT_LIBCALL \
+  _Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct, \
+  0 /* No stack usage */, \
+  0b00010010 /* IRQs deferred, zero two registers */
+
+CHERIOT_EXPORT_LIBCALL \
+  _Z24token_obj_unseal_dynamicP10SKeyStructP10SObjStruct, \
+  0 /* No stack usage */, \
+  0b00010010 /* IRQs deferred, zero two registers */
diff --git a/sdk/firmware.ldscript.in b/sdk/firmware.ldscript.in
index 9fc9a29..a9a3956 100644
--- a/sdk/firmware.ldscript.in
+++ b/sdk/firmware.ldscript.in
@@ -46,6 +46,8 @@
 	scheduler_code : CAPALIGN
 	{
 		.scheduler_start = .;
+		*.scheduler.compartment(.compartment_sealing_keys);
+		.scheduler_import_start = .;
 		*.scheduler.compartment(.compartment_import_table);
 		.scheduler_import_end = .;
 		*.scheduler.compartment(.text .text.* .rodata .rodata.* .data.rel.ro);
@@ -55,6 +57,8 @@
 	allocator_code : CAPALIGN
 	{
 		.allocator_start = .;
+		*/cheriot.allocator.compartment(.compartment_sealing_keys);
+		.allocator_import_start = .;
 		*/cheriot.allocator.compartment(.compartment_import_table);
 		.allocator_import_end = .;
 		allocator.compartment(.text .text.* .rodata .rodata.* .data.rel.ro);
@@ -66,6 +70,8 @@
 	token_library_code : CAPALIGN
 	{
 		.token_library_start = .;
+		*/cheriot.token_library.library(.compartment_sealing_keys);
+		.token_library_import_start = .;
 		*/cheriot.token_library.library(.compartment_import_table);
 		.token_library_import_end = .;
 		token_library.library(.text .text.* .rodata .rodata.* .data.rel.ro);
@@ -156,6 +162,8 @@
 		LONG(.compartment_switcher_start);
 		# Compartment switcher end
 		SHORT(.compartment_switcher_end - .compartment_switcher_start);
+		# Cross-compartment call return path
+		SHORT(switcher_skip_compartment_call - .compartment_switcher_start);
 		# Compartment switcher sealing key
 		SHORT(compartment_switcher_sealing_key - .compartment_switcher_start);
 		# Switcher's copy of the scheduler's PCC.
@@ -178,8 +186,10 @@
 		LONG(.scheduler_globals);
 		# Scheduler globals end size
 		SHORT(SIZEOF(.scheduler_globals));
+		# Start of the scheduler's import table
+		LONG(.scheduler_import_start);
 		# Size of the scheduler import table
-		SHORT(.scheduler_import_end - .scheduler_start);
+		SHORT(.scheduler_import_end - .scheduler_import_start);
 		# Address of scheduler export table
 		LONG(.scheduler_export_table);
 		# Size of the scheduler export table
@@ -197,8 +207,10 @@
 		LONG(.allocator_globals);
 		# Allocator globals end
 		SHORT(SIZEOF(.allocator_globals));
+		# Start of the allocator's import table
+		LONG(.allocator_import_start);
 		# Size of the allocator import table
-		SHORT(.allocator_import_end - .allocator_start);
+		SHORT(.allocator_import_end - .allocator_import_start);
 		# Address of allocator export table
 		LONG(.allocator_export_table);
 		# Size of the allocator export table
@@ -215,8 +227,10 @@
 		# No data segment
 		LONG(0);
 		SHORT(0);
+		# Start of the token_library's import table
+		LONG(.token_library_import_start);
 		# Size of the token server import table
-		SHORT(.token_library_import_end - .token_library_start);
+		SHORT(.token_library_import_end - .token_library_import_start);
 		# Address of the token server export table
 		LONG(.token_library_export_table);
 		# Size of the token server export table
@@ -232,7 +246,7 @@
 		# loader versions.
 		# New versions of this can be generated with:
 		# head /dev/random | shasum | cut -c 0-8
-		LONG(0x6cef3879);
+		LONG(0xca2b63de);
 		# Number of library headers.
 		SHORT(@library_count@);
 		# Number of compartment headers.
diff --git a/sdk/include/FreeRTOS-Compat/queue.h b/sdk/include/FreeRTOS-Compat/queue.h
index 088d588..9b8f072 100644
--- a/sdk/include/FreeRTOS-Compat/queue.h
+++ b/sdk/include/FreeRTOS-Compat/queue.h
@@ -8,17 +8,7 @@
 /**
  * Queue handle.  This is used to reference queues in the API functions.
  */
-typedef struct
-{
-	/**
-	 * The real handle, holds pointers to the relevant elements of the queue.
-	 */
-	struct QueueHandle handle;
-	/**
-	 * The pointer used to free the queue.
-	 */
-	void *freePointer;
-} * QueueHandle_t;
+typedef struct MessageQueue *QueueHandle_t;
 
 /**
  * Receive a message on a queue.  The message is received into `buffer`, which
@@ -34,7 +24,7 @@
 xQueueReceive(QueueHandle_t queueHandle, void *buffer, TickType_t waitTicks)
 {
 	struct Timeout timeout = {0, waitTicks};
-	int            rv = queue_receive(&timeout, &queueHandle->handle, buffer);
+	int            rv = queue_receive(&timeout, queueHandle, buffer);
 
 	if (rv == 0)
 		return pdPASS;
@@ -54,7 +44,7 @@
                                           TickType_t    waitTicks)
 {
 	struct Timeout timeout = {0, waitTicks};
-	int            rv      = queue_send(&timeout, &queueHandle->handle, buffer);
+	int            rv      = queue_send(&timeout, queueHandle, buffer);
 
 	if (rv == 0)
 		return pdPASS;
@@ -86,24 +76,13 @@
 static inline QueueHandle_t xQueueCreate(UBaseType_t uxQueueLength,
                                          UBaseType_t uxItemSize)
 {
-	QueueHandle_t  ret;
+	QueueHandle_t  ret = NULL;
 	struct Timeout timeout = {0, UnlimitedTimeout};
-	ret                    = (QueueHandle_t)malloc(sizeof(*ret));
-	if (!ret)
-	{
-		return NULL;
-	}
 	int rc = queue_create(&timeout,
 	                      MALLOC_CAPABILITY,
-	                      &ret->handle,
-	                      &ret->freePointer,
+	                      &ret,
 	                      uxItemSize,
 	                      uxQueueLength);
-	if (rc)
-	{
-		free(ret);
-		return NULL;
-	}
 	return ret;
 }
 #endif
@@ -113,8 +92,7 @@
  */
 static inline void vQueueDelete(QueueHandle_t xQueue)
 {
-	free(xQueue->freePointer);
-	free(xQueue);
+	queue_destroy(MALLOC_CAPABILITY, xQueue);
 }
 
 /**
@@ -126,7 +104,7 @@
 static inline UBaseType_t uxQueueMessagesWaiting(const QueueHandle_t xQueue)
 {
 	size_t ret;
-	int    rv = queue_items_remaining(&xQueue->handle, &ret);
+	int    rv = queue_items_remaining(xQueue, &ret);
 
 	assert(rv == 0);
 
diff --git a/sdk/include/assembly-helpers.h b/sdk/include/assembly-helpers.h
index cdc92d7..73b0a68 100644
--- a/sdk/include/assembly-helpers.h
+++ b/sdk/include/assembly-helpers.h
@@ -22,6 +22,25 @@
 };
 
 /**
+ * Export a macro into assembly named `name` with value `value`.  In C++, this
+ * macro will report an error if the provided value does not equal the constexpr
+ * evaluation of `expression`.
+ */
+#	define EXPORT_ASSEMBLY_NAME(name, val)                                    \
+		static_assert(CheckSize<name, val>::value,                             \
+		              "Value provided for assembly is incorrect");
+
+/**
+ * Export a macro into assembly named `name` with value `value`.  In C++, this
+ * macro will report an error if the provided value does not equal the constexpr
+ * evaluation of `expression`.
+ */
+#	define EXPORT_ASSEMBLY_EXPRESSION(name, expression, val)                  \
+		static constexpr size_t name = expression;                             \
+		static_assert(CheckSize<name, val>::value,                             \
+		              "Value provided for assembly is incorrect");
+
+/**
  * Export a macro into assembly of the form `{structure}_offset_{field}`.  The
  * value of this macro will be `value`.  In C++, this macro will report an error
  * if the provided value does not match the compiler's understanding of the
@@ -61,13 +80,19 @@
 		static_assert(CheckSize<sizeof(structure), val>::value,                \
 		              "Size provided for assembly is incorrect");
 #elif defined(__ASSEMBLER__)
+#	define EXPORT_ASSEMBLY_NAME(name, value)                                  \
+		.set name, value
+#	define EXPORT_ASSEMBLY_EXPRESSION(name, expression, value)                \
+		.set name, value
 #	define EXPORT_ASSEMBLY_OFFSET_NAMED(structure, field, value, name)        \
-		.set name value
+		.set name, value
 #	define EXPORT_ASSEMBLY_OFFSET(structure, field, value)                    \
 		.set structure##_offset_##field, value
 #	define EXPORT_ASSEMBLY_SIZE(structure, value) .set structure##_size, value
 #else
-#	define EXPORT_ASSEMBLY_OFFSET(structure, field, name, value)
+#	define EXPORT_ASSEMBLY_NAME(name, value)
+#	define EXPORT_ASSEMBLY_EXPRESSION(name, expression, value)
+#	define EXPORT_ASSEMBLY_OFFSET(structure, field, name)
 #	define EXPORT_ASSEMBLY_SIZE(structure, name, value)
 #	define EXPORT_ASSEMBLY_OFFSET_NAMED(structure, field, value, name)
 #endif
diff --git a/sdk/include/cdefs.h b/sdk/include/cdefs.h
index 2242e7e..0a91697 100644
--- a/sdk/include/cdefs.h
+++ b/sdk/include/cdefs.h
@@ -61,7 +61,6 @@
 #define __section(x) __attribute__((section(x)))
 #define __alloc_size(x) __attribute__((alloc_size(x)))
 #define __alloc_align(x) __attribute__((alloc_align(x)))
-#define __cheri_callback __attribute__((cheri_ccallback))
 #if __has_attribute(cheriot_minimum_stack)
 #	define __cheriot_minimum_stack(x) __attribute__((cheriot_minimum_stack(x)))
 #else
@@ -69,15 +68,34 @@
 	  "cheriot_minimum_stack attribute not supported, please update your compiler"
 #	define __cheriot_minimum_stack(x)
 #endif
+
 // When running clang-tidy, we use the same compile flags for everything and so
 // will get errors about things being defined in the wrong compartment, so
 // define away the compartment name and pretend everything is local for now.
-#ifdef CLANG_TIDY
+#if defined(CLANG_TIDY) || defined(__CHERIOT_BAREMETAL__)
 #	define __cheri_compartment(x)
 #else
 #	define __cheri_compartment(x) __attribute__((cheri_compartment(x)))
 #endif
-#define __cheri_libcall __attribute__((cheri_libcall))
+
+// Define the CHERIoT calling-convention attributes macros to nothing if we're
+// targeting bare metal and to the correct attributes if we're targeting the
+// RTOS.
+#ifdef __CHERIOT_BAREMETAL__
+#	define __cheri_libcall
+#	define __cheri_callback
+#else
+#	define __cheri_libcall __attribute__((cheri_libcall))
+#	define __cheri_callback __attribute__((cheri_ccallback))
+
+/**
+ * Define the symbol for the libcall that the compiler will expand the `strlen`
+ * builtin to.  This builtin is used internally in libc++ (and possibly in
+ * other places) to avoid the namespace pollution from including `string.h` but
+ * is either constant folded in the front end or expanded to a libcall.
+ */
+unsigned __builtin_strlen(const char *str) __asm__("_Z6strlenPKc");
+#endif
 
 #define offsetof(a, b) __builtin_offsetof(a, b)
 
@@ -107,14 +125,6 @@
 #	define __clang_ignored_warning_pop()
 #endif
 
-/**
- * Define the symbol for the libcall that the compiler will expand the `strlen`
- * builtin to.  This builtin is used internally in libc++ (and possibly in
- * other places) to avoid the namespace pollution from including `string.h` but
- * is either constant folded in the front end or expanded to a libcall.
- */
-unsigned __builtin_strlen(const char *str) __asm__("_Z6strlenPKc");
-
 #if !defined(CLANG_TIDY) && !__has_builtin(__builtin_cheri_top_get)
 #	error Your compiler is too old for this version of CHERIoT RTOS, please upgrade to a newer version
 #endif
diff --git a/sdk/include/cheri.h b/sdk/include/cheri.h
index f7cc6bc..b10d059 100644
--- a/sdk/include/cheri.h
+++ b/sdk/include/cheri.h
@@ -9,6 +9,359 @@
 struct Timeout;
 
 /**
+ * The complete set of architectural permissions.
+ */
+enum CHERIPermission
+{
+	/**
+	 * Capability refers to global memory (this capability may be stored
+	 * anywhere).
+	 */
+	CheriPermissionGlobal = 0,
+	/**
+	 * Global capabilities can be loaded through this capability.  Without
+	 *  this permission, any capability loaded via this capability will
+	 *  have `Global` and `LoadGlobal` removed.
+	 */
+	CheriPermissionLoadGlobal = 1,
+	/**
+	 * Capability may be used to store.  Any store via a capability without
+	 * this permission will trap.
+	 */
+	CheriPermissionStore = 2,
+	/**
+	 * Capabilities with store permission may be loaded through this
+	 * capability.  Without this, any loaded capability will have
+	 * `LoadMutable` and `Store` removed.
+	 */
+	CheriPermissionLoadMutable = 3,
+	/**
+	 * This capability may be used to store capabilities that do not have
+	 * `Global` permission.
+	 */
+	CheriPermissionStoreLocal = 4,
+	/**
+	 * This capability can be used to load.
+	 */
+	CheriPermissionLoad = 5,
+	/**
+	 * Any load and store permissions on this capability convey the right to
+	 * load or store capabilities in addition to data.
+	 */
+	CheriPermissionLoadStoreCapability = 6,
+	/**
+	 * If installed as the program counter capability, running code may
+	 * access privileged system registers.
+	 */
+	CheriPermissionAccessSystemRegisters = 7,
+	/**
+	 * This capability may be used as a jump target and used to execute
+	 * instructions.
+	 */
+	CheriPermissionExecute = 8,
+	/**
+	 * This capability may be used to unseal other capabilities.  The
+	 * 'address' range is in the sealing type namespace and not in the
+	 * memory namespace.
+	 */
+	CheriPermissionUnseal = 9,
+	/**
+	 * This capability may be used to seal other capabilities.  The
+	 * 'address' range is in the sealing type namespace and not in the
+	 * memory namespace.
+	 */
+	CheriPermissionSeal = 10,
+	/**
+	 * Software defined permission bit, no architectural meaning.
+	 */
+	CheriPermissionUser0 = 11
+};
+
+/**
+ * The codes used in the cause field of the mtval CSR when the processor
+ * takes a CHERI exception.
+ */
+enum CHERICauseCode
+{
+	/**
+	 * No exception. This value is passed to the error handler after a
+	 * forced unwind in a called compartment.
+	 */
+	CheriCauseCodeNone = 0,
+	/**
+	 * Attempted to use a capability outside its bounds.
+	 */
+	CheriCauseCodeBoundsViolation = 1,
+	/**
+	 * Attempted to use an untagged capability to authorize something.
+	 */
+	CheriCauseCodeTagViolation = 2,
+	/**
+	 * Attempted to use a sealed capability to authorize something.
+	 */
+	CheriCauseCodeSealViolation = 3,
+	/**
+	 * Attempted to jump to a capability without `Permission::Execute`.
+	 */
+	CheriCauseCodePermitExecuteViolation = 0x11,
+	/**
+	 * Attempted to load via a capability without `Permission::Load`.
+	 */
+	CheriCauseCodePermitLoadViolation = 0x12,
+	/**
+	 * Attempted to store via a capability without `Permission::Store`.
+	 */
+	CheriCauseCodePermitStoreViolation = 0x13,
+	/**
+	 * Attempted to store a tagged capability via a capability without
+	 * `Permission::LoadStoreCapability`.
+	 */
+	CheriCauseCodePermitStoreCapabilityViolation = 0x15,
+	/**
+	 * Attempted to store a tagged capability without `Permission::Global`
+	 * via capability without `Permission::StoreLocal`.
+	 */
+	CheriCauseCodePermitStoreLocalCapabilityViolation = 0x16,
+	/**
+	 * Attempted to access a restricted CSR or SCR with PCC without
+	 * `Permission::AccessSystemRegisters`.
+	 */
+	CheriCauseCodePermitAccessSystemRegistersViolation = 0x18,
+	/**
+	 * Used to represent a value that has no valid meaning in hardware.
+	 */
+	CheriCauseCodeInvalid = -1
+};
+
+/**
+ * Register numbers as reported in cap idx field of  `mtval` CSR when
+ * a CHERI exception is taken. Values less than 32 refer to general
+ * purpose registers and others to SCRs (of these, only PCC can actually
+ * cause an exception).
+ */
+enum CHERIRegisterNumber
+{
+	/**
+	 * The zero register, which always contains the `NULL` capability.
+	 */
+	CheriRegisterNumberCzr = 0x0,
+	/**
+	 * `$c1` / `$cra` used by the ABI as the return address.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCra = 0x1,
+	/**
+	 * `$c2` / `$csp` used by the ABI as the stack pointer.
+	 * Preserved across calls.
+	 */
+	CheriRegisterNumberCsp = 0x2,
+	/**
+	 * `$c3` / `$cgp` used by the ABI as the global pointer.
+	 * Not allocatable by the compiler, set by the switcher on compartment
+	 * entry.
+	 */
+	CheriRegisterNumberCgp = 0x3,
+	/**
+	 * `$c4` / `$ctp` used by the ABI as the thread pointer.
+	 * Currently unused by the compiler.
+	 * Not preserved across compartment calls.
+	 */
+	CheriRegisterNumberCtp = 0x4,
+	/**
+	 * `$c5` / `$ct0` used by the ABI as temporary register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCT0 = 0x5,
+	/**
+	 * `$c6` / `$ct1` used by the ABI as temporary register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCT1 = 0x6,
+	/**
+	 * `$c7` / `$ct2` used by the ABI as temporary register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCT2 = 0x7,
+	/**
+	 * `$c8` / `$cs0` used by the ABI as a callee-saved register.
+	 * Preserved across calls.
+	 */
+	CheriRegisterNumberCS0 = 0x8,
+	/**
+	 * `$c9` / `$cs1` used by the ABI as a callee-saved register.
+	 * Preserved across calls.
+	 */
+	CheriRegisterNumberCS1 = 0x9,
+	/**
+	 * `$c10` / `$ca0` used by the ABI as an argument register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCA0 = 0xa,
+	/**
+	 * `$c11` / `$ca1` used by the ABI as an argument register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCA1 = 0xb,
+	/**
+	 * `$c12` / `$ca2` used by the ABI as an argument register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCA2 = 0xc,
+	/**
+	 * `$c13` / `$ca3` used by the ABI as an argument register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCA3 = 0xd,
+	/**
+	 * `$c14` / `$ca4` used by the ABI as an argument register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCA4 = 0xe,
+	/**
+	 * `$c15` / `$ca5` used by the ABI as an argument register.
+	 * Not preserved across calls.
+	 */
+	CheriRegisterNumberCA5 = 0xf,
+	/**
+	 * The Program Counter Capability.
+	 *
+	 * Special capability register used to authorize instruction fetch. The
+	 * address is that of the faulting instruction. Also used for accessing
+	 * read-only globals.
+	 */
+	CheriRegisterNumberPcc = 0x20,
+	/**
+	 * Machine-mode Trap Code Capability.
+	 *
+	 * Special capability register that
+	 * is installed in PCC when the CPU takes a trap. The address has the
+	 * same semantics as the RISC-V `mtvec` CSR. Only accessible when PCC
+	 * has the AccessSystemRegisters permission.
+	 */
+	CheriRegisterNumberMtcc = 0x3c,
+	/**
+	 * Machine-mode Tusted Data Capability.
+	 *
+	 * Special capability register that contains the memory root capability
+	 * on boot. Only accessible when PCC has the AccessSystemRegisters
+	 * permission.  Use by the RTOS to store a capability to the trusted
+	 * stack.
+	 */
+	CheriRegisterNumberMtdc = 0x3d,
+	/**
+	 * Machine-mode Scratch Capability. Special capabiltiy register that
+	 * contains the sealing root capability on boot. Only accessible when
+	 * PCC has the AccessSystemRegisters permission.
+	 */
+	CheriRegisterNumberMScratchC = 0x3e,
+	/**
+	 * Machine-mode Exception Program Counter Capability. Special capability
+	 * register that contains the PCC of the faulting instruction on trap.
+	 * The address has the same semantics as the RISC-V `mepc` CSR. Only
+	 * accessible when PCC has the AccessSystemRegisters permission.
+	 */
+	CheriRegisterNumberMepcc = 0x3f,
+	/**
+	 * Indicates a value that is not used by the hardware to refer to a
+	 * register.
+	 */
+	CheriRegisterNumberInvalid = -1
+};
+
+/**
+ * Sealing types.
+ */
+enum CHERISealingType
+{
+	/**
+	 * 0 represents unsealed.
+	 */
+	CheriSealTypeUnsealed = 0,
+
+	/**
+	 * Sentry that inherits interrupt status.
+	 */
+	CheriSealTypeSentryInheriting,
+
+	/**
+	 * Sentry that disables interrupts on calls.
+	 */
+	CheriSealTypeSentryDisabling,
+
+	/**
+	 * Sentry that enables interrupts on calls.
+	 */
+	CheriSealTypeSentryEnabling,
+
+	/**
+	 * Return sentry that disables interrupts on return
+	 */
+	CheriSealTypeReturnSentryDisabling,
+
+	/**
+	 * Return sentry that enables interrupts on return
+	 */
+	CheriSealTypeReturnSentryEnabling,
+
+	/**
+	 * Marker for the first sealing type that's valid for data capabilities.
+	 */
+	CheriSealTypeFirstDataSealingType = 9,
+
+	/**
+	 * The sealing type used for sealed export table entries.
+	 *
+	 * This is RTOS- and not CHERIoT-specific.
+	 */
+	CheriSealTypeSealedImportTableEntries = CheriSealTypeFirstDataSealingType,
+
+	/**
+	 * The compartment switcher has a sealing type for the trusted stack.
+	 *
+	 * This must be the second data sealing type so that we can also permit
+	 * the switcher to unseal sentries and export table entries.
+	 *
+	 * This is RTOS- and not CHERIoT-specific.
+	 */
+	CheriSealTypeSealedTrustedStacks,
+
+	/**
+	 * The allocator has a sealing type for the software sealing mechanism
+	 * with dynamically allocated objects.
+	 *
+	 * This is RTOS- and not CHERIoT-specific.
+	 */
+	CheriSealTypeAllocator,
+
+	/**
+	 * The loader reserves a sealing type for the software sealing
+	 * mechanism.  The permit-unseal capability for this is destroyed after
+	 * the loader has run, which guarantees that anything sealed with this
+	 * type was present in the original firmware image.  The token library
+	 * has the only permit-unseal capability for this type.
+	 *
+	 * This is RTOS- and not CHERIoT-specific.
+	 */
+	CheriSealTypeStaticToken,
+
+	/**
+	 * The first sealing key that is reserved for use by the allocator's
+	 * software sealing mechanism and used for static sealing types,
+	 *
+	 * Architecturally, this is the smallest non-interpreted sealing type.
+	 */
+	CheriSealTypeFirstStaticSoftware = 16,
+
+	/**
+	 * The first sealing key in the space that the allocator will
+	 * dynamically allocate for sealing types.
+	 *
+	 * This is RTOS- and not CHERIoT-specific.
+	 */
+	CheriSealTypeFirstDynamicSoftware = 0x1000000
+};
+
+/**
  * Checks that `ptr` is valid, unsealed, has at least `rawPermissions`, and has
  * at least `space` bytes after the current offset.
  *
diff --git a/sdk/include/cheri.hh b/sdk/include/cheri.hh
index 8e18db3..4663e17 100644
--- a/sdk/include/cheri.hh
+++ b/sdk/include/cheri.hh
@@ -22,64 +22,64 @@
 		 * Capability refers to global memory (this capability may be stored
 		 * anywhere).
 		 */
-		Global = 0,
+		Global = CheriPermissionGlobal,
 		/**
 		 * Global capabilities can be loaded through this capability.  Without
 		 *  this permission, any capability loaded via this capability will
 		 *  have `Global` and `LoadGlobal` removed.
 		 */
-		LoadGlobal = 1,
+		LoadGlobal = CheriPermissionLoadGlobal,
 		/**
 		 * Capability may be used to store.  Any store via a capability without
 		 * this permission will trap.
 		 */
-		Store = 2,
+		Store = CheriPermissionStore,
 		/**
 		 * Capabilities with store permission may be loaded through this
 		 * capability.  Without this, any loaded capability will have
 		 * `LoadMutable` and `Store` removed.
 		 */
-		LoadMutable = 3,
+		LoadMutable = CheriPermissionLoadMutable,
 		/**
 		 * This capability may be used to store capabilities that do not have
 		 * `Global` permission.
 		 */
-		StoreLocal = 4,
+		StoreLocal = CheriPermissionStoreLocal,
 		/**
 		 * This capability can be used to load.
 		 */
-		Load = 5,
+		Load = CheriPermissionLoad,
 		/**
 		 * Any load and store permissions on this capability convey the right to
 		 * load or store capabilities in addition to data.
 		 */
-		LoadStoreCapability = 6,
+		LoadStoreCapability = CheriPermissionLoadStoreCapability,
 		/**
 		 * If installed as the program counter capability, running code may
 		 * access privileged system registers.
 		 */
-		AccessSystemRegisters = 7,
+		AccessSystemRegisters = CheriPermissionAccessSystemRegisters,
 		/**
 		 * This capability may be used as a jump target and used to execute
 		 * instructions.
 		 */
-		Execute = 8,
+		Execute = CheriPermissionExecute,
 		/**
 		 * This capability may be used to unseal other capabilities.  The
 		 * 'address' range is in the sealing type namespace and not in the
 		 * memory namespace.
 		 */
-		Unseal = 9,
+		Unseal = CheriPermissionUnseal,
 		/**
 		 * This capability may be used to seal other capabilities.  The
 		 * 'address' range is in the sealing type namespace and not in the
 		 * memory namespace.
 		 */
-		Seal = 10,
+		Seal = CheriPermissionSeal,
 		/**
 		 * Software defined permission bit, no architectural meaning.
 		 */
-		User0 = 11
+		User0 = CheriPermissionUser0
 	};
 
 	/**
@@ -361,6 +361,30 @@
 	};
 
 	/**
+	 * Rounds `len` up to a CHERI representable length for the current
+	 * architecture.
+	 */
+	__always_inline inline size_t representable_length(size_t length)
+	{
+		return __builtin_cheri_round_representable_length(length);
+	}
+
+	/**
+	 * Returns the alignment mask required for a given length.
+	 */
+	__always_inline inline size_t representable_alignment_mask(size_t length)
+	{
+		return __builtin_cheri_representable_alignment_mask(length);
+	}
+
+	/// Can the range [base, base + size) be precisely covered by a capability?
+	inline bool is_precise_range(ptraddr_t base, size_t size)
+	{
+		return (base & ~representable_alignment_mask(size)) == 0 &&
+		       representable_length(size) == size;
+	}
+
+	/**
 	 * Helper class for accessing capability properties on pointers.
 	 */
 	template<typename T>
@@ -390,12 +414,12 @@
 		 */
 		class PropertyProxyBase
 		{
+			protected:
 			/**
 			 * The capability that this proxy refers to.
 			 */
 			Capability &cap;
 
-			protected:
 			/**
 			 * Replaces the underlying capability
 			 */
@@ -521,6 +545,68 @@
 				set(__builtin_cheri_bounds_set(ptr(), bounds));
 				return *this;
 			}
+
+			private:
+			BoundsProxy &set_inexact_at_most_slow(size_t bounds)
+			{
+				ptraddr_t newBaseAddress = this->cap.address();
+
+				// The number of bits in CHERIoT's capability encoding's
+				// mantissa.  This is part of the capability encoding and
+				// so, ideally, wouldn't be hard coded here.
+				static constexpr size_t MantissaBits = 9;
+
+				// The maximum possible representable length given the new
+				// base is a full mantissa width of 1s followed by 0s with
+				// its least significant 1 aligned to the least significant
+				// 1 in the base address.
+				size_t maximumLength = ((1 << MantissaBits) - 1)
+				                       << __builtin_ctz(newBaseAddress);
+
+				// Ensure that the requested length is representable by
+				// making sure that it fits within a mantissa width,
+				// rounding down by dropping any lower bits.  This might be
+				// excessive by up to one bit position, because the
+				// representable alignment mask is designed to work with the
+				// rounding-up inexact bounds setting instruction.  As a result,
+				// we might not return the largest possible representable
+				// length, but we won't return a wildly too small one, either.
+				size_t alignedLength =
+				  bounds & representable_alignment_mask(bounds);
+
+				// Select the smaller of those two lengths.
+				bounds = std::min<size_t>(alignedLength, maximumLength);
+				*this  = bounds;
+				return *this;
+			}
+
+			public:
+			/**
+			 * Set the bounds to `length` if `length` is representable with the
+			 * current alignment of `buffer`. If not, then select a smaller
+			 * `length` that is representable.  Unlike set_inexact(), the
+			 * resulting base will always be the current address; that is, there
+			 * will be no padding below the current address.
+			 *
+			 * The caller must call .length() on the resulting capability to
+			 * determine the imposed bounds.
+			 *
+			 * See is_precise_range().
+			 */
+			__always_inline BoundsProxy &set_inexact_at_most(size_t bounds)
+			{
+				// Just try to set the requested bounds, first.  If that works,
+				// there's no need for bit-twiddling at all.
+				Capability p = ptr();
+				p.bounds()   = bounds;
+				if (p.is_valid())
+				{
+					set(static_cast<T *>(p));
+					return *this;
+				}
+
+				return set_inexact_at_most_slow(bounds);
+			}
 		};
 
 		/**
@@ -1020,30 +1106,6 @@
 	};
 
 	/**
-	 * Rounds `len` up to a CHERI representable length for the current
-	 * architecture.
-	 */
-	__always_inline inline size_t representable_length(size_t length)
-	{
-		return __builtin_cheri_round_representable_length(length);
-	}
-
-	/**
-	 * Returns the alignment mask required for a given length.
-	 */
-	__always_inline inline size_t representable_alignment_mask(size_t length)
-	{
-		return __builtin_cheri_representable_alignment_mask(length);
-	}
-
-	/// Can the range [base, base + size) be precisely covered by a capability?
-	inline bool is_precise_range(ptraddr_t base, size_t size)
-	{
-		return (base & ~representable_alignment_mask(size)) == 0 &&
-		       representable_length(size) == size;
-	}
-
-	/**
 	 * Concept that matches pointers.
 	 */
 	template<typename T>
@@ -1169,50 +1231,53 @@
 		 * No exception. This value is passed to the error handler after a
 		 * forced unwind in a called compartment.
 		 */
-		None = 0,
+		None = CheriCauseCodeNone,
 		/**
 		 * Attempted to use a capability outside its bounds.
 		 */
-		BoundsViolation = 1,
+		BoundsViolation = CheriCauseCodeBoundsViolation,
 		/**
 		 * Attempted to use an untagged capability to authorize something.
 		 */
-		TagViolation = 2,
+		TagViolation = CheriCauseCodeTagViolation,
 		/**
 		 * Attempted to use a sealed capability to authorize something.
 		 */
-		SealViolation = 3,
+		SealViolation = CheriCauseCodeSealViolation,
 		/**
 		 * Attempted to jump to a capability without `Permission::Execute`.
 		 */
-		PermitExecuteViolation = 0x11,
+		PermitExecuteViolation = CheriCauseCodePermitExecuteViolation,
 		/**
 		 * Attempted to load via a capability without `Permission::Load`.
 		 */
-		PermitLoadViolation = 0x12,
+		PermitLoadViolation = CheriCauseCodePermitLoadViolation,
 		/**
 		 * Attempted to store via a capability without `Permission::Store`.
 		 */
-		PermitStoreViolation = 0x13,
+		PermitStoreViolation = CheriCauseCodePermitStoreViolation,
 		/**
 		 * Attempted to store a tagged capability via a capability without
 		 * `Permission::LoadStoreCapability`.
 		 */
-		PermitStoreCapabilityViolation = 0x15,
+		PermitStoreCapabilityViolation =
+		  CheriCauseCodePermitStoreCapabilityViolation,
 		/**
 		 * Attempted to store a tagged capability without `Permission::Global`
 		 * via capability without `Permission::StoreLocal`.
 		 */
-		PermitStoreLocalCapabilityViolation = 0x16,
+		PermitStoreLocalCapabilityViolation =
+		  CheriCauseCodePermitStoreLocalCapabilityViolation,
 		/**
 		 * Attempted to access a restricted CSR or SCR with PCC without
 		 * `Permission::AccessSystemRegisters`.
 		 */
-		PermitAccessSystemRegistersViolation = 0x18,
+		PermitAccessSystemRegistersViolation =
+		  CheriCauseCodePermitAccessSystemRegistersViolation,
 		/**
 		 * Used to represent a value that has no valid meaning in hardware.
 		 */
-		Invalid = -1
+		Invalid = CheriCauseCodeInvalid,
 	};
 
 	/**
@@ -1226,84 +1291,84 @@
 		/**
 		 * The zero register, which always contains the `NULL` capability.
 		 */
-		CZR = 0x0,
+		CZR = CheriRegisterNumberCzr,
 		/**
 		 * `$c1` / `$cra` used by the ABI as the return address.
 		 * Not preserved across calls.
 		 */
-		CRA = 0x1,
+		CRA = CheriRegisterNumberCra,
 		/**
 		 * `$c2` / `$csp` used by the ABI as the stack pointer.
 		 * Preserved across calls.
 		 */
-		CSP = 0x2,
+		CSP = CheriRegisterNumberCsp,
 		/**
 		 * `$c3` / `$cgp` used by the ABI as the global pointer.
 		 * Not allocatable by the compiler, set by the switcher on compartment
 		 * entry.
 		 */
-		CGP = 0x3,
+		CGP = CheriRegisterNumberCgp,
 		/**
 		 * `$c4` / `$ctp` used by the ABI as the thread pointer.
 		 * Currently unused by the compiler.
 		 * Not preserved across compartment calls.
 		 */
-		CTP = 0x4,
+		CTP = CheriRegisterNumberCtp,
 		/**
 		 * `$c5` / `$ct0` used by the ABI as temporary register.
 		 * Not preserved across calls.
 		 */
-		CT0 = 0x5,
+		CT0 = CheriRegisterNumberCT0,
 		/**
 		 * `$c6` / `$ct1` used by the ABI as temporary register.
 		 * Not preserved across calls.
 		 */
-		CT1 = 0x6,
+		CT1 = CheriRegisterNumberCT1,
 		/**
 		 * `$c7` / `$ct2` used by the ABI as temporary register.
 		 * Not preserved across calls.
 		 */
-		CT2 = 0x7,
+		CT2 = CheriRegisterNumberCT2,
 		/**
 		 * `$c8` / `$cs0` used by the ABI as a callee-saved register.
 		 * Preserved across calls.
 		 */
-		CS0 = 0x8,
+		CS0 = CheriRegisterNumberCS0,
 		/**
 		 * `$c9` / `$cs1` used by the ABI as a callee-saved register.
 		 * Preserved across calls.
 		 */
-		CS1 = 0x9,
+		CS1 = CheriRegisterNumberCS1,
 		/**
 		 * `$c10` / `$ca0` used by the ABI as an argument register.
 		 * Not preserved across calls.
 		 */
-		CA0 = 0xa,
+		CA0 = CheriRegisterNumberCA0,
 		/**
 		 * `$c11` / `$ca1` used by the ABI as an argument register.
 		 * Not preserved across calls.
 		 */
-		CA1 = 0xb,
+		CA1 = CheriRegisterNumberCA1,
 		/**
 		 * `$c12` / `$ca2` used by the ABI as an argument register.
 		 * Not preserved across calls.
 		 */
-		CA2 = 0xc,
+		CA2 = CheriRegisterNumberCA2,
 		/**
 		 * `$c13` / `$ca3` used by the ABI as an argument register.
 		 * Not preserved across calls.
 		 */
-		CA3 = 0xd,
+		CA3 = CheriRegisterNumberCA3,
 		/**
 		 * `$c14` / `$ca4` used by the ABI as an argument register.
 		 * Not preserved across calls.
 		 */
-		CA4 = 0xe,
+		CA4 = CheriRegisterNumberCA4,
 		/**
 		 * `$c15` / `$ca5` used by the ABI as an argument register.
 		 * Not preserved across calls.
 		 */
-		CA5 = 0xf,
+		CA5 = CheriRegisterNumberCA5,
 		/**
 		 * The Program Counter Capability.
 		 *
@@ -1311,7 +1376,7 @@
 		 * address is that of the faulting instruction. Also used for accessing
 		 * read-only globals.
 		 */
-		PCC = 0x20,
+		PCC = CheriRegisterNumberPcc,
 		/**
 		 * Machine-mode Trap Code Capability.
 		 *
@@ -1320,7 +1385,7 @@
 		 * same semantics as the RISC-V `mtvec` CSR. Only accessible when PCC
 		 * has the AccessSystemRegisters permission.
 		 */
-		MTCC = 0x3c,
+		MTCC = CheriRegisterNumberMtcc,
 		/**
 		 * Machine-mode Tusted Data Capability.
 		 *
@@ -1329,25 +1394,25 @@
 		 * permission.  Use by the RTOS to store a capability to the trusted
 		 * stack.
 		 */
-		MTDC = 0x3d,
+		MTDC = CheriRegisterNumberMtdc,
 		/**
 		 * Machine-mode Scratch Capability. Special capabiltiy register that
 		 * contains the sealing root capability on boot. Only accessible when
 		 * PCC has the AccessSystemRegisters permission.
 		 */
-		MScratchC = 0x3e,
+		MScratchC = CheriRegisterNumberMScratchC,
 		/**
 		 * Machine-mode Exception Program Counter Capability. Special capability
 		 * register that contains the PCC of the faulting instruction on trap.
 		 * The address has the same semantics as the RISC-V `mepc` CSR. Only
 		 * accessible when PCC has the AccessSystemRegisters permission.
 		 */
-		MEPCC = 0x3f,
+		MEPCC = CheriRegisterNumberMepcc,
 		/**
 		 * Indicates a value that is not used by the hardware to refer to a
 		 * register.
 		 */
-		Invalid = -1
+		Invalid = CheriRegisterNumberInvalid,
 	};
 
 	/**
diff --git a/sdk/include/compartment-macros.h b/sdk/include/compartment-macros.h
index ef0a024..ed728f1 100644
--- a/sdk/include/compartment-macros.h
+++ b/sdk/include/compartment-macros.h
@@ -142,16 +142,6 @@
  */
 #define DEVICE_EXISTS(x) defined(DEVICE_EXISTS_##x)
 
-#define SEALING_CAP()                                                          \
-	({                                                                         \
-		void *ret;                                                             \
-		__asm("1:	"                                                            \
-		      "	auipcc		%0, %%cheriot_compartment_hi(__sealingkey)\n"          \
-		      "	clc			%0, %%cheriot_compartment_lo_i(1b)(%0)\n"                \
-		      : "=C"(ret));                                                    \
-		ret;                                                                   \
-	})
-
 /**
  * Helper macro, used by `STATIC_SEALING_TYPE`.  Do not use this directly, it
  * exists to avoid error-prone copying and pasting of the mangled name for a
diff --git a/sdk/include/compartment.h b/sdk/include/compartment.h
index 6113c83..00079dc 100644
--- a/sdk/include/compartment.h
+++ b/sdk/include/compartment.h
@@ -4,52 +4,18 @@
 #pragma once
 #include <cdefs.h>
 #include <compartment-macros.h>
+#include <stddef.h>
 #include <stdint.h>
 
 #ifdef __cplusplus
 #	include <cheri.hh>
-template<typename T>
-static inline CHERI::Capability<T> compart_seal(T *in)
-{
-	void *key = SEALING_CAP();
-
-	return CHERI::Capability{in}.seal(key);
-}
-
-template<typename T>
-static inline CHERI::Capability<T> compart_unseal(T *in)
-{
-	void *key = SEALING_CAP();
-
-	return CHERI::Capability{in}.unseal(key);
-}
-
-template<typename T>
-static inline auto compart_unseal(void *in)
-{
-	return compart_unseal(static_cast<T *>(in));
-}
-#else
-#	include <cheri-builtins.h>
-static inline void *compart_seal(void *in)
-{
-	void *key = SEALING_CAP();
-
-	return cseal(in, key);
-}
-
-static inline void *compart_unseal(void *in)
-{
-	void *key = SEALING_CAP();
-
-	return cunseal(in, key);
-}
 #endif
 
 /**
  * State for error handlers to use.
  *
- * Note: This structure should have the same layout as the register-save area.
+ * Note: This structure should have the same layout as the register-save area
+ * (that is, the initial sequence of a TrustedStack, up through ca5, inclusive).
  */
 struct ErrorState
 {
diff --git a/sdk/include/fail-simulator-on-error.h b/sdk/include/fail-simulator-on-error.h
index d26dceb..cad8bd7 100644
--- a/sdk/include/fail-simulator-on-error.h
+++ b/sdk/include/fail-simulator-on-error.h
@@ -42,56 +42,36 @@
 {
 	if (mcause == priv::MCAUSE_CHERI)
 	{
+		// An unexpected error -- log it and end the simulation with error.
+		// Note: handle CZR differently as `get_register_value` will return a
+		// nullptr which we cannot dereference.
+
 		auto [exceptionCode, registerNumber] =
 		  CHERI::extract_cheri_mtval(mtval);
-		// The thread entry point is called with a NULL return address so the
-		// cret at the end of the entry point function will trap if it is
-		// reached. We don't want to treat this as an error but thankfully we
-		// detect it quite specifically by checking for all of:
-		// 1) CHERI cause is tag violation
-		// 2) faulting register is CRA
-		// 3) value of CRA is NULL
-		// 4) we've reached the top of the thread's stack
-		CHERI::Capability stackCapability{
-		  frame->get_register_value<CHERI::RegisterNumber::CSP>()};
-		CHERI::Capability returnCapability{
-		  frame->get_register_value<CHERI::RegisterNumber::CRA>()};
-		// The top of the stack is 16 bytes above the stack pointer on entry,
-		// to provide space for unwind lists and so on.
-		if (registerNumber == CHERI::RegisterNumber::CRA &&
-		    returnCapability.address() == 0 &&
-		    exceptionCode == CHERI::CauseCode::TagViolation &&
-		    (stackCapability.top() - 16) == stackCapability.address())
-		{
-			// looks like thread exit -- just log it then ForceUnwind
-			DebugErrorHandler::log(
-			  "Thread exit CSP={}, PCC={}", stackCapability, frame->pcc);
-		}
-		else
-		{
-			// An unexpected error -- log it and end the simulation
-			// with error.  Note: handle CZR differently as
-			// `get_register_value` will return a nullptr which we
-			// cannot dereference.
-			DebugErrorHandler::log(
-			  "{} error at {} (return address: {}), with capability register "
-			  "{}: {}",
-			  exceptionCode,
-			  frame->pcc,
-			  frame->get_register_value<CHERI::RegisterNumber::CRA>(),
-			  registerNumber,
-			  registerNumber == CHERI::RegisterNumber::CZR
-			    ? nullptr
-			    : *frame->get_register_value(registerNumber));
-			simulation_exit(1);
-		}
+
+		DebugErrorHandler::log(
+		  "{} error at {} (return address: {}), with capability register "
+		  "{}: {}",
+		  exceptionCode,
+		  frame->pcc,
+		  frame->get_register_value<CHERI::RegisterNumber::CRA>(),
+		  registerNumber,
+		  registerNumber == CHERI::RegisterNumber::CZR
+		    ? nullptr
+		    : *frame->get_register_value(registerNumber));
 	}
 	else
 	{
 		// other error (e.g. __builtin_trap causes ReservedInstruciton)
 		// log and end simulation with error.
 		DebugErrorHandler::log("Unhandled error {} at {}", mcause, frame->pcc);
-		simulation_exit(1);
 	}
+
+	simulation_exit(1);
+	/*
+	 * simulation_exit may fail (say, we're not on a simulator or there isn't
+	 * enough stack space to invoke the function.  In that case, just fall back
+	 * to forcibly unwinding.
+	 */
 	return ErrorRecoveryBehaviour::ForceUnwind;
 }
diff --git a/sdk/include/platform/sunburst/platform-uart.hh b/sdk/include/platform/sunburst/platform-uart.hh
index a9acf85..09f217d 100644
--- a/sdk/include/platform/sunburst/platform-uart.hh
+++ b/sdk/include/platform/sunburst/platform-uart.hh
@@ -4,6 +4,10 @@
 #include_next <platform-uart.hh>
 #pragma pop_macro("CHERIOT_PLATFORM_CUSTOM_UART")
 
+#ifndef DEFAULT_UART_BAUD_RATE
+#	define DEFAULT_UART_BAUD_RATE 921'600
+#endif
+
 /**
  * OpenTitan UART
  *
@@ -128,6 +132,23 @@
 		ControlTransmitEnable = 1 << 0,
 	};
 
+	/// Status Register Fields
+	enum : uint32_t
+	{
+		/// Receive FIFO is empty.
+		StatusReceiveEmpty = 1 << 5,
+		/// Receive logic is idle.
+		StatusReceiveIdle = 1 << 4,
+		/// Transmit FIFO is empty and all bits have been transmitted.
+		StatusTransmitIdle = 1 << 3,
+		/// Transmit FIFO is empty; transmission may still be occurring.
+		StatusTransmitEmpty = 1 << 2,
+		/// Receive FIFO is full.
+		StatusReceiveFull = 1 << 1,
+		/// Transmit FIFO is full.
+		StatusTransmitFull = 1 << 0,
+	};
+
 	/// The encoding for different transmit watermark levels.
 	enum class TransmitWatermark
 	{
@@ -181,8 +202,8 @@
 	/// Clears the contents of the receive and transmit FIFOs.
 	void fifos_clear() volatile
 	{
-		fifoCtrl = (fifoCtrl & ~0b11) | FifoControlTransmitReset |
-		           FifoControlReceiveReset;
+		fifoCtrl =
+		  fifoCtrl | FifoControlTransmitReset | FifoControlReceiveReset;
 	}
 
 	/**
@@ -204,7 +225,7 @@
 	 */
 	void receive_watermark(ReceiveWatermark level) volatile
 	{
-		fifoCtrl = static_cast<uint32_t>(level) << 5 | (fifoCtrl & 0b11100011);
+		fifoCtrl = static_cast<uint32_t>(level) << 2 | (fifoCtrl & 0b11100011);
 	}
 
 	/// Enable the given interrupt.
@@ -219,7 +240,7 @@
 		interruptEnable = interruptEnable & ~interrupt;
 	}
 
-	void init(unsigned baudRate = 115'200) volatile
+	void init(unsigned baudRate = DEFAULT_UART_BAUD_RATE) volatile
 	{
 		// Nco = 2^20 * baud rate / cpu frequency
 		const uint32_t Nco =
@@ -240,12 +261,12 @@
 
 	bool can_write() volatile
 	{
-		return transmit_fifo_level() < 32;
+		return !(status & StatusTransmitFull);
 	}
 
 	bool can_read() volatile
 	{
-		return receive_fifo_level() > 0;
+		return !(status & StatusReceiveEmpty);
 	}
 
 	/**
diff --git a/sdk/include/platform/sunburst/platform-usbdev.hh b/sdk/include/platform/sunburst/platform-usbdev.hh
new file mode 100644
index 0000000..1a279bc
--- /dev/null
+++ b/sdk/include/platform/sunburst/platform-usbdev.hh
@@ -0,0 +1,681 @@
+// SPDX-FileCopyrightText: CHERIoT contributors
+// SPDX-License-Identifier: Apache-2.0
+
+#pragma once
+#include <cdefs.h>
+#include <optional>
+#include <stdint.h>
+#include <utils.hh>
+
+/**
+ * A driver for OpenTitan USB Device, which is used in the Sonata system.
+ *
+ * This peripheral's source and documentation can be found at:
+ * https://github.com/lowRISC/opentitan/tree/ab878b5d3578939a04db72d4ed966a56a869b2ed/hw/ip/usbdev
+ *
+ * With rendered register documentation served at:
+ * https://opentitan.org/book/hw/ip/usbdev/doc/registers.html
+ *
+ * An incredibly brief overview of how the USB device and it's buffers:
+ * Data packet ingress and egress goes via a pool of 64 byte buffers living
+ * in a 2kB SRAM packet buffer, which is accessable as a large MMIO region.
+ * The software manages these buffers using buffer IDs as references.
+ * IDs are pushed or popped into different FIFOs by either the software or
+ * device depending on whether they contain a packet to be sent, are available
+ * for a packet to be received into them, or contain a packet that has been
+ * received.
+ *
+ * See https://opentitan.org/book/hw/ip/usbdev/doc/programmers_guide.html for
+ * more information.
+ */
+class OpenTitanUsbdev : private utils::NoCopyNoMove
+{
+	public:
+	/// Supported sizes for the USB Device.
+	static constexpr uint8_t MaxPacketLength = 64u;
+	static constexpr uint8_t BufferCount     = 32u;
+	static constexpr uint8_t MaxEndpoints    = 12u;
+
+	/**
+	 * The offset from the start of the USB Device MMIO region at which
+	 * packet buffer memory begins.
+	 */
+	static constexpr uint32_t BufferStartAddress = 0x800u;
+
+	/// Device Registers
+	uint32_t interruptState;
+	uint32_t interruptEnable;
+	uint32_t interruptTest;
+	uint32_t alertTest;
+	uint32_t usbControl;
+	uint32_t endpointOutEnable;
+	uint32_t endpointInEnable;
+	uint32_t usbStatus;
+	uint32_t availableOutBuffer;
+	uint32_t availableSetupBuffer;
+	uint32_t receiveBuffer;
+	/// Register to enable receive SETUP transactions
+	uint32_t receiveEnableSetup;
+	/// Register to enable receive OUT transactions
+	uint32_t receiveEnableOut;
+	/// Register to set NAK (Not/Negated Acknowledge) after OUT transactions
+	uint32_t setNotAcknowledgeOut;
+	/// Register showing ACK receival to indicate a successful IN send
+	uint32_t inSent;
+	/// Registers for controlling the stalling of OUT and IN endpoints
+	uint32_t outStall;
+	uint32_t inStall;
+	/**
+	 * IN transaction configuration registers. There is one register per
+	 * endpoint for the USB device.
+	 */
+	uint32_t configIn[MaxEndpoints];
+	/**
+	 * Registers for configuring which endpoints should be treated as
+	 * isochronous endpoints. This means that if the corresponding bit is set,
+	 * then that no handshake packet will be sent for an OUT/IN transaction on
+	 * that endpoint.
+	 */
+	uint32_t outIsochronous;
+	uint32_t inIsochronous;
+	/// Registers for configuring if endpoints data toggle on transactions
+	uint32_t outDataToggle;
+	uint32_t inDataToggle;
+
+	private:
+	/**
+	 * Registers to sense/drive the USB PHY pins. That is, these registers can
+	 * be used to respectively read out the state of the USB device inputs and
+	 * outputs, or to control the inputs and outputs from software. These
+	 * registers are kept private as they are intended to be used for debugging
+	 * purposes or during chip testing, and not in actual software.
+	 */
+	[[maybe_unused]] uint32_t phyPinsSense;
+	[[maybe_unused]] uint32_t phyPinsDrive;
+
+	public:
+	/// Config register for the USB PHY pins.
+	uint32_t phyConfig;
+
+	/// Interrupt definitions for OpenTitan's USB Device.
+	enum class UsbdevInterrupt : uint32_t
+	{
+		/// Interrupt asserted whilst the receive FIFO (buffer) is not empty.
+		PacketReceived = 1u << 0,
+		/**
+		 * Interrupt asserted when a packet was sent as part of an IN
+		 * transaction, but not cleared from the `inSent` register.
+		 */
+		PacketSent = 1u << 1,
+		/**
+		 * Interrupt raised when VBUS (power supply) is lost, i.e. the link to
+		 * the USB host controller has been disconnected.
+		 */
+		Disconnected = 1u << 2,
+		/**
+		 * Interrupt raised when the link is active, but a Start of Frame (SOF)
+		 * packet has not been received within a given timeout threshold, which
+		 * is set to 4.096 milliseconds.
+		 */
+		HostLost = 1u << 3,
+		/**
+		 * Interrupt raised when a Bus Reset condition is indicated on the link
+		 * by the link being held in an SE0 state (Single Ended Zero, both lines
+		 * being pulled low) for longer than 3 microseconds.
+		 */
+		LinkReset = 1u << 4,
+		/**
+		 * Interrupt raised when the link has entered the suspend state, due to
+		 * being idle for more than 3 milliseconds.
+		 */
+		LinkSuspend = 1u << 5,
+		///  Interrupt raised on link transition from suspended to non-idle.
+		LinkResume = 1u << 6,
+		/// Interrupt asserted whilst the Available OUT buffer is empty.
+		AvailableOutEmpty = 1u << 7,
+		///  Interrupt asserted whilst the Receive buffer is full.
+		ReceiveFull = 1u << 8,
+		/**
+		 * Interrupt raised when the Available OUT buffer or the Available SETUP
+		 * buffer overflows.
+		 */
+		AvailableBufferOverflow = 1u << 9,
+		///  Interrupt raised when an error occurs during an IN transaction.
+		LinkInError = 1u << 10,
+		/**
+		 * Interrupt raised when a CRC (cyclic redundancy check) error occurs on
+		 * a received packet; i.e. there was an error in transmission.
+		 */
+		RedundancyCheckError = 1u << 11,
+		///  Interrupt raised when an invalid Packet Identifier is received.
+		PacketIdentifierError = 1u << 12,
+		///  Interrupt raised when a bit stuffing violation is detected.
+		BitstuffingError = 1u << 13,
+		/**
+		 * Interrupt raised when the USB frame number is updated with a valid
+		 * SOF (Start of Frame) packet.
+		 */
+		FrameUpdated = 1u << 14,
+		///  Interrupt raised when VBUS (power supply) is detected.
+		Powered = 1u << 15,
+		///  Interrupt raised when an error occurs during an OUT transaction.
+		LinkOutError = 1u << 16,
+		///  Interrupt asserted whilst the Available SETUP buffer is empty.
+		AvailableSetupEmpty = 1u << 17,
+	};
+
+	/**
+	 * Definitions of fields (and their locations) for the USB Control register
+	 * (offset 0x10).
+	 *
+	 * https://opentitan.org/book/hw/ip/usbdev/doc/registers.html#usbctrl
+	 */
+	enum class UsbControlField : uint32_t
+	{
+		Enable           = 1u << 0,
+		ResumeLinkActive = 1u << 1,
+		DeviceAddress    = 0x7Fu << 16,
+	};
+
+	/**
+	 * Definitions of fields (and their locations) for the USB Status register
+	 * (offset 0x1c).
+	 *
+	 * https://opentitan.org/book/hw/ip/usbdev/doc/registers.html#usbstat
+	 */
+	enum class UsbStatusField : uint32_t
+	{
+		Frame               = 0x7FFu << 0,
+		HostLost            = 1u << 11,
+		LinkState           = 0x7u << 12,
+		Sense               = 1u << 15,
+		AvailableOutDepth   = 0xFu << 16,
+		AvailableSetupDepth = 0x7u << 20,
+		AvailableOutFull    = 1u << 23,
+		ReceiveDepth        = 0xFu << 24,
+		AvailableSetupFull  = 1u << 30,
+		ReceiveEmpty        = 1u << 31,
+	};
+
+	/**
+	 * Definitions of fields (and their locations) for the Receive FIFO
+	 * buffer register (offset 0x28).
+	 *
+	 * https://opentitan.org/book/hw/ip/usbdev/doc/registers.html#rxfifo
+	 */
+	enum class ReceiveBufferField : uint32_t
+	{
+		BufferId   = 0x1Fu << 0,
+		Size       = 0x7Fu << 8,
+		Setup      = 1u << 19,
+		EndpointId = 0xFu << 20,
+	};
+
+	/**
+	 * Definitions of fields (and their locations) for a Config In register
+	 * (where there is one such register for each endpoint). These are
+	 * the registers with offsets 0x44 up to (and not including) 0x74.
+	 *
+	 * https://opentitan.org/book/hw/ip/usbdev/doc/registers.html#configin
+	 */
+	enum class ConfigInField : uint32_t
+	{
+		BufferId = 0x1Fu << 0,
+		Size     = 0x7Fu << 8,
+		Sending  = 1u << 29,
+		Pending  = 1u << 30,
+		Ready    = 1u << 31,
+	};
+
+	/**
+	 * Definitions of fields (and their locations) for the PHY Config
+	 * Register (offset 0x8c).
+	 *
+	 * https://opentitan.org/book/hw/ip/usbdev/doc/registers.html#phy_config
+	 */
+	enum class PhyConfigField : uint32_t
+	{
+		UseDifferentialReceiver = 1u << 0,
+		//  Other PHY Configuration fields are omitted.
+	};
+
+	/**
+	 * Ensure that the Available OUT and Available SETUP buffers are kept
+	 * supplied with buffers for packet reception.
+	 *
+	 * @param bufferBitmap A bitmap of the buffers that are not currently
+	 * committed (where 1 corresponds to not in use).
+	 * @returns The updated bitmap after supplying buffers.
+	 */
+	[[nodiscard]] uint64_t supply_buffers(uint64_t bufferBitmap) volatile
+	{
+		constexpr uint32_t SetupFullBit =
+		  uint32_t(UsbStatusField::AvailableSetupFull);
+		constexpr uint32_t OutFullBit =
+		  uint32_t(UsbStatusField::AvailableOutFull);
+
+		for (uint8_t index = 0; index < BufferCount; index++)
+		{
+			const uint32_t Buffer = (1u << index);
+			if (!(bufferBitmap & Buffer))
+			{
+				continue; // Skip buffers that are not available
+			}
+
+			// If a buffer is available, and either Available SETUP or OUT are
+			// not yet full, then commit that buffer and mark it as in use.
+			if (usbStatus & SetupFullBit)
+			{
+				if (usbStatus & OutFullBit)
+				{
+					break; // Both are full - stop trying to supply buffers.
+				}
+				availableOutBuffer = index;
+			}
+			else
+			{
+				availableSetupBuffer = index;
+			}
+			bufferBitmap &= ~Buffer;
+		}
+		return bufferBitmap;
+	}
+
+	/**
+	 * Enable a specified interrupt / interrupts.
+	 */
+	void interrupt_enable(UsbdevInterrupt interrupt) volatile
+	{
+		interruptEnable = interruptEnable | uint32_t(interrupt);
+	}
+
+	/**
+	 * Disable a specified interrupt / interrupts.
+	 */
+	void interrupt_disable(UsbdevInterrupt interrupt) volatile
+	{
+		interruptEnable = interruptEnable & ~uint32_t(interrupt);
+	}
+
+	/**
+	 * Initialise the USB device, ensuring that packet buffers are available for
+	 * reception and that the PHY has been appropriately configured. Note that
+	 * at this stage, endpoints have not been configured and the device has not
+	 * been connected to the USB.
+	 *
+	 * @param bufferBitmap An out-parameter, to initialise a bitmap of the
+	 * buffers that are not currently commited (1 corresponds to not in use).
+	 *
+	 * @returns 0 if initialisation is sucessful, and non-zero otherwise.
+	 */
+	[[nodiscard]] int init(uint64_t &bufferBitmap) volatile
+	{
+		bufferBitmap = supply_buffers((uint64_t(1u) << BufferCount) - 1u);
+		phyConfig    = uint32_t(PhyConfigField::UseDifferentialReceiver);
+		return 0;
+	}
+
+	/**
+	 * Set up the configuration of an OUT endpoint for the USB device.
+	 *
+	 * @param endpointId The ID of the OUT endpoint to configure.
+	 * @param enabled Whether the OUT endpoint should be enabled or not.
+	 * @param setup Whether SETUP transactions should be enabled for the
+	 * endpoint.
+	 * @param isochronous Whether the endpoint should operate isochronously or
+	 * non-isochronously.
+	 *
+	 * @returns 0 if configuration is successful, and non-zero otherwise.
+	 */
+	[[nodiscard]] int out_endpoint_configure(uint8_t endpointId,
+	                                         bool    enabled,
+	                                         bool    setup,
+	                                         bool    isochronous) volatile
+	{
+		if (endpointId >= MaxEndpoints)
+		{
+			return -1;
+		}
+		const uint32_t Mask = 1u << endpointId;
+		endpointOutEnable = (endpointOutEnable & ~Mask) | (enabled ? Mask : 0u);
+		outIsochronous = (outIsochronous & ~Mask) | (isochronous ? Mask : 0u);
+		receiveEnableSetup = (receiveEnableSetup & ~Mask) | (setup ? Mask : 0u);
+		receiveEnableOut   = (receiveEnableOut & ~Mask) | (enabled ? Mask : 0u);
+		return 0;
+	}
+
+	/**
+	 * Set up the configuration of an IN endpoint for the USB device.
+	 *
+	 * @param endpointId The ID of the IN endpoint to configure
+	 * @param enabled Whether the IN endpoint should be enabled or not.
+	 * @param isochronous Whether the endpoint should operate isochronously or
+	 * non-isochronously.
+	 *
+	 * @returns 0 if configuration is successful, and non-zero otherwise.
+	 */
+	[[nodiscard]] int in_endpoint_configure(uint8_t endpointId,
+	                                        bool    enabled,
+	                                        bool    isochronous) volatile
+	{
+		if (endpointId >= MaxEndpoints)
+		{
+			return -1;
+		}
+		const uint32_t Mask = 1u << endpointId;
+		endpointInEnable = (endpointInEnable & ~Mask) | (enabled ? Mask : 0u);
+		inIsochronous    = (inIsochronous & ~Mask) | (isochronous ? Mask : 0u);
+		return 0;
+	}
+
+	/**
+	 * Set the STALL state of a specified endpoint pair (both IN and OUT).
+	 *
+	 * @param endpointId The ID of the endpoint pair to modify.
+	 * @param stalling Whether the endpoints are stalling or not.
+	 *
+	 * @returns 0 if successful, and non-zero otherwise.
+	 */
+	[[nodiscard]] int endpoint_stalling_set(uint8_t endpointId,
+	                                        bool    stalling) volatile
+	{
+		if (endpointId >= MaxEndpoints)
+		{
+			return -1;
+		}
+		const uint32_t Mask = 1u << endpointId;
+		outStall            = (outStall & ~Mask) | (stalling ? Mask : 0u);
+		inStall             = (inStall & ~Mask) | (stalling ? Mask : 0u);
+		return 0;
+	}
+
+	/**
+	 * Connect the device to the USB, indicating its presence to the USB host
+	 * controller. Endpoints must already have been configured at this point
+	 * because traffic may be received imminently.
+	 *
+	 * @returns 0 if successful, and non-zero otherwise.
+	 * @returns -1 if endpoint 0 isn't enabled,
+	 *             suggesting the endpoints haven't been configured.
+	 */
+	[[nodiscard]] int connect() volatile
+	{
+		if (!(endpointInEnable & endpointOutEnable & 0b1))
+		{
+			return -1;
+		}
+		usbControl = usbControl | uint32_t(UsbControlField::Enable);
+		return 0;
+	}
+
+	/**
+	 * Disconnect the device from the USB.
+	 *
+	 * @returns 0 if successful, and non-zero otherwise.
+	 */
+	void disconnect() volatile
+	{
+		usbControl = usbControl & ~uint32_t(UsbControlField::Enable);
+	}
+
+	/**
+	 * Check whether the USB device is connected (i.e. pullup enabled).
+	 *
+	 * @returns True to indicate it is connected, and false otherwise.
+	 */
+	[[nodiscard]] bool connected() volatile
+	{
+		return (usbControl & uint32_t(UsbControlField::Enable));
+	}
+
+	/**
+	 * Set the device address on the USB; this address will have been supplied
+	 * by the USB host controller in the standard `SET_ADDRESS` Control
+	 * Transfer.
+	 *
+	 * @param address The device address to set on the USB.
+	 *
+	 * @returns 0 if successful, and non-zero otherwise.
+	 */
+	[[nodiscard]] int device_address_set(uint8_t address) volatile
+	{
+		if (address >= 0x80)
+		{
+			return -1; // Device addresses are only 7 bits long.
+		}
+		constexpr uint32_t Mask = uint32_t(UsbControlField::DeviceAddress);
+		usbControl              = (usbControl & ~Mask) | (address << 16);
+		return 0;
+	}
+
+	/**
+	 * Check and retrieve the endpoint and buffer numbers of a
+	 * recently-collected IN data packet. The caller is responsible for reusing
+	 * or releasing the buffer.
+	 *
+	 * @param endpointId An out-parameter, to which the ID of the endpoint for
+	 * a recently-collected IN data packet will be written.
+	 * @param bufferId An out-parameter, to which the ID of the buffer for a
+	 * recently-collected IN data packet will be written.
+	 *
+	 * @returns 0 if successful, and non-zero otherwise.
+	 */
+	[[nodiscard]] int retrieve_collected_packet(uint8_t &endpointId,
+	                                            uint8_t &bufferId) volatile
+	{
+		constexpr uint32_t BufferIdMask = uint32_t(ConfigInField::BufferId);
+		uint32_t           sent         = inSent;
+
+		// Clear the first encountered packet sent indication.
+		for (endpointId = 0; endpointId < MaxEndpoints; endpointId++)
+		{
+			const uint32_t EndpointBit = 1u << endpointId;
+			if (sent & EndpointBit)
+			{
+				// Clear the `in_sent` bit for this specific endpoint, and
+				// indicate which buffer has been released.
+				inSent   = EndpointBit;
+				bufferId = (configIn[endpointId] & BufferIdMask);
+				return 0;
+			}
+		}
+
+		// If no packet sent indications were found, then fail.
+		return -1;
+	}
+
+	/**
+	 * Present a packet on the specified IN endpoint for collection by the USB
+	 * host controller.
+	 *
+	 * @param bufferId The buffer to use to store the packet.
+	 * @param endpointId The IN endpoint used to send the packet.
+	 * @param data The packet to be transmitted.
+	 * @param size The size of the packet.
+	 */
+	void packet_send(uint8_t         bufferId,
+	                 uint8_t         endpointId,
+	                 const uint32_t *data,
+	                 uint8_t         size) volatile
+	{
+		// Transmission of zero length packets is common over USB
+		if (size > 0)
+		{
+			usbdev_transfer(buffer(bufferId), data, size, true);
+		}
+
+		constexpr uint32_t ReadyBit = uint32_t(ConfigInField::Ready);
+		configIn[endpointId]        = bufferId | (size << 8);
+		configIn[endpointId]        = configIn[endpointId] | ReadyBit;
+	}
+
+	/// The information associated with a received packet
+	struct ReceiveBufferInfo
+	{
+		uint32_t info;
+		/// The endpoint ID the received packet was received on
+		constexpr uint8_t endpoint_id()
+		{
+			return (info & uint32_t(ReceiveBufferField::EndpointId)) >> 20;
+		}
+		/// The size of the received packet
+		constexpr uint16_t size()
+		{
+			return (info & uint32_t(ReceiveBufferField::Size)) >> 8;
+		}
+		/// Whether the received packet was a setup packet
+		constexpr bool is_setup()
+		{
+			return (info & uint32_t(ReceiveBufferField::Setup)) != 0;
+		}
+		/// The buffer ID used to store the received packet
+		constexpr uint8_t buffer_id()
+		{
+			return (info & uint32_t(ReceiveBufferField::BufferId)) >> 0;
+		}
+	};
+
+	/**
+	 * If a packet has been received, removes the packet's buffer from the
+	 * receive FIFO giving it's information and ownership to the user.
+	 *
+	 * `packet_data_get` can be used to retrieve the packet's data.
+	 *
+	 * @returns Information about the received packet, if a packet had been
+	 * received.
+	 */
+	[[nodiscard]] std::optional<ReceiveBufferInfo> packet_take() volatile
+	{
+		if (!(usbStatus & uint32_t(UsbStatusField::ReceiveDepth)))
+		{
+			return {}; // No packets received
+		}
+		return ReceiveBufferInfo{receiveBuffer};
+	}
+
+	/**
+	 * Retrieves the data from a buffer containing a received packet.
+	 *
+	 * @param destination A destination buffer to read the packet's data into.
+	 */
+	void packet_data_get(ReceiveBufferInfo bufferInfo,
+	                     uint32_t         *destination) volatile
+	{
+		const auto [id, size] =
+		  std::pair{bufferInfo.buffer_id(), bufferInfo.size()};
+		// Reception of Zero Length Packets occurs in the Status Stage of IN
+		// Control Transfers.
+		if (size > 0)
+		{
+			usbdev_transfer(destination, buffer(id), size, false);
+		}
+	}
+
+	private:
+	/**
+	 * Return a pointer to the given offset within the USB device register
+	 * space; this is used to access the packet buffer memory.
+	 *
+	 * @param bufferId The buffer number to access the packet buffer memory for
+	 *
+	 * @returns A pointer to the buffer's memory.
+	 */
+	uint32_t *buffer(uint8_t bufferId) volatile
+	{
+		const uint32_t Offset = BufferStartAddress + bufferId * MaxPacketLength;
+		const uintptr_t Address = reinterpret_cast<uintptr_t>(this) + Offset;
+		return const_cast<uint32_t *>(reinterpret_cast<uint32_t *>(Address));
+	}
+
+	/**
+	 * Perform a transfer to or from packet buffer memory. This function is
+	 * hand-optimised to perform a faster, unrolled, word-based data transfer
+	 * for efficiency.
+	 *
+	 * @param destination A pointer to transfer the source data to.
+	 * @param source A pointer to the data to be transferred.
+	 * @param size The size of the data pointed to by `source`.
+	 * @param toDevice True if the transfer is to the device (e.g. when sending
+	 * a packet), and False if not (e.g. when receiving a packet).
+	 */
+	static void usbdev_transfer(uint32_t       *destination,
+	                            const uint32_t *source,
+	                            uint8_t         size,
+	                            bool            toDevice)
+	{
+		// Unroll word transfer. Each word transfer is 4 bytes, so we must round
+		// to the closest multiple of (4 * words) when unrolling.
+		constexpr uint8_t  UnrollFactor = 4u;
+		constexpr uint32_t UnrollMask   = (UnrollFactor * 4u) - 1;
+
+		// Round down to the previous multiple for unrolling
+		const uint32_t  UnrollSize = (size & ~UnrollMask);
+		const uint32_t *sourceEnd  = reinterpret_cast<uint32_t *>(
+          reinterpret_cast<uintptr_t>(source) + UnrollSize);
+
+		// This is manulally unrolled for two reasons:
+		// 1. We can't do partial writes to the USB packet buffer,
+		//    which memcpy will attempt and causes a BUS fault.
+		// 2. In the sonata system at the time of writing,
+		//    the core clock is 40MHz compared to the USB device's 48MHz.
+		//    This approach was found to be significantly faster than when
+		//    left to compiler to optimisation.
+		//
+		// Ensure the unrolling here matches `UnrollFactor`.
+		while (source < sourceEnd)
+		{
+			destination[0] = source[0];
+			destination[1] = source[1];
+			destination[2] = source[2];
+			destination[3] = source[3];
+			destination += UnrollFactor;
+			source += UnrollFactor;
+		}
+
+		// Copy the remaining whole words.
+		for (size &= UnrollMask; size >= UnrollFactor; size -= UnrollFactor)
+		{
+			*destination++ = *source++;
+		}
+		if (size == 0)
+		{
+			return;
+		}
+
+		// Copy trailing tail bytes, as USBDEV only supports 32-bit accesses.
+		if (toDevice)
+		{
+			// Collect final bytes into a word.
+			const volatile uint8_t *trailingBytes =
+			  reinterpret_cast<const volatile uint8_t *>(source);
+			uint32_t partialWord = trailingBytes[0];
+			if (size > 1)
+			{
+				partialWord |= trailingBytes[1] << 8;
+			}
+			if (size > 2)
+			{
+				partialWord |= trailingBytes[2] << 16;
+			}
+			// Write the final word to the device.
+			*destination = partialWord;
+		}
+		else
+		{
+			volatile uint8_t *destinationBytes =
+			  reinterpret_cast<volatile uint8_t *>(destination);
+			// Collect the final word from the device.
+			const uint32_t TrailingBytes = *source;
+			// Unpack it into final bytes.
+			destinationBytes[0] = static_cast<uint8_t>(TrailingBytes);
+			if (size > 1)
+			{
+				destinationBytes[1] = static_cast<uint8_t>(TrailingBytes >> 8);
+			}
+			if (size > 2)
+			{
+				destinationBytes[2] = static_cast<uint8_t>(TrailingBytes >> 16);
+			}
+		}
+	}
+};
diff --git a/sdk/include/priv/riscv.h b/sdk/include/priv/riscv.h
index d5c616e..d8cc51c 100644
--- a/sdk/include/priv/riscv.h
+++ b/sdk/include/priv/riscv.h
@@ -75,6 +75,7 @@
 	constexpr size_t MCAUSE_LOAD_PAGE_FAULT     = 13;
 	constexpr size_t MCAUSE_STORE_PAGE_FAULT    = 15;
 	constexpr size_t MCAUSE_THREAD_EXIT         = 24;
+	constexpr size_t MCAUSE_THREAD_INTERRUPT    = 25;
 	constexpr size_t MCAUSE_CHERI               = 28;
 
 	constexpr size_t MSTATUS_UIE = (1 << 0);
diff --git a/sdk/include/queue.h b/sdk/include/queue.h
index dc16e72..68743da 100644
--- a/sdk/include/queue.h
+++ b/sdk/include/queue.h
@@ -31,50 +31,71 @@
 #include <timeout.h>
 
 /**
- * A handle to a queue endpoint.
+ * Structure representing a queue.  This structure represents the queue
+ * metadata, the buffer is stored at the end.
  *
- * Dropping permissions can make this a receive-only or a send-only handle.
+ * A queue is a ring buffer of fixed-sized elements with a producer and consumer
+ * counter.
  */
-struct QueueHandle
+struct MessageQueue
 {
 	/**
-	 * The size of one element in this queue.
+	 * The size of one element in this queue.  This should not be modified after
+	 * construction.
 	 */
 	size_t elementSize;
 	/**
-	 * The size of the queue.
+	 * The size of the queue.  This should not be modified after construction.
 	 */
 	size_t queueSize;
 	/**
-	 * The buffer used for storing queue elements.
-	 */
-	void *buffer;
-	/**
 	 * The producer counter.
 	 */
-	_Atomic(uint32_t) *producer;
+	_Atomic(uint32_t) producer;
 	/**
 	 * The consumer counter.
 	 */
-	_Atomic(uint32_t) *consumer;
+	_Atomic(uint32_t) consumer;
+#ifdef __cplusplus
+	MessageQueue(size_t elementSize, size_t queueSize)
+	  : elementSize(elementSize), queueSize(queueSize)
+	{
+	}
+#endif
 };
 
+_Static_assert(sizeof(struct MessageQueue) % sizeof(void *) == 0,
+               "MessageQueue structure must end correctly aligned for storing "
+               "capabilities.");
+
 __BEGIN_DECLS
 
 /**
+ * Returns the allocation size needed for a queue with the specified number and
+ * size of elements.  This can be used to statically allocate queues.
+ *
+ * Returns the allocation size on success, or `-EINVAL` if the arguments would
+ * cause an overflow.
+ */
+ssize_t __cheri_libcall queue_allocation_size(size_t elementSize,
+                                              size_t elementCount);
+
+/**
  * Allocates space for a queue using `heapCapability` and stores a handle to it
- * via `outQueue`.  The underlying allocation (which is necessary to free the
- * queue) is returned via `outAllocation`.
+ * via `outQueue`.
  *
  * The queue is has space for `elementCount` entries.  Each entry is a fixed
  * size, `elementSize` bytes.
+ *
+ * Returns 0 on success, `-ENOMEM` on allocation failure, and `-EINVAL` if the
+ * arguments are invalid (for example, if the requested number of elements
+ * multiplied by the element size would overflow).
  */
-int __cheri_libcall queue_create(Timeout            *timeout,
-                                 struct SObjStruct  *heapCapability,
-                                 struct QueueHandle *outQueue,
-                                 void              **outAllocation,
-                                 size_t              elementSize,
-                                 size_t              elementCount);
+int __cheri_libcall queue_create(Timeout              *timeout,
+                                 struct SObjStruct    *heapCapability,
+                                 struct MessageQueue **outQueue,
+                                 size_t                elementSize,
+                                 size_t                elementCount);
 
 /**
  * Destroys a queue. This wakes up all threads waiting to produce or consume,
@@ -87,29 +108,8 @@
  * Returns 0 on success. On failure, returns `-EPERM` if the queue handle is
  * restricted (see comment above).
  */
-int __cheri_libcall queue_destroy(struct SObjStruct  *heapCapability,
-                                  struct QueueHandle *handle);
-
-/**
- * Convert a queue handle returned from `queue_create` into one that can be
- * used *only* for receiving.
- *
- * Note: This is primarily defence in depth.  A malicious holder of this queue
- * handle can still set the consumer counter to invalid values.
- */
-struct QueueHandle __cheri_libcall
-queue_make_receive_handle(struct QueueHandle handle);
-
-/**
- * Convert a queue handle returned from `queue_create` into one that can be
- * used *only* for sending.
- *
- * Note: This is primarily defence in depth.  A malicious holder of this queue
- * handle can still set the producer counter to invalid values and overwrite
- * arbitrary queue locations.
- */
-struct QueueHandle __cheri_libcall
-queue_make_send_handle(struct QueueHandle handle);
+int __cheri_libcall queue_destroy(struct SObjStruct   *heapCapability,
+                                  struct MessageQueue *handle);
 
 /**
  * Send a message to the queue specified by `handle`.  This expects to be able
@@ -122,9 +122,9 @@
  * This expected to be called with a valid queue handle.  It does not validate
  * that this is correct.  It uses `safe_memcpy` and so will check the buffer.
  */
-int __cheri_libcall queue_send(Timeout            *timeout,
-                               struct QueueHandle *handle,
-                               const void         *src);
+int __cheri_libcall queue_send(Timeout             *timeout,
+                               struct MessageQueue *handle,
+                               const void          *src);
 
 /**
  * Receive a message over a queue specified by `handle`.  This expects to be
@@ -135,9 +135,9 @@
  * Returns 0 on success, `-ETIMEOUT` if the timeout was exhausted, `-EINVAL` on
  * invalid arguments.
  */
-int __cheri_libcall queue_receive(Timeout            *timeout,
-                                  struct QueueHandle *handle,
-                                  void               *dst);
+int __cheri_libcall queue_receive(Timeout             *timeout,
+                                  struct MessageQueue *handle,
+                                  void                *dst);
 
 /**
  * Returns the number of items in the queue specified by `handle` via `items`.
@@ -150,27 +150,28 @@
  * may change in between the return of this function and the caller acting on
  * the result.
  */
-int __cheri_libcall queue_items_remaining(struct QueueHandle *handle,
-                                          size_t             *items);
+int __cheri_libcall queue_items_remaining(struct MessageQueue *handle,
+                                          size_t              *items);
 
 /**
  * Allocate a new message queue that is managed by the message queue
- * compartment.  This is returned as two sealed pointers to send and receive
- * ends of the queue.
+ * compartment.  The resulting queue handle (returned in `outQueue`) is a
+ * sealed capability to a queue that can be used for both sending and
+ * receiving.
  */
 int __cheri_compartment("message_queue")
   queue_create_sealed(Timeout            *timeout,
                       struct SObjStruct  *heapCapability,
-                      struct SObjStruct **outQueueSend,
-                      struct SObjStruct **outQueReceive,
+                      struct SObjStruct **outQueue,
                       size_t              elementSize,
                       size_t              elementCount);
 
 /**
- * Destroy a queue using a sealed queue endpoint handle.  The queue is not
- * actually freed until *both* endpoints are destroyed, which means that you
- * can safely call this from the sending end without the receiving end losing
- * access to messages held in the queue.
+ * Destroy a queue handle.  If this is called on a restricted endpoint
+ * (returned from `queue_receive_handle_create_sealed` or
+ * `queue_send_handle_create_sealed`), this frees only the handle.  If called
+ * with the queue handle returned from `queue_create_sealed`, this will destroy
+ * the queue.
  */
 int __cheri_compartment("message_queue")
   queue_destroy_sealed(Timeout           *timeout,
@@ -215,7 +216,7 @@
  */
 void __cheri_libcall
 multiwaiter_queue_receive_init(struct EventWaiterSource *source,
-                               struct QueueHandle       *handle);
+                               struct MessageQueue      *handle);
 
 /**
  * Initialise an event waiter source so that it will wait for the queue to be
@@ -224,7 +225,7 @@
  */
 void __cheri_libcall
 multiwaiter_queue_send_init(struct EventWaiterSource *source,
-                            struct QueueHandle       *handle);
+                            struct MessageQueue      *handle);
 
 /**
  * Initialise an event waiter source as in `multiwaiter_queue_receive_init`,
@@ -250,4 +251,32 @@
   multiwaiter_queue_send_init_sealed(struct EventWaiterSource *source,
                                      struct SObjStruct        *handle);
 
+/**
+ * Convert a queue handle returned from `queue_create_sealed` into one that can
+ * be used *only* for receiving.
+ *
+ * Returns 0 on success and writes the resulting restricted handle via
+ * `outHandle`.  Returns `-ENOMEM` on allocation failure or `-EINVAL` if the
+ * handle is not valid.
+ */
+int __cheri_compartment("message_queue")
+  queue_receive_handle_create_sealed(struct Timeout     *timeout,
+                                     struct SObjStruct  *heapCapability,
+                                     struct SObjStruct  *handle,
+                                     struct SObjStruct **outHandle);
+
+/**
+ * Convert a queue handle returned from `queue_create_sealed` into one that can
+ * be used *only* for sending.
+ *
+ * Returns 0 on success and writes the resulting restricted handle via
+ * `outHandle`.  Returns `-ENOMEM` on allocation failure or `-EINVAL` if the
+ * handle is not valid.
+ */
+int __cheri_compartment("message_queue")
+  queue_send_handle_create_sealed(struct Timeout     *timeout,
+                                  struct SObjStruct  *heapCapability,
+                                  struct SObjStruct  *handle,
+                                  struct SObjStruct **outHandle);
+
 __END_DECLS
diff --git a/sdk/include/setjmp-assembly.h b/sdk/include/setjmp-assembly.h
new file mode 100644
index 0000000..5c2bc30
--- /dev/null
+++ b/sdk/include/setjmp-assembly.h
@@ -0,0 +1,11 @@
+// Copyright CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#pragma once
+
+#include <assembly-helpers.h>
+
+EXPORT_ASSEMBLY_OFFSET(__jmp_buf, __cs0, 0)
+EXPORT_ASSEMBLY_OFFSET(__jmp_buf, __cs1, 8)
+EXPORT_ASSEMBLY_OFFSET(__jmp_buf, __csp, 16)
+EXPORT_ASSEMBLY_OFFSET(__jmp_buf, __cra, 24)
diff --git a/sdk/include/setjmp.h b/sdk/include/setjmp.h
index d8d3cdf..9710ccd 100644
--- a/sdk/include/setjmp.h
+++ b/sdk/include/setjmp.h
@@ -30,11 +30,14 @@
  */
 typedef struct __jmp_buf jmp_buf[1];
 
+#include <setjmp-assembly.h>
+
+__BEGIN_DECLS
 /**
  * C `setjmp` function.  Returns (up to) twice.  First returns 0, returns a
  * value passed to `longjmp` on the second return.
  */
-__attribute__((returns_twice)) extern "C" int setjmp(jmp_buf env);
+__attribute__((returns_twice)) int setjmp(jmp_buf env);
 __asm__(".section .text.setjmp,\"awG\",@progbits,setjmp,comdat\n"
         ".globl setjmp\n"
         ".p2align 2\n"
@@ -50,7 +53,7 @@
 /**
  * C `longjmp` function.  Does not return, jumps back to the `setjmp` call.
  */
-extern "C" void longjmp(jmp_buf env, int val);
+__attribute__((__noreturn__)) void longjmp(jmp_buf env, int val);
 __asm__(".section .text.longjmp,\"awG\",@progbits,longjmp,comdat\n"
         ".globl longjmp\n"
         ".p2align 2\n"
@@ -62,3 +65,4 @@
         "	clc	cra, 24(ca0)\n"
         "	mv	a0, a1\n"
         "	cjr	cra\n");
+__END_DECLS
diff --git a/sdk/include/stdbool.h b/sdk/include/stdbool.h
index c4013ec..debc62b 100644
--- a/sdk/include/stdbool.h
+++ b/sdk/include/stdbool.h
@@ -5,9 +5,11 @@
 #define _STDBOOL_H_
 
 #ifndef __cplusplus
+#if __STDC_VERSION__ < 202000
 typedef _Bool bool;
 #	define true 1
 #	define false 0
+#endif
 #endif // __cplusplus
 
 #endif // _STDBOOL_H_
diff --git a/sdk/include/stdlib.h b/sdk/include/stdlib.h
index 6955d23..adc2143 100644
--- a/sdk/include/stdlib.h
+++ b/sdk/include/stdlib.h
@@ -329,6 +329,6 @@
 
 static inline void yield(void)
 {
-	__asm volatile("ecall");
+	__asm volatile("ecall" ::: "memory");
 }
 __END_DECLS
diff --git a/sdk/include/token.h b/sdk/include/token.h
index 3c7ba20..c25c04b 100644
--- a/sdk/include/token.h
+++ b/sdk/include/token.h
@@ -69,17 +69,51 @@
                      size_t);
 
 /**
- * Unseal the obj given the key.
+ * Unseal the object given the key.
  *
- * The key must have the permit-unseal permission.
+ * The key may be either a static or dynamic key (i.e. one created with the
+ * `STATIC_SEALING_TYPE` macro or with `token_key_new`) and the object may be
+ * either allocated dynamically (via the token APIs) or statically (via the
+ * `DEFINE_STATIC_SEALED_VALUE` macro).
  *
- * @return unsealed obj if key and obj are valid and they match. nullptr
- * otherwise
+ * Returns the unsealed object if the key and object are valid and of the
+ * correct type, null otherwise.
+ *
+ * This function is equivalent to calling both `token_obj_unseal_static` and
+ * `token_obj_unseal_dynamic` and returning the result of the first one that
+ * succeeds, or null if both fail.
  */
 [[cheri::interrupt_state(disabled)]] void *
   __cheri_libcall token_obj_unseal(SKey, SObj);
 
 /**
+ * Unseal the object given the key.
+ *
+ * The key must be a static sealing key (i.e. one created with the
+ * `STATIC_SEALING_TYPE` macro) and the object must be a statically sealed
+ * object (i.e. one created with the `DEFINE_STATIC_SEALED_VALUE` macro).
+ *
+ * Returns the unsealed object if the key and object are valid and of the
+ * correct type, null otherwise.
+ */
+[[cheri::interrupt_state(disabled)]] void *
+  __cheri_libcall token_obj_unseal_static(SKey, SObj);
+
+/**
+ * Unseal the object given the key.
+ *
+ * The key may be either a static or dynamic key (i.e. one created with the
+ * `STATIC_SEALING_TYPE` macro or with `token_key_new`) and the object must be
+ * allocated dynamically with `token_sealed_alloc` or
+ * `token_sealed_unsealed_alloc`.
+ *
+ * Returns the unsealed object if the key and object are valid and of the
+ * correct type, null otherwise.
+ */
+[[cheri::interrupt_state(disabled)]] void *
+  __cheri_libcall token_obj_unseal_dynamic(SKey, SObj);
+
+/**
  * Destroy the obj given its key, freeing memory.
  *
  * The key must have the permit-unseal permission.
diff --git a/sdk/include/unwind-assembly.h b/sdk/include/unwind-assembly.h
new file mode 100644
index 0000000..377d97f
--- /dev/null
+++ b/sdk/include/unwind-assembly.h
@@ -0,0 +1,12 @@
+// Copyright CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#pragma once
+
+#include <assembly-helpers.h>
+#include <setjmp-assembly.h>
+
+#define INVOCATION_LOCAL_UNWIND_LIST_OFFSET 8
+
+EXPORT_ASSEMBLY_OFFSET(CleanupList, next, 0)
+EXPORT_ASSEMBLY_OFFSET(CleanupList, env, 8)
diff --git a/sdk/include/unwind.h b/sdk/include/unwind.h
index 7a1c898..ce6a25a 100644
--- a/sdk/include/unwind.h
+++ b/sdk/include/unwind.h
@@ -9,11 +9,13 @@
 struct CleanupList
 {
 	/// Next pointer.
-	CleanupList *next;
+	struct CleanupList *next;
 	/// Jump buffer to return to.
-	__jmp_buf env;
+	struct __jmp_buf env;
 };
 
+#include <unwind-assembly.h>
+
 /**
  * Head of the cleanup list.
  *
@@ -25,7 +27,8 @@
 {
 	void     *csp = __builtin_cheri_stack_get();
 	ptraddr_t top = __builtin_cheri_top_get(csp);
-	csp           = __builtin_cheri_address_set(csp, top - 8);
+	csp           = __builtin_cheri_address_set(
+	            csp, top - INVOCATION_LOCAL_UNWIND_LIST_OFFSET);
 	return (struct CleanupList **)csp;
 }
 
@@ -34,9 +37,9 @@
  */
 __always_inline static inline void cleanup_unwind(void)
 {
-	CleanupList **__head = cleanup_list_head();
-	CleanupList  *__top  = *__head;
-	*__head              = __top->next;
+	struct CleanupList **__head = cleanup_list_head();
+	struct CleanupList  *__top  = *__head;
+	*__head                     = __top->next;
 	switcher_handler_invocation_count_reset();
 	longjmp(&__top->env, 1);
 }
@@ -53,10 +56,10 @@
  */
 #define CHERIOT_DURING                                                         \
 	{                                                                          \
-		CleanupList cleanupListEntry;                                          \
-		auto      **__head    = cleanup_list_head();                           \
-		cleanupListEntry.next = *__head;                                       \
-		*__head               = &cleanupListEntry;                             \
+		struct CleanupList   cleanupListEntry;                                 \
+		struct CleanupList **__head = cleanup_list_head();                     \
+		cleanupListEntry.next       = *__head;                                 \
+		*__head                     = &cleanupListEntry;                       \
 		if (setjmp(&cleanupListEntry.env) == 0)                                \
 		{
 /// See CHERIOT_DURING.
diff --git a/sdk/lib/freestanding/memcpy.c b/sdk/lib/freestanding/memcpy.c
index 56ed012..5b7c791 100644
--- a/sdk/lib/freestanding/memcpy.c
+++ b/sdk/lib/freestanding/memcpy.c
@@ -49,7 +49,9 @@
 typedef void *word;
 
 #define wsize sizeof(word)
-_Static_assert(wsize != 0 && (wsize & (wsize - 1)) == 0);
+_Static_assert(wsize != 0);
+_Static_assert((wsize & (wsize - 1)) == 0);
+
 #define wmask (wsize - 1)
 
 void *__cheri_libcall memcpy(void *dst0, const void *src0, size_t length)
diff --git a/sdk/lib/queue/README.md b/sdk/lib/queue/README.md
new file mode 100644
index 0000000..b5837a3
--- /dev/null
+++ b/sdk/lib/queue/README.md
@@ -0,0 +1,12 @@
+Message queues
+==============
+
+Message queues, as described in [`queue.h`](../../include/queue.h).
+
+This directory provides two targets.
+
+ - The message queue library (`message_queue_library`) provides APIs for message queues that can be shared between two threads in the same compartment.
+ - The message queue compartment (`message_queue`) wraps these in APIs that can be used from different compartments.
+
+The library uses the `setjmp`-based error handler (see: [`unwind.h`](../../include/unwind.h)) to recover from invalid bounds or permissions.
+If you are using the library and want to be robust in the presence of CHERI exceptions, you should either add `unwind_error_handler` as a dependency of your compartment or provide an error handler that calls `cleanup_unwind`.
diff --git a/sdk/lib/queue/queue.cc b/sdk/lib/queue/queue.cc
index 879f8c6..716ad77 100644
--- a/sdk/lib/queue/queue.cc
+++ b/sdk/lib/queue/queue.cc
@@ -7,11 +7,12 @@
 #include <stdint.h>
 #include <timeout.h>
 #include <type_traits>
+#include <unwind.h>
 
 using namespace CHERI;
 using cheriot::atomic;
 
-using Debug = ConditionalDebug<false, "Queue library">;
+using Debug = ConditionalDebug<false, "MessageQueue library">;
 
 #ifdef __cplusplus
 using MessageQueueCounter = atomic<uint32_t>;
@@ -208,15 +209,15 @@
 	/**
 	 * Returns a pointer to the element in the queue indicated by `counter`.
 	 */
-	Capability<void> buffer_at_counter(struct QueueHandle &handle,
-	                                   uint32_t            counter)
+	Capability<void> buffer_at_counter(struct MessageQueue &handle,
+	                                   uint32_t             counter)
 	{
 		// Handle wrap for the second run around the counter.
 		size_t index =
 		  counter >= handle.queueSize ? counter - handle.queueSize : counter;
 		auto             offset = index * handle.elementSize;
-		Capability<void> pointer{handle.buffer};
-		pointer.address() += offset;
+		Capability<void> pointer{&handle};
+		pointer.address() += sizeof(MessageQueue) + offset;
 		return pointer;
 	}
 
@@ -332,102 +333,30 @@
 		  old, (old & HighBitFlagLock::reserved_bits()) | value));
 	}
 
-	/// Permissions for read-only access to a counter.
-	static constexpr PermissionSet ReadOnly{Permission::Global,
-	                                        Permission::Load};
-	/// Permissions for read-only access to a buffer.
-	static constexpr PermissionSet ReadOnlyCapability{
-	  Permission::Global,
-	  Permission::Load,
-	  Permission::LoadStoreCapability,
-	  Permission::LoadGlobal,
-	  Permission::LoadGlobal};
-	/// Permissions for write-only access to a buffer.
-	static constexpr PermissionSet WriteOnlyCapability{
-	  Permission::Global,
-	  Permission::Store,
-	  Permission::LoadStoreCapability};
-
-	/**
-	 * Helper to drop our short-lived claims.
-	 */
-	void drop_claims()
-	{
-		Timeout t{0};
-		heap_claim_fast(&t, nullptr, nullptr);
-	}
-
-	void bound_queue_buffer(struct QueueHandle handle)
-	{
-		Capability buffer   = handle.buffer;
-		Capability producer = handle.producer;
-		// Restrict the bounds using the address of the producer, which
-		// comes immediately after the queue buffer. This should be
-		// strictly equivalent to calculating the size of the queue
-		// from the number of elements and the size of elements (we
-		// assert that below).
-		buffer.bounds() = producer.address() - buffer.address();
-		Debug::Assert(
-		  [&]() -> bool {
-			  size_t bufferSize;
-			  bool   overflow = __builtin_mul_overflow(
-			      handle.queueSize, handle.elementSize, &bufferSize);
-			  bufferSize = CHERI::representable_length(bufferSize);
-			  return (!overflow) && (buffer.bounds() == bufferSize);
-		  },
-		  "Mismatch between the size of the queue as reported by `queueSize` "
-		  "and `elementSize` and its real size.");
-	}
-
 } // namespace
 
-struct QueueHandle queue_make_receive_handle(struct QueueHandle handle)
-{
-	Capability buffer   = handle.buffer;
-	Capability producer = handle.producer;
-	bound_queue_buffer(handle);
-	buffer.permissions() &= ReadOnlyCapability;
-	producer.permissions() &= ReadOnly;
-	handle.buffer   = buffer;
-	handle.producer = producer;
-	return handle;
-}
-
-struct QueueHandle queue_make_send_handle(struct QueueHandle handle)
-{
-	Capability buffer   = handle.buffer;
-	Capability consumer = handle.consumer;
-	bound_queue_buffer(handle);
-	buffer.permissions() &= WriteOnlyCapability;
-	consumer.permissions() &= ReadOnly;
-	handle.buffer   = buffer;
-	handle.consumer = consumer;
-	return handle;
-}
-
-int queue_destroy(struct SObjStruct *heapCapability, struct QueueHandle *handle)
+int queue_destroy(struct SObjStruct   *heapCapability,
+                  struct MessageQueue *handle)
 {
 	int ret = 0;
 	// Only upgrade the locks for destruction if we know that we will be
 	// able to free the queue at the end. This will fail if passed a
 	// restricted buffer, which will happen if `queue_destroy` is called on
 	// a restricted queue.
-	if (ret = heap_can_free(heapCapability, handle->buffer); ret != 0)
+	if (ret = heap_can_free(heapCapability, handle); ret != 0)
 	{
 		return ret;
 	}
 
-	auto           *producer = handle->producer;
-	HighBitFlagLock producerLock{*producer};
+	HighBitFlagLock producerLock{handle->producer};
 	producerLock.upgrade_for_destruction();
 
-	auto           *consumer = handle->consumer;
-	HighBitFlagLock consumerLock{*consumer};
+	HighBitFlagLock consumerLock{handle->consumer};
 	consumerLock.upgrade_for_destruction();
 
 	// This should not fail because of the `heap_can_free` check, unless we
 	// run out of stack.
-	if (ret = heap_free(heapCapability, handle->buffer); ret != 0)
+	if (ret = heap_free(heapCapability, handle); ret != 0)
 	{
 		return ret;
 	}
@@ -435,27 +364,16 @@
 	return ret;
 }
 
-int queue_create(Timeout            *timeout,
-                 struct SObjStruct  *heapCapability,
-                 struct QueueHandle *outQueue,
-                 void              **outAllocation,
-                 size_t              elementSize,
-                 size_t              elementCount)
+ssize_t queue_allocation_size(size_t elementSize, size_t elementCount)
 {
 	size_t bufferSize;
 	size_t allocSize;
 	bool   overflow =
 	  __builtin_mul_overflow(elementCount, elementSize, &bufferSize);
-	// We must be able to accurately represent the buffer, so round it up to a
-	// representable length.
-	bufferSize = CHERI::representable_length(bufferSize);
 	static constexpr size_t CounterSize = sizeof(uint32_t);
-	// Round up the size to be correctly aligned for the counters at the end
-	// (if necessary) and add two counters worth of space.
-	overflow |= __builtin_add_overflow(
-	  bufferSize,
-	  (2 * CounterSize) + (CounterSize - (bufferSize & (CounterSize - 1))),
-	  &allocSize);
+	// We also need space for the header
+	overflow |=
+	  __builtin_add_overflow(sizeof(MessageQueue), bufferSize, &allocSize);
 	if (overflow)
 	{
 		return -EINVAL;
@@ -471,6 +389,21 @@
 		return -EINVAL;
 	}
 
+	return allocSize;
+}
+
+int queue_create(Timeout              *timeout,
+                 struct SObjStruct    *heapCapability,
+                 struct MessageQueue **outQueue,
+                 size_t                elementSize,
+                 size_t                elementCount)
+{
+	ssize_t allocSize = queue_allocation_size(elementSize, elementCount);
+	if (allocSize < 0)
+	{
+		return allocSize;
+	}
+
 	// Allocate the space for the queue.
 	Capability buffer{heap_allocate(timeout, heapCapability, allocSize)};
 	if (!buffer.is_valid())
@@ -478,86 +411,79 @@
 		return -ENOMEM;
 	}
 
-	Capability<std::atomic<uint32_t>> producer{
-	  buffer.cast<std::atomic<uint32_t>>()};
-	Capability<std::atomic<uint32_t>> consumer{
-	  buffer.cast<std::atomic<uint32_t>>()};
-	// Make the producer and consumer point after the buffer
-	producer.address() += bufferSize;
-	consumer.address() += bufferSize + CounterSize;
-	// Set their bounds to 4 bytes.
-	producer.bounds() = CounterSize;
-	consumer.bounds() = CounterSize;
-	// The pointer used to free the allocation
-	*outAllocation = buffer;
-	Debug::log("Created queue with buffer: {}", buffer);
-	// The handle
-	*outQueue = {elementSize, elementCount, buffer, producer, consumer};
-
+	*outQueue = new (buffer.get()) MessageQueue(elementSize, elementCount);
 	return 0;
 }
 
-int queue_send(Timeout *timeout, struct QueueHandle *handle, const void *src)
+int queue_send(Timeout *timeout, struct MessageQueue *handle, const void *src)
 {
 	Debug::log("Send called on: {}", handle);
-	auto *producer   = handle->producer;
-	auto *consumer   = handle->consumer;
+	auto *producer   = &handle->producer;
+	auto *consumer   = &handle->consumer;
 	bool  shouldWake = false;
 	{
 		Debug::log("Lock word: {}", producer->load());
 		HighBitFlagLock l{*producer};
 		if (LockGuard g{l, timeout})
 		{
-			uint32_t producerCounter = counter_load(producer);
-			uint32_t consumerValue   = consumer->load();
-			uint32_t consumerCounter =
-			  consumerValue & ~(HighBitFlagLock::reserved_bits());
-			Debug::log("Producer counter: {}, consumer counter: {}, Size: {}",
-			           producerCounter,
-			           consumerCounter,
-			           handle->queueSize);
-			while (is_full(handle->queueSize, producerCounter, consumerCounter))
+			volatile int ret = 0;
+			// In an error-handling context, try to add the element to the
+			// queue.  If the permissions on src are invalid, or either `handle`
+			// or `src` is freed concurrently, we will hit the path that returns
+			// -EPERM.  The counter update happens last, so any failure will
+			// simply leave the queue in the old state.
+			on_error(
+			  [&] {
+				  uint32_t producerCounter = counter_load(producer);
+				  uint32_t consumerValue   = consumer->load();
+				  uint32_t consumerCounter =
+				    consumerValue & ~(HighBitFlagLock::reserved_bits());
+				  Debug::log(
+				    "Producer counter: {}, consumer counter: {}, Size: {}",
+				    producerCounter,
+				    consumerCounter,
+				    handle->queueSize);
+				  while (is_full(
+				    handle->queueSize, producerCounter, consumerCounter))
+				  {
+					  // Wait on the value to change.  If we hit this path while
+					  // the consumer lock is held, then the high bits will be
+					  // set.  Make sure that we yield.
+					  if (consumer->wait(timeout, consumerValue) == -ETIMEDOUT)
+					  {
+						  Debug::log("Timed out on futex");
+						  ret = -ETIMEDOUT;
+						  return;
+					  }
+					  consumerValue = consumer->load();
+					  consumerCounter =
+					    consumerValue & ~(HighBitFlagLock::reserved_bits());
+				  }
+				  auto entry = buffer_at_counter(*handle, producerCounter);
+				  Debug::log("Send copying {} bytes from {} to {}",
+				             handle->elementSize,
+				             src,
+				             entry);
+				  memcpy(entry, src, handle->elementSize);
+				  counter_store(
+				    &handle->producer,
+				    increment_and_wrap(handle->queueSize, producerCounter));
+				  // Check if the queue was empty before we updated the producer
+				  // counter.  By the time that we reach this point, anything on
+				  // the consumer side will be on the path to a futex_wait with
+				  // the old version of the producer counter and so will bounce
+				  // out again.
+				  shouldWake =
+				    is_empty(producerCounter, counter_load(consumer));
+			  },
+			  [&]() {
+				  ret = -EPERM;
+				  Debug::log("Error in send");
+			  });
+			if (ret != 0)
 			{
-				// Wait on the value to change.  If we hit this path while the
-				// consumer lock is held, then the high bits will be set.  Make
-				// sure that we yield.
-				if (consumer->wait(timeout, consumerValue) == -ETIMEDOUT)
-				{
-					Debug::log("Timed out on futex");
-					return -ETIMEDOUT;
-				}
-				consumerValue = consumer->load();
-				consumerCounter =
-				  consumerValue & ~(HighBitFlagLock::reserved_bits());
+				return ret;
 			}
-			auto entry = buffer_at_counter(*handle, producerCounter);
-			if (int claim = heap_claim_fast(timeout, handle->buffer, src);
-			    claim != 0)
-			{
-				Debug::log("Claim failed: {}", claim);
-				return claim;
-			}
-			if (!check_pointer<PermissionSet{Permission::Load}, false>(
-			      src, handle->elementSize))
-			{
-				drop_claims();
-				Debug::log("Load / bounds check failed: {}");
-				return -EPERM;
-			}
-			Debug::log("Send copying {} bytes from {} to {}",
-			           handle->elementSize,
-			           src,
-			           entry);
-			memcpy(entry, src, handle->elementSize);
-			drop_claims();
-			counter_store(
-			  handle->producer,
-			  increment_and_wrap(handle->queueSize, producerCounter));
-			// Check if the queue was empty before we updated the producer
-			// counter.  By the time that we reach this point, anything on the
-			// consumer side will be on the path to a futex_wait with the old
-			// version of the producer counter and so will bounce out again.
-			shouldWake = is_empty(producerCounter, counter_load(consumer));
 		}
 		else
 		{
@@ -567,71 +493,77 @@
 	}
 	if (shouldWake)
 	{
-		handle->producer->notify_all();
+		handle->producer.notify_all();
 	}
 	return 0;
 }
 
-int queue_receive(Timeout *timeout, struct QueueHandle *handle, void *dst)
+int queue_receive(Timeout *timeout, struct MessageQueue *handle, void *dst)
 {
 	Debug::log("Receive called on: {}", handle);
-	auto *producer   = handle->producer;
-	auto *consumer   = handle->consumer;
+	auto *producer   = &handle->producer;
+	auto *consumer   = &handle->consumer;
 	bool  shouldWake = false;
 	{
 		HighBitFlagLock l{*consumer};
 		if (LockGuard g{l, timeout})
 		{
-			uint32_t producerValue = producer->load();
-			uint32_t producerCounter =
-			  producerValue & ~(HighBitFlagLock::reserved_bits());
-			uint32_t consumerCounter = counter_load(consumer);
-			Debug::log("Producer counter: {}, consumer counter: {}, Size: {}",
-			           producerCounter,
-			           consumerCounter,
-			           handle->queueSize);
-			while (is_empty(producerCounter, consumerCounter))
+			volatile int ret = 0;
+			// In an error-handling context, try to add the element to the
+			// queue.  If the permissions on `dst` are invalid, or either
+			// `handle` or `dst` is freed concurrently, we will hit the path
+			// that returns `-EPERM`.  The counter update happens last, so any
+			// failure will simply leave the queue in the old state.
+			on_error(
+			  [&] {
+				  uint32_t producerValue = producer->load();
+				  uint32_t producerCounter =
+				    producerValue & ~(HighBitFlagLock::reserved_bits());
+				  uint32_t consumerCounter = counter_load(consumer);
+				  Debug::log(
+				    "Producer counter: {}, consumer counter: {}, Size: {}",
+				    producerCounter,
+				    consumerCounter,
+				    handle->queueSize);
+				  while (is_empty(producerCounter, consumerCounter))
+				  {
+					  // Wait on the value to change.  If we hit this path while
+					  // the producer lock is held, then the high bits will be
+					  // set.  Make sure that we yield.
+					  if (producer->wait(timeout, producerValue) == -ETIMEDOUT)
+					  {
+						  ret = -ETIMEDOUT;
+						  return;
+					  }
+					  producerValue = producer->load();
+					  producerCounter =
+					    producerValue & ~(HighBitFlagLock::reserved_bits());
+				  }
+				  auto entry = buffer_at_counter(*handle, consumerCounter);
+				  Debug::log("Receive copying {} bytes from {} to {}",
+				             handle->elementSize,
+				             entry,
+				             dst);
+				  memcpy(dst, entry, handle->elementSize);
+				  counter_store(
+				    consumer,
+				    increment_and_wrap(handle->queueSize, consumerCounter));
+				  // Check if the queue was full before we updated the consumer
+				  // counter.  By the time that we reach this point, anything on
+				  // the producer side will be on the path to a futex_wait with
+				  // the old version of the consumer counter and so will bounce
+				  // out again.
+				  shouldWake = is_full(
+				    handle->queueSize, counter_load(producer), consumerCounter);
+			  },
+			  [&]() {
+				  ret = -EPERM;
+				  Debug::log("Error in receive");
+			  });
+			if (ret != 0)
 			{
-				// Wait on the value to change.  If we hit this path while the
-				// producer lock is held, then the high bits will be set.  Make
-				// sure that we yield.
-				if (producer->wait(timeout, producerValue) == -ETIMEDOUT)
-				{
-					return -ETIMEDOUT;
-				}
-				producerValue = producer->load();
-				producerCounter =
-				  producerValue & ~(HighBitFlagLock::reserved_bits());
+				return ret;
 			}
-			auto entry = buffer_at_counter(*handle, consumerCounter);
-			if (int claim = heap_claim_fast(timeout, handle->buffer, dst);
-			    claim != 0)
-			{
-				return claim;
-			}
-			if (!check_pointer<PermissionSet{Permission::Store}, false>(
-			      dst, handle->elementSize))
-			{
-				drop_claims();
-				Debug::log("Check pointer failed with {} for {} byte write",
-				           dst,
-				           handle->elementSize);
-				return -EPERM;
-			}
-			Debug::log("Receive copying {} bytes from {} to {}",
-			           handle->elementSize,
-			           entry,
-			           dst);
-			memcpy(dst, entry, handle->elementSize);
-			drop_claims();
-			counter_store(
-			  consumer, increment_and_wrap(handle->queueSize, consumerCounter));
-			// Check if the queue was full before we updated the consumer
-			// counter.  By the time that we reach this point, anything on the
-			// producer side will be on the path to a futex_wait with the old
-			// version of the consumer counter and so will bounce out again.
-			shouldWake = is_full(
-			  handle->queueSize, counter_load(producer), consumerCounter);
 		}
 		else
 		{
@@ -639,17 +571,19 @@
 			return -ETIMEDOUT;
 		}
 	}
+	// If the queue is concurrently freed, this can trap, but we won't leak any
+	// locks.
 	if (shouldWake)
 	{
-		handle->consumer->notify_all();
+		handle->consumer.notify_all();
 	}
 	return 0;
 }
 
-int queue_items_remaining(struct QueueHandle *handle, size_t *items)
+int queue_items_remaining(struct MessageQueue *handle, size_t *items)
 {
-	auto producerCounter = counter_load(handle->producer);
-	auto consumerCounter = counter_load(handle->consumer);
+	auto producerCounter = counter_load(&handle->producer);
+	auto consumerCounter = counter_load(&handle->consumer);
 	*items =
 	  items_remaining(handle->queueSize, producerCounter, consumerCounter);
 	Debug::log("Producer counter: {}, consumer counter: {}, items: {}",
@@ -660,20 +594,20 @@
 }
 
 void multiwaiter_queue_send_init(struct EventWaiterSource *source,
-                                 struct QueueHandle       *handle)
+                                 struct MessageQueue      *handle)
 {
-	uint32_t producer   = counter_load(handle->producer);
-	uint32_t consumer   = counter_load(handle->consumer);
-	source->eventSource = handle->consumer;
+	uint32_t producer   = counter_load(&handle->producer);
+	uint32_t consumer   = counter_load(&handle->consumer);
+	source->eventSource = &handle->consumer;
 	source->value =
 	  is_full(handle->queueSize, producer, consumer) ? consumer : -1;
 }
 
 void multiwaiter_queue_receive_init(struct EventWaiterSource *source,
-                                    struct QueueHandle       *handle)
+                                    struct MessageQueue      *handle)
 {
-	uint32_t producer   = counter_load(handle->producer);
-	uint32_t consumer   = counter_load(handle->consumer);
-	source->eventSource = handle->producer;
+	uint32_t producer   = counter_load(&handle->producer);
+	uint32_t consumer   = counter_load(&handle->consumer);
+	source->eventSource = &handle->producer;
 	source->value       = is_empty(producer, consumer) ? producer : -1;
 }
diff --git a/sdk/lib/queue/queue_compartment.cc b/sdk/lib/queue/queue_compartment.cc
index 96f4845..9aec00a 100644
--- a/sdk/lib/queue/queue_compartment.cc
+++ b/sdk/lib/queue/queue_compartment.cc
@@ -8,10 +8,14 @@
 
 using namespace CHERI;
 
-using Debug = ConditionalDebug<false, "Queue compartment">;
+using Debug = ConditionalDebug<false, "MessageQueue compartment">;
 
 namespace
 {
+	__always_inline SKey handle_key()
+	{
+		return STATIC_SEALING_TYPE(MessageQueueHandle);
+	}
 	__always_inline SKey receive_key()
 	{
 		return STATIC_SEALING_TYPE(ReceiveHandle);
@@ -21,88 +25,62 @@
 		return STATIC_SEALING_TYPE(SendHandle);
 	}
 
-	struct QueueEndpoint
+	/**
+	 * Wrapper used for restricted endpoints.  This is used to provide
+	 * capabilities that allow only sending or receiving.  Instances of this
+	 * will be sealed with either `send_key()` or `receive_key()` to define
+	 * their types.
+	 */
+	struct RestrictedEndpoint
 	{
-		QueueHandle handle;
-		void       *allocation;
-		// Lock that protects against double free.
-		FlagLockPriorityInherited lock;
+		MessageQueue *handle;
 	};
 
+	/**
+	 * Unseal something that is either a queue handle or a restricted endpoint
+	 * with the specified key.
+	 */
+	MessageQueue *unseal(SKey key, SObj handle)
+	{
+		MessageQueue *queue = nullptr;
+		if (auto *unsealed =
+		      token_unseal(key, Sealed<RestrictedEndpoint>{handle}))
+		{
+			queue = unsealed->handle;
+		}
+		else if (auto *unsealed =
+		           token_unseal(handle_key(), Sealed<MessageQueue>{handle}))
+		{
+			queue = unsealed;
+		}
+		return queue;
+	}
+
 } // namespace
 
 int queue_create_sealed(Timeout            *timeout,
                         struct SObjStruct  *heapCapability,
-                        struct SObjStruct **outQueueSend,
-                        struct SObjStruct **outQueueReceive,
+                        struct SObjStruct **outQueue,
                         size_t              elementSize,
                         size_t              elementCount)
 {
-	if (!check_timeout_pointer(timeout))
+	ssize_t allocSize = queue_allocation_size(elementSize, elementCount);
+	if (allocSize < 0)
 	{
-		return -EPERM;
+		return -EINVAL;
 	}
 
-	// Allocate the queue endpoints
-	auto [send, sendSealed] =
-	  token_allocate<QueueEndpoint>(timeout, heapCapability, send_key());
-	if (!send)
+	void *unsealed = nullptr;
+	// Allocate the space for the queue.
+	auto sealed = token_sealed_unsealed_alloc(
+	  timeout, heapCapability, handle_key(), allocSize, &unsealed);
+	if (!unsealed)
 	{
-		return timeout->may_block() ? -ENOMEM : -ETIMEDOUT;
-	}
-	auto [receive, receiveSealed] =
-	  token_allocate<QueueEndpoint>(timeout, heapCapability, receive_key());
-	if (!receive)
-	{
-		token_obj_destroy(heapCapability, send_key(), sendSealed);
-		return timeout->may_block() ? -ENOMEM : -ETIMEDOUT;
+		return -ENOMEM;
 	}
 
-	// Bidirectional queue handle
-	QueueHandle handle;
-	// The pointer to the queue that is used when freeing
-	void *freeBuffer;
-	// Allocate the queue object
-	int ret = queue_create(
-	  timeout, heapCapability, &handle, &freeBuffer, elementSize, elementCount);
-	if (ret != 0)
-	{
-		token_obj_destroy(heapCapability, send_key(), sendSealed);
-		token_obj_destroy(heapCapability, receive_key(), receiveSealed);
-		return ret;
-	}
-
-	send->handle        = queue_make_send_handle(handle);
-	send->allocation    = freeBuffer;
-	receive->handle     = queue_make_receive_handle(handle);
-	receive->allocation = freeBuffer;
-	// Add a second claim on the buffer so that we can free the queue by freeing
-	// it twice, once in each endpoint.
-	// TODO we should check the return value of `heap_claim`
-	heap_claim(heapCapability, freeBuffer);
-
-	if (int claimed = heap_claim_fast(timeout, outQueueSend, outQueueReceive);
-	    claimed != 0)
-	{
-		return claimed;
-	}
-	if (!check_pointer<PermissionSet{Permission::Load,
-	                                 Permission::Store,
-	                                 Permission::LoadStoreCapability}>(
-	      outQueueReceive, sizeof(void *)) ||
-	    !check_pointer<PermissionSet{Permission::Load,
-	                                 Permission::Store,
-	                                 Permission::LoadStoreCapability}>(
-	      outQueueSend, sizeof(void *)))
-	{
-		// Free twice because we claimed it once in addition to the original
-		// allocation.
-		heap_free(heapCapability, freeBuffer);
-		heap_free(heapCapability, freeBuffer);
-		return -EPERM;
-	}
-	*outQueueSend    = sendSealed;
-	*outQueueReceive = receiveSealed;
+	new (unsealed) MessageQueue(elementSize, elementCount);
+	*outQueue = sealed;
 	return 0;
 }
 
@@ -110,99 +88,131 @@
                          struct SObjStruct *heapCapability,
                          struct SObjStruct *queueHandle)
 {
-	if (!check_timeout_pointer(timeout))
+	if (token_obj_unseal(handle_key(), queueHandle) != nullptr)
 	{
-		return -EPERM;
+		token_obj_destroy(heapCapability, handle_key(), queueHandle);
+		return 0;
 	}
-	Debug::log("Destroying queue {}", queueHandle);
-	auto  token = receive_key();
-	auto *end   = token_unseal(token, Sealed<QueueEndpoint>{queueHandle});
-	// This function takes either endpoint, so we need to try unsealing with
-	// both keys.
-	if (!end)
+	if (token_obj_unseal(send_key(), queueHandle) != nullptr)
 	{
-		token = send_key();
-		end   = token_unseal(token, Sealed<QueueEndpoint>{queueHandle});
+		token_obj_destroy(heapCapability, send_key(), queueHandle);
+		return 0;
 	}
-	if (!end)
+	if (token_obj_unseal(receive_key(), queueHandle) != nullptr)
 	{
-		return -EINVAL;
+		token_obj_destroy(heapCapability, receive_key(), queueHandle);
+		return 0;
 	}
-	// Don't bother with a lock guard: we will destroy this lock if we reach the
-	// end. If we lose a race here, this will trap and we will implicitly return
-	// `-ECOMPARTMENTFAIL`.
-	if (!end->lock.try_lock(timeout))
-	{
-		return -ETIMEDOUT;
-	}
-	if (heap_free(heapCapability, end->allocation) != 0)
-	{
-		end->lock.unlock();
-		return -EPERM;
-	}
-	token_obj_destroy(heapCapability, token, queueHandle);
-	return 0;
+	return -EINVAL;
 }
 
 int queue_send_sealed(Timeout           *timeout,
                       struct SObjStruct *handle,
                       const void        *src)
 {
-	auto *end = token_unseal(send_key(), Sealed<QueueEndpoint>{handle});
-	// If we failed to unseal, or if the timeout pointer is invalid, invalid
-	// argument error.
-	if (!end || !check_timeout_pointer(timeout))
+	MessageQueue *queue = unseal(send_key(), handle);
+	if (!queue || !check_timeout_pointer(timeout))
 	{
 		return -EINVAL;
 	}
-	return queue_send(timeout, &end->handle, src);
+	return queue_send(timeout, queue, src);
 }
 
 int queue_receive_sealed(Timeout *timeout, struct SObjStruct *handle, void *dst)
 {
-	auto *end = token_unseal(receive_key(), Sealed<QueueEndpoint>{handle});
-	// If we failed to unseal, or if the timeout is on the heap, invalid
-	// argument error.
-	if (!end || !check_timeout_pointer(timeout))
+	MessageQueue *queue = unseal(receive_key(), handle);
+	if (!queue || !check_timeout_pointer(timeout))
 	{
 		return -EINVAL;
 	}
-	return queue_receive(timeout, &end->handle, dst);
+	return queue_receive(timeout, queue, dst);
 }
 
 int multiwaiter_queue_receive_init_sealed(struct EventWaiterSource *source,
                                           struct SObjStruct        *handle)
 {
-	auto *end = token_unseal(receive_key(), Sealed<QueueEndpoint>{handle});
-	if (!end)
+	MessageQueue *queue = unseal(receive_key(), handle);
+	if (!queue)
 	{
 		return -EINVAL;
 	}
-	multiwaiter_queue_receive_init(source, &end->handle);
+	multiwaiter_queue_receive_init(source, queue);
 	return 0;
 }
 
 int multiwaiter_queue_send_init_sealed(struct EventWaiterSource *source,
                                        struct SObjStruct        *handle)
 {
-	auto *end = token_unseal(send_key(), Sealed<QueueEndpoint>{handle});
-	if (!end)
+	MessageQueue *queue = unseal(send_key(), handle);
+	if (!queue)
 	{
 		return -EINVAL;
 	}
-	multiwaiter_queue_send_init(source, &end->handle);
+	multiwaiter_queue_send_init(source, queue);
 	return 0;
 }
 
-int queue_items_remaining_sealed(struct SObjStruct *queueHandle, size_t *items)
+int queue_items_remaining_sealed(struct SObjStruct *handle, size_t *items)
 {
-	auto *end = token_unseal(receive_key(), Sealed<QueueEndpoint>{queueHandle});
+	MessageQueue *queue = unseal(send_key(), handle);
 	// This function takes either endpoint, so we need to try unsealing with
 	// both keys.
-	if (!end)
+	if (!queue)
 	{
-		end = token_unseal(send_key(), Sealed<QueueEndpoint>{queueHandle});
+		if (auto *unsealed =
+		      token_unseal(receive_key(), Sealed<RestrictedEndpoint>{handle}))
+		{
+			queue = unsealed->handle;
+		}
 	}
-	queue_items_remaining(&end->handle, items);
+	if (!queue)
+	{
+		return -EINVAL;
+	}
+	queue_items_remaining(queue, items);
+	return 0;
+}
+
+int queue_receive_handle_create_sealed(struct Timeout     *timeout,
+                                       struct SObjStruct  *heapCapability,
+                                       struct SObjStruct  *handle,
+                                       struct SObjStruct **outHandle)
+{
+	MessageQueue *queue =
+	  token_unseal(handle_key(), Sealed<MessageQueue>(handle));
+	if (!queue)
+	{
+		return -EINVAL;
+	}
+	auto [unsealed, sealed] = token_allocate<RestrictedEndpoint>(
+	  timeout, heapCapability, receive_key());
+	if (!unsealed)
+	{
+		return -ENOMEM;
+	}
+	unsealed->handle = queue;
+	*outHandle       = sealed;
+	return 0;
+}
+
+int queue_send_handle_create_sealed(struct Timeout     *timeout,
+                                    struct SObjStruct  *heapCapability,
+                                    struct SObjStruct  *handle,
+                                    struct SObjStruct **outHandle)
+{
+	MessageQueue *queue =
+	  token_unseal(handle_key(), Sealed<MessageQueue>(handle));
+	if (!queue)
+	{
+		return -EINVAL;
+	}
+	auto [unsealed, sealed] =
+	  token_allocate<RestrictedEndpoint>(timeout, heapCapability, send_key());
+	if (!unsealed)
+	{
+		return -ENOMEM;
+	}
+	unsealed->handle = queue;
+	*outHandle       = sealed;
 	return 0;
 }
diff --git a/sdk/lib/queue/xmake.lua b/sdk/lib/queue/xmake.lua
index 53ec1f2..113b580 100644
--- a/sdk/lib/queue/xmake.lua
+++ b/sdk/lib/queue/xmake.lua
@@ -9,6 +9,7 @@
   add_files("queue.cc")
 
 compartment("message_queue")
+  add_deps("unwind_error_handler")
   add_deps("message_queue_library")
   set_default(false)
   add_files("queue_compartment.cc")
diff --git a/sdk/lib/stdio/printf.cc b/sdk/lib/stdio/printf.cc
index 8fc5f51..579b6b6 100644
--- a/sdk/lib/stdio/printf.cc
+++ b/sdk/lib/stdio/printf.cc
@@ -88,7 +88,9 @@
 			*++p = upper ? toupper(c) : c;
 		} while (num /= base);
 		if (lenp)
+		{
 			*lenp = p - nbuf;
+		}
 		return (p);
 	}
 
@@ -158,7 +160,9 @@
 			while ((ch = static_cast<unsigned char>(*fmt++)) != '%' || stop)
 			{
 				if (ch == '\0')
+				{
 					return (retval);
+				}
 				putchar(ch);
 			}
 			percent   = fmt - 1;
@@ -229,21 +233,31 @@
 						n  = n * 10 + ch - '0';
 						ch = *fmt;
 						if (ch < '0' || ch > '9')
+						{
 							break;
+						}
 					}
 					if (dot)
+					{
 						dwidth = n;
+					}
 					else
+					{
 						width = n;
+					}
 					goto reswitch; // NOLINT
 				case 'b':
 					num = static_cast<unsigned int>(va_arg(ap, int));
 					p   = va_arg(ap, char *);
 					for (q = ksprintn(nbuf, num, *p++, nullptr, 0); *q;)
+					{
 						putchar(*q--);
+					}
 
 					if (num == 0)
+					{
 						break;
+					}
 
 					for (tmp = 0; *p;)
 					{
@@ -252,15 +266,23 @@
 						{
 							putchar(tmp ? ',' : '<');
 							for (; (n = *p) > ' '; ++p)
+							{
 								putchar(n);
+							}
 							tmp = 1;
 						}
 						else
+						{
 							for (; *p > ' '; ++p)
+							{
 								continue;
+							}
+						}
 					}
 					if (tmp)
+					{
 						putchar('>');
+					}
 					break;
 				case 'c':
 					putchar(va_arg(ap, int));
@@ -269,15 +291,21 @@
 					up = va_arg(ap, unsigned char *);
 					p  = va_arg(ap, char *);
 					if (!width)
+					{
 						width = 16;
+					}
 					while (width--)
 					{
 						putchar(hex2ascii(*up >> 4));
 						putchar(hex2ascii(*up & 0x0f));
 						up++;
 						if (width)
+						{
 							for (q = p; *q; q++)
+							{
 								putchar(*q);
+							}
+						}
 					}
 					break;
 				case 'd':
@@ -292,7 +320,9 @@
 						cflag = 1;
 					}
 					else
+					{
 						hflag = 1;
+					}
 					goto reswitch; // NOLINT
 				case 'j':
 					jflag = 1;
@@ -304,23 +334,39 @@
 						qflag = 1;
 					}
 					else
+					{
 						lflag = 1;
+					}
 					goto reswitch; // NOLINT
 				case 'n':
 					if (jflag)
+					{
 						*(va_arg(ap, intmax_t *)) = retval;
+					}
 					else if (qflag)
+					{
 						*(va_arg(ap, long long *)) = retval;
+					}
 					else if (lflag)
+					{
 						*(va_arg(ap, long *)) = retval;
+					}
 					else if (zflag)
+					{
 						*(va_arg(ap, size_t *)) = retval;
+					}
 					else if (hflag)
+					{
 						*(va_arg(ap, short *)) = static_cast<short>(retval);
+					}
 					else if (cflag)
+					{
 						*(va_arg(ap, char *)) = retval;
+					}
 					else
+					{
 						*(va_arg(ap, int *)) = retval;
+					}
 					break;
 				case 'o':
 					base = 8;
@@ -338,8 +384,10 @@
 				case 'r':
 					base = radix;
 					if (sign)
+					{
 						goto handle_sign; // NOLINT
-					goto handle_nosign;   // NOLINT
+					}
+					goto handle_nosign; // NOLINT
 				case 's':
 					p = va_arg(ap, char *);
 					if (p == nullptr)
@@ -400,39 +448,71 @@
 				handle_nosign:
 					sign = 0;
 					if (jflag)
+					{
 						num = va_arg(ap, uintmax_t);
+					}
 					else if (qflag)
+					{
 						num = va_arg(ap, unsigned long long);
+					}
 					else if (tflag)
+					{
 						num = va_arg(ap, ptrdiff_t);
+					}
 					else if (lflag)
+					{
 						num = va_arg(ap, unsigned long);
+					}
 					else if (zflag)
+					{
 						num = va_arg(ap, size_t);
+					}
 					else if (hflag)
+					{
 						num = static_cast<unsigned short>(va_arg(ap, int));
+					}
 					else if (cflag)
+					{
 						num = static_cast<unsigned char>(va_arg(ap, int));
+					}
 					else
+					{
 						num = va_arg(ap, unsigned int);
+					}
 					goto number; // NOLINT
 				handle_sign:
 					if (jflag)
+					{
 						num = va_arg(ap, intmax_t);
+					}
 					else if (qflag)
+					{
 						num = va_arg(ap, long long);
+					}
 					else if (tflag)
+					{
 						num = va_arg(ap, ptrdiff_t);
+					}
 					else if (lflag)
+					{
 						num = va_arg(ap, long);
+					}
 					else if (zflag)
+					{
 						num = va_arg(ap, ssize_t);
+					}
 					else if (hflag)
+					{
 						num = static_cast<short>(va_arg(ap, int));
+					}
 					else if (cflag)
+					{
 						num = static_cast<char>(va_arg(ap, int));
+					}
 					else
+					{
 						num = va_arg(ap, int);
+					}
 				number:
 					if (sign && static_cast<intmax_t>(num) < 0)
 					{
@@ -444,22 +524,36 @@
 					if (sharpflag && num != 0)
 					{
 						if (base == 8)
+						{
 							tmp++;
+						}
 						else if (base == 16)
+						{
 							tmp += 2;
+						}
 					}
 					if (neg)
+					{
 						tmp++;
+					}
 
 					if (!ladjust && padc == '0')
+					{
 						dwidth = width - tmp;
+					}
 					width -= tmp + (dwidth > n ? dwidth : n);
 					dwidth -= n;
 					if (!ladjust)
+					{
 						while (width-- > 0)
+						{
 							putchar(' ');
+						}
+					}
 					if (neg)
+					{
 						putchar('-');
+					}
 					if (sharpflag && num != 0)
 					{
 						if (base == 8)
@@ -473,19 +567,29 @@
 						}
 					}
 					while (dwidth-- > 0)
+					{
 						putchar('0');
+					}
 
 					while (*p)
+					{
 						putchar(*p--);
+					}
 
 					if (ladjust)
+					{
 						while (width-- > 0)
+						{
 							putchar(' ');
+						}
+					}
 
 					break;
 				default:
 					while (percent < fmt)
+					{
 						putchar(*percent++);
+					}
 					/*
 					 * Since we ignore an formatting argument it is no
 					 * longer safe to obey the remaining formatting
@@ -524,7 +628,9 @@
 	};
 	int retval = kvprintf(format, callback, &info, 10, ap);
 	if (info.remain >= 1)
+	{
 		*info.str++ = '\0';
+	}
 	return (retval);
 }
 
diff --git a/sdk/lib/unwind_error_handler/unwind.S b/sdk/lib/unwind_error_handler/unwind.S
index 6e56a98..6c74c06 100644
--- a/sdk/lib/unwind_error_handler/unwind.S
+++ b/sdk/lib/unwind_error_handler/unwind.S
@@ -1,16 +1,29 @@
+#include <unwind-assembly.h>
+
+/**
+ * A direct re-implementation of unwind.h's cleanup_unwind() as a stackless
+ * error handler.
+ *
+ * If there is no registered CleanupList structure (equivalently, there's no
+ * CHERIOT_DURING block active at the time of the fault), then this requests
+ * unwnding out of the compartment.  Otherwise, we will longjmp() out to the
+ * indicated handler (that is, the CHERIOT_HANDLER block associated with the
+ * current CHERIOT_DURING block), having reset the compartment error handler
+ * invocation counter to zero.
+ */
 .section .compartment_error_handler_stackless,"aw",@progbits
 .globl compartment_error_handler_stackless
 .p2align 2
 .type compartment_error_handler_stackless,@function
 compartment_error_handler_stackless:
-// Get the head of the error list.
+// Get the head of the error list (see cleanup_list_head)
 	cgettop      t0, csp
 	csetaddr     csp, csp, t0
-	clc          cs0, -8(csp)
+	clc          cs0, -INVOCATION_LOCAL_UNWIND_LIST_OFFSET(csp)
 	beqz         s0, .Lforce_unwind
-// Pop the top error from the list. */
-	clc          ct0, 0(cs0)
-	csc          ct0, -8(csp)
+// Pop the top error from the list
+	clc          ct0, CleanupList_offset_next(cs0)
+	csc          ct0, -INVOCATION_LOCAL_UNWIND_LIST_OFFSET(csp)
 // Mark this error handler as having finished.  We may still trap again
 // and reenter this, but now that we've popped the top element from the
 // stack we will run some different cleanup code next time. */
@@ -19,11 +32,12 @@
 	clc             ct2, %cheriot_compartment_lo_i(.Llookup_reset)(ct2)
 	cjalr           ct2
 // longjmp to the error handler.
-	clc          cs1, 16(cs0)
-	clc          csp, 24(cs0)
-	clc          cra, 32(cs0)
-	clc          cs0, 8(cs0)
+	clc          cs1, (CleanupList_offset_env + __jmp_buf_offset___cs1)(cs0)
+	clc          csp, (CleanupList_offset_env + __jmp_buf_offset___csp)(cs0)
+	clc          cra, (CleanupList_offset_env + __jmp_buf_offset___cra)(cs0)
+	clc          cs0, (CleanupList_offset_env + __jmp_buf_offset___cs0)(cs0)
 	cjr          cra
+
 .Lforce_unwind:
 	li           a0, 1
 	cret
diff --git a/sdk/privileged-compartment.ldscript b/sdk/privileged-compartment.ldscript
index 9cb984f..c8f1b0a 100644
--- a/sdk/privileged-compartment.ldscript
+++ b/sdk/privileged-compartment.ldscript
@@ -17,17 +17,19 @@
 		# Array of compartment exports
 		*(.compartment_exports .compartment_exports.*);
 	}
+	# Reserve space at the start for privileged compartments that need special sealing keys.
+	.compartment_sealing_keys : ALIGN(8)
+	{
+		# Start of the compartment's PCC region
+		HIDDEN(__compartment_pcc_start = .);
+		# The sealing keys for this compartment is before the import table, if they exist
+		*(.sealing_key1*)
+		*(.sealing_key2*)
+	}
 	# Lay out the compartment imports section.  This will end up on PCC.
 	.compartment_import_table : ALIGN(8)
 	{
 		# Array of compartment imports 
-		HIDDEN(__compartment_pcc_start = .);
-		# The sealing key for this compartment is before the import table.
-		HIDDEN(__sealingkey = .);
-		. = . + 8;
-		# Space for a second sealing key, used only by the allocator.
-		HIDDEN(__sealingkey2 = .);
-		. = . + 8;
 		# The first import table entry is the compartment switcher.
 		HIDDEN(.compartment_switcher = .);
 		. = . + 8;
diff --git a/sdk/xmake.lua b/sdk/xmake.lua
index da170b7..0f26d6e 100644
--- a/sdk/xmake.lua
+++ b/sdk/xmake.lua
@@ -653,11 +653,9 @@
 				"\n\t\tSHORT(.software_revoker_end - .software_revoker_start);" ..
 				"\n\t\tLONG(.software_revoker_globals);" ..
 				"\n\t\tSHORT(SIZEOF(.software_revoker_globals));" ..
-				-- The import table offset is computed from the start by code
-				-- that assumes that the first two words are space for sealing
-				-- keys, so we set it to 16 here to provide a computed size of
-				-- 0.
-				"\n\t\tSHORT(16)" ..
+				-- The software revoker has no import table.
+				"\n\t\tLONG(0)" ..
+				"\n\t\tSHORT(0)" ..
 				"\n\t\tLONG(.software_revoker_export_table);" ..
 				"\n\t\tSHORT(.software_revoker_export_table_end - .software_revoker_export_table);\n" ..
 				"\n\t\tLONG(0);" ..
diff --git a/tests.extra/regress-thread_exit_IRQ/README.md b/tests.extra/regress-thread_exit_IRQ/README.md
new file mode 100644
index 0000000..e0e9f2f
--- /dev/null
+++ b/tests.extra/regress-thread_exit_IRQ/README.md
@@ -0,0 +1,6 @@
+This checks for a specific bug fixed in 2024/11, where it was possible to
+invoke the scheduler's exception entrypoint, which must run with IRQs deferred,
+with IRQs enabled if a thread exited from its initial activation via a slightly
+unusual path.
+
+See https://github.com/CHERIoT-Platform/cheriot-rtos/pull/346
diff --git a/tests.extra/regress-thread_exit_IRQ/helper.cc b/tests.extra/regress-thread_exit_IRQ/helper.cc
new file mode 100644
index 0000000..023b4fe
--- /dev/null
+++ b/tests.extra/regress-thread_exit_IRQ/helper.cc
@@ -0,0 +1,5 @@
+#include "helper.h"
+[[cheri::interrupt_state(enabled)]] void* help(void)
+{
+	return __builtin_return_address(0);
+}
diff --git a/tests.extra/regress-thread_exit_IRQ/helper.h b/tests.extra/regress-thread_exit_IRQ/helper.h
new file mode 100644
index 0000000..578659e
--- /dev/null
+++ b/tests.extra/regress-thread_exit_IRQ/helper.h
@@ -0,0 +1,2 @@
+#include <compartment.h>
+void* __cheri_compartment("helper") help(void);
diff --git a/tests.extra/regress-thread_exit_IRQ/top.cc b/tests.extra/regress-thread_exit_IRQ/top.cc
new file mode 100644
index 0000000..57087ce
--- /dev/null
+++ b/tests.extra/regress-thread_exit_IRQ/top.cc
@@ -0,0 +1,5 @@
+#include "helper.h"
+void __cheri_compartment("top") entry()
+{
+	asm volatile ("cmove cra, %0; cret" : : "C"(help()));
+}
diff --git a/tests.extra/regress-thread_exit_IRQ/xmake.lua b/tests.extra/regress-thread_exit_IRQ/xmake.lua
new file mode 100644
index 0000000..38462b2
--- /dev/null
+++ b/tests.extra/regress-thread_exit_IRQ/xmake.lua
@@ -0,0 +1,29 @@
+set_project("CHERIoT Scheduler IRQ Exception PoC")
+sdkdir = "../../sdk"
+includes(sdkdir)
+set_toolchains("cheriot-clang")
+
+option("board")
+    set_default("sail")
+
+compartment("helper")
+    add_files("helper.cc")
+
+compartment("top")
+    add_files("top.cc")
+
+firmware("top_compartment")
+    add_deps("freestanding", "debug")
+    add_deps("top", "helper")
+    on_load(function(target)
+        target:values_set("board", "$(board)")
+        target:values_set("threads", {
+            {
+                compartment = "top",
+                priority = 1,
+                entry_point = "entry",
+                stack_size = 0x200,
+                trusted_stack_frames = 1
+            }
+        }, {expand = false})
+    end)
diff --git a/tests/allocator-test.cc b/tests/allocator-test.cc
index 97f19c9..17faf66 100644
--- a/tests/allocator-test.cc
+++ b/tests/allocator-test.cc
@@ -666,7 +666,9 @@
 	  !array.is_valid(), "Allocating too large an array succeeded: {}", array);
 	array = heap_allocate_array(&t, MALLOC_CAPABILITY, 16, 2);
 	TEST(array.is_valid(), "Allocating array failed: {}", array);
-	TEST(array.length() == 32,
+	// If there's heap fragmentation, this may be rounded up to 40 because we
+	// can't use the 8 bytes after the end for another object.
+	TEST((array.length() >= 32) && (array.length() <= 40),
 	     "Allocating array returned incorrect length: {}",
 	     array);
 	ret = heap_free(MALLOC_CAPABILITY, array);
diff --git a/tests/ccompile-test.c b/tests/ccompile-test.c
index 7463b7c..da5401c 100644
--- a/tests/ccompile-test.c
+++ b/tests/ccompile-test.c
@@ -9,6 +9,7 @@
 #include <assert.h>
 #include <cdefs.h>
 #include <cheri-builtins.h>
+#include <cheri.h>
 #include <compartment.h>
 #include <ctype.h>
 #include <errno.h>
@@ -38,4 +39,4 @@
 #include <time.h>
 #include <timeout.h>
 #include <token.h>
-#include <cheri.h>
+#include <unwind.h>
diff --git a/tests/compartment_calls-test.cc b/tests/compartment_calls-test.cc
index 2f0cff1..a8ed1ee 100644
--- a/tests/compartment_calls-test.cc
+++ b/tests/compartment_calls-test.cc
@@ -22,26 +22,26 @@
 	int value = ConstantValue;
 
 	ret = compartment_call_inner(value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 
 	ret = compartment_call_inner(value, value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 
 	ret = compartment_call_inner(value, value, &value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 
 	ret = compartment_call_inner(value, value, &value, value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 
 	ret = compartment_call_inner(value, value, &value, value, &value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 
 	ret = compartment_call_inner(value, value, &value, value, &value, value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 
 	ret =
 	  compartment_call_inner(value, value, &value, value, &value, value, value);
-	TEST(ret == 0, "compartment_call_inner returend {}", ret);
+	TEST(ret == 0, "compartment_call_inner returned {}", ret);
 }
 
 int test_compartment_call()
diff --git a/tests/crash_recovery-test.cc b/tests/crash_recovery-test.cc
index 0254654..48dc278 100644
--- a/tests/crash_recovery-test.cc
+++ b/tests/crash_recovery-test.cc
@@ -10,9 +10,18 @@
 int               crashes = 0;
 std::atomic<bool> expectFault;
 
+static void test_irqs_are_enabled()
+{
+	void *r = __builtin_return_address(0);
+	TEST(__builtin_cheri_type_get(r) == CheriSealTypeReturnSentryEnabling,
+	     "Calling context has IRQs disabled");
+}
+
 extern "C" enum ErrorRecoveryBehaviour
 compartment_error_handler(struct ErrorState *frame, size_t mcause, size_t mtval)
 {
+	test_irqs_are_enabled();
+
 	crashes++;
 	if (mcause == 0x2)
 	{
diff --git a/tests/misc-test.cc b/tests/misc-test.cc
index f537067..dc09d77 100644
--- a/tests/misc-test.cc
+++ b/tests/misc-test.cc
@@ -170,12 +170,59 @@
 	     permissions);
 }
 
+// This test is somewhat intimately familiar with parameters of CHERIoT's
+// capability encoding and so might need revision if that changes.
+void check_capability_set_inexact_at_most()
+{
+	void *p = malloc(3128);
+
+	debug_log("Test Capability::BoundsProxy::set_inexact_at_most with {}", p);
+
+	// Too many bits for mantissa, regardless of base alignment
+	{
+		Capability<void> q      = {p};
+		size_t           reqlen = 2047;
+		q.bounds().set_inexact_at_most(reqlen);
+		debug_log("Requesting 2047 gives {}: {}", q.length(), q);
+		TEST(q.is_valid(), "set_inexact_at_most untagged");
+		TEST(q.length() < 2047, "set_inexact_at_most failed to truncate");
+		TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+	}
+
+	// Fits in mantissa, but not reachable from misaligned base
+	{
+		Capability<void> q = {p};
+		q.address() += 2;
+		size_t reqlen = 1024;
+		q.bounds().set_inexact_at_most(reqlen);
+		debug_log("Requesting 1024 at align 2 gives {}: {}", q.length(), q);
+		TEST(q.is_valid(), "set_inexact_at_most untagged");
+		TEST(q.length() < 1024, "set_inexact_at_most failed to truncate");
+		TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+	}
+
+	// Fits in mantissa and reachable from misaligned base
+	{
+		Capability<void> q = {p};
+		q.address() += 1;
+		size_t reqlen = 511;
+		q.bounds().set_inexact_at_most(reqlen);
+		debug_log("Requesting 511 at align 1 gives {}: {}", q.length(), q);
+		TEST(q.is_valid(), "set_inexact_at_most untagged");
+		TEST(q.length() == 511, "set_inexact_at_most truncated unnecessarily");
+		TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+	}
+
+	free(p);
+}
+
 int test_misc()
 {
 	check_timeouts();
 	check_memchr();
 	check_memrchr();
 	check_pointer_utilities();
+	check_capability_set_inexact_at_most();
 	debug_log("Testing shared objects.");
 	check_shared_object("exampleK",
 	                    SHARED_OBJECT(void, exampleK),
diff --git a/tests/multiwaiter-test.cc b/tests/multiwaiter-test.cc
index d0f380f..d9d99e9 100644
--- a/tests/multiwaiter-test.cc
+++ b/tests/multiwaiter-test.cc
@@ -70,16 +70,14 @@
 	TEST(events[0].value == 0, "Futex reports wake but none occurred");
 	TEST(events[1].value == 1, "Futex reports no wake");
 
-	QueueHandle queue;
-	void       *queueMemory;
+	MessageQueue *queue;
 	t.remaining = 0;
-	ret =
-	  queue_create(&t, MALLOC_CAPABILITY, &queue, &queueMemory, sizeof(int), 1);
+	ret         = queue_create(&t, MALLOC_CAPABILITY, &queue, sizeof(int), 1);
 
 	TEST(ret == 0, "Queue create failed:", ret);
 	int     val = 0;
 	Timeout noWait{0};
-	ret = queue_send(&noWait, &queue, &val);
+	ret = queue_send(&noWait, queue, &val);
 	TEST(ret == 0, "Queue send failed: {}", ret);
 
 	debug_log("Testing queue, blocked on send");
@@ -87,12 +85,12 @@
 		sleep(1);
 		int     val;
 		Timeout noWait{0};
-		int     ret = queue_receive(&noWait, &queue, &val);
+		int     ret = queue_receive(&noWait, queue, &val);
 		TEST(ret == 0, "Background receive failed: {}", ret);
 		TEST(val == 0, "Background receive returned incorrect value: {}", ret);
 		debug_log("Background thread made queue ready to send");
 	});
-	multiwaiter_queue_send_init(&events[0], &queue);
+	multiwaiter_queue_send_init(&events[0], queue);
 	t.remaining = 6;
 	ret         = multiwaiter_wait(&t, mw, events, 1);
 	TEST(ret == 0, "multiwaiter returned {}, expected 0", ret);
@@ -103,23 +101,23 @@
 		sleep(1);
 		int     val = 1;
 		Timeout noWait{0};
-		int     ret = queue_send(&noWait, &queue, &val);
+		int     ret = queue_send(&noWait, queue, &val);
 		TEST(ret == 0, "Background send failed: {}", ret);
 		debug_log("Background thread made queue ready to receive");
 	});
-	multiwaiter_queue_receive_init(&events[0], &queue);
+	multiwaiter_queue_receive_init(&events[0], queue);
 	t   = 10;
 	ret = multiwaiter_wait(&t, mw, events, 1);
 	TEST(ret == 0, "multiwaiter returned {}, expected 0", ret);
 	TEST(events[0].value == 1, "Queue did not return ready to receive");
-	ret = queue_receive(&noWait, &queue, &val);
+	ret = queue_receive(&noWait, queue, &val);
 	TEST(ret == 0, "Queue ready to receive but receive returned {}", ret);
 	TEST(val == 1, "Incorrect value returned from queue: {}", val);
 
 	debug_log("Testing waiting on a queue and a futex");
 	futex = 0;
 	setFutex(&futex, 1);
-	multiwaiter_queue_receive_init(&events[0], &queue);
+	multiwaiter_queue_receive_init(&events[0], queue);
 	events[1]   = {&futex, EventWaiterFutex, 0};
 	t.remaining = 6;
 	ret         = multiwaiter_wait(&t, mw, events, 2);
@@ -128,7 +126,6 @@
 	     "Queue reports ready to receive but should be empty.");
 	TEST(events[1].value == 1, "Futex reports no wake");
 
-	free(queueMemory);
 	multiwaiter_delete(MALLOC_CAPABILITY, mw);
 	return 0;
 }
diff --git a/tests/queue-test.cc b/tests/queue-test.cc
index da18b87..b8c36dc 100644
--- a/tests/queue-test.cc
+++ b/tests/queue-test.cc
@@ -4,7 +4,7 @@
 #include "compartment.h"
 #include "token.h"
 #include <cstdlib>
-#define TEST_NAME "Queue"
+#define TEST_NAME "MessageQueue"
 #include "tests.hh"
 #include <FreeRTOS-Compat/queue.h>
 #include <debug.hh>
@@ -28,77 +28,76 @@
 
 void test_queue_unsealed()
 {
-	char               bytes[ItemSize];
-	static QueueHandle queue;
-	static void       *queueMemory;
-	Timeout            timeout{0, 0};
+	char                 bytes[ItemSize];
+	static MessageQueue *queue;
+	Timeout              timeout{0, 0};
 	debug_log("Testing queue send operations");
 	auto checkSpace = [&](size_t         expected,
 	                      SourceLocation loc = SourceLocation::current()) {
 		size_t items;
-		queue_items_remaining(&queue, &items);
+		queue_items_remaining(queue, &items);
 		TEST(items == expected,
-		     "Queue test line {} reports {} items, should contain {}",
+		     "MessageQueue test line {} reports {} items, should contain {}",
 		     loc.line(),
 		     items,
 		     expected);
 	};
-	int rv = queue_create(
-	  &timeout, MALLOC_CAPABILITY, &queue, &queueMemory, ItemSize, MaxItems);
-	TEST(queue.elementSize == ItemSize,
-	     "Queue element size is {}, expected {}",
-	     queue.elementSize,
+	int rv =
+	  queue_create(&timeout, MALLOC_CAPABILITY, &queue, ItemSize, MaxItems);
+	TEST(queue->elementSize == ItemSize,
+	     "MessageQueue element size is {}, expected {}",
+	     queue->elementSize,
 	     ItemSize);
-	TEST(queue.queueSize == MaxItems,
-	     "Queue size is {}, expected {}",
-	     queue.queueSize,
+	TEST(queue->queueSize == MaxItems,
+	     "MessageQueue size is {}, expected {}",
+	     queue->queueSize,
 	     MaxItems);
-	TEST(rv == 0, "Queue creation failed with {}", rv);
-	rv = queue_send(&timeout, &queue, Message[0]);
+	TEST(rv == 0, "MessageQueue creation failed with {}", rv);
+	rv = queue_send(&timeout, queue, Message[0]);
 	checkSpace(1);
 	TEST(rv == 0, "Sending the first message failed with {}", rv);
 	checkSpace(1);
-	rv = queue_send(&timeout, &queue, Message[1]);
+	rv = queue_send(&timeout, queue, Message[1]);
 	TEST(rv == 0, "Sending the second message failed with {}", rv);
 	checkSpace(2);
-	// Queue is full, it should time out.
+	// MessageQueue is full, it should time out.
 	timeout.remaining = 5;
-	rv                = queue_send(&timeout, &queue, Message[1]);
+	rv                = queue_send(&timeout, queue, Message[1]);
 	TEST(rv == -ETIMEDOUT,
 	     "Sending to a full queue didn't time out as expected, returned {}",
 	     rv);
 	checkSpace(2);
 	debug_log("Testing queue receive operations");
 	timeout.remaining = 10;
-	rv                = queue_receive(&timeout, &queue, bytes);
+	rv                = queue_receive(&timeout, queue, bytes);
 	TEST(rv == 0, "Receiving the first message failed with {}", rv);
 	TEST(memcmp(Message[0], bytes, ItemSize) == 0,
 	     "First message received but not as expected. Got {}",
 	     bytes);
 	checkSpace(1);
-	rv = queue_receive(&timeout, &queue, bytes);
+	rv = queue_receive(&timeout, queue, bytes);
 	TEST(rv == 0, "Receiving the second message failed with {}", rv);
 	TEST(memcmp(Message[1], bytes, ItemSize) == 0,
 	     "Second message received but not as expected. Got {}",
 	     bytes);
 	checkSpace(0);
 	timeout.remaining = 5;
-	rv                = queue_receive(&timeout, &queue, bytes);
+	rv                = queue_receive(&timeout, queue, bytes);
 	TEST(
 	  rv == -ETIMEDOUT,
 	  "Receiving from an empty queue didn't time out as expected, returned {}",
 	  rv);
 	// Check that the items remaining calculations are correct after overflow.
-	queue_send(&timeout, &queue, Message[1]);
+	queue_send(&timeout, queue, Message[1]);
 	checkSpace(1);
-	queue_receive(&timeout, &queue, bytes);
+	queue_receive(&timeout, queue, bytes);
 	checkSpace(0);
-	queue_send(&timeout, &queue, Message[1]);
+	queue_send(&timeout, queue, Message[1]);
 	checkSpace(1);
-	queue_receive(&timeout, &queue, bytes);
+	queue_receive(&timeout, queue, bytes);
 	checkSpace(0);
-	rv = queue_destroy(MALLOC_CAPABILITY, &queue);
-	TEST(rv == 0, "Queue deletion failed with {}", rv);
+	rv = queue_destroy(MALLOC_CAPABILITY, queue);
+	TEST(rv == 0, "MessageQueue deletion failed with {}", rv);
 	debug_log("All queue library tests successful");
 }
 
@@ -108,10 +107,18 @@
 	Timeout t{1};
 	SObj    receiveHandle;
 	SObj    sendHandle;
+	SObj    queue;
 	char    bytes[ItemSize];
-	int     ret = queue_create_sealed(
-	      &t, MALLOC_CAPABILITY, &sendHandle, &receiveHandle, ItemSize, MaxItems);
-	TEST(ret == 0, "Queue creation failed with {}", ret);
+	int     ret =
+	  queue_create_sealed(&t, MALLOC_CAPABILITY, &queue, ItemSize, MaxItems);
+	TEST(ret == 0, "MessageQueue creation failed with {}", ret);
+	ret = queue_receive_handle_create_sealed(
+	  &t, MALLOC_CAPABILITY, queue, &receiveHandle);
+	TEST(
+	  ret == 0, "MessageQueue receive endpoint creation failed with {}", ret);
+	ret = queue_send_handle_create_sealed(
+	  &t, MALLOC_CAPABILITY, queue, &sendHandle);
+	TEST(ret == 0, "MessageQueue send endpoint creation failed with {}", ret);
 
 	t   = UnlimitedTimeout;
 	ret = queue_send_sealed(&t, receiveHandle, Message[1]);
@@ -159,11 +166,14 @@
 
 	t   = 1;
 	ret = queue_destroy_sealed(&t, MALLOC_CAPABILITY, sendHandle);
-	TEST(ret == 0, "Queue send destruction failed with {}", ret);
+	TEST(ret == 0, "MessageQueue send destruction failed with {}", ret);
 
 	t   = 1;
 	ret = queue_destroy_sealed(&t, MALLOC_CAPABILITY, receiveHandle);
-	TEST(ret == 0, "Queue receive destruction failed with {}", ret);
+	TEST(ret == 0, "MessageQueue receive destruction failed with {}", ret);
+
+	ret = queue_destroy_sealed(&t, MALLOC_CAPABILITY, queue);
+	TEST(ret == 0, "MessageQueue destruction failed with {}", ret);
 
 	TEST(heap_quota_remaining(MALLOC_CAPABILITY) == heapSpace,
 	     "Heap space leaked");
diff --git a/tests/stack-test.cc b/tests/stack-test.cc
index c814bf9..b3b894f 100644
--- a/tests/stack-test.cc
+++ b/tests/stack-test.cc
@@ -150,6 +150,12 @@
 	expect_handler(false);
 	exhaust_thread_stack();
 
+	debug_log("exhausting the compartment stack during a switcher call");
+	expect_handler(false);
+	threadStackTestFailed = true;
+	exhaust_thread_stack_spill(callback);
+	TEST(threadStackTestFailed == false, "switcher did not return error");
+
 	debug_log("modifying stack permissions on fault");
 	PermissionSet compartmentStackPermissions = get_stack_permissions();
 	for (auto permissionToRemove : compartmentStackPermissions)
diff --git a/tests/stack_integrity_thread.cc b/tests/stack_integrity_thread.cc
index 7a629c5..c897432 100644
--- a/tests/stack_integrity_thread.cc
+++ b/tests/stack_integrity_thread.cc
@@ -94,6 +94,40 @@
 	TEST(false, "Should be unreachable");
 }
 
+/**
+ * Arrange to exhaust the stack inside the cross-compartment switcher's spill of
+ * callee-saved state.  The result should simply be an error return, rather than
+ * a forced-unwind.
+ */
+void exhaust_thread_stack_spill(__cheri_callback void (*fn)())
+{
+	register auto      rfn asm("ct1") = fn;
+	register uintptr_t res asm("ca0") = 0;
+
+	__asm__ volatile(
+	  // Save the stack to put back later
+	  "cmove     cs0, csp\n"
+
+	  // Shrink the available stack space
+	  "cgetbase  s1, csp\n"
+	  "addi      s1, s1, %[stackleft]\n"
+	  "csetaddr  csp, csp, s1\n"
+
+	  // Make the call
+	  "1:\n"
+	  "auipcc ct2, %%cheriot_compartment_hi(.compartment_switcher)\n"
+	  "clc ct2, %%cheriot_compartment_lo_i(1b)(ct2)\n"
+	  "cjalr ct2\n"
+
+	  "cmove     csp, cs0\n"
+	  : /* outs */ "+C"(res)
+	  : /* ins */[stackleft] "i"(sizeof(void *))
+	  : /* clobbers */ "ct2", "cs0", "cs1");
+
+	*threadStackTestFailed = false;
+	TEST(res == -ENOTENOUGHSTACK, "Bad return {}", res);
+}
+
 void set_csp_permissions_on_fault(PermissionSet newPermissions)
 {
 	__asm__ volatile(
diff --git a/tests/stack_tests.h b/tests/stack_tests.h
index fbc757b..93ad94b 100644
--- a/tests/stack_tests.h
+++ b/tests/stack_tests.h
@@ -8,6 +8,8 @@
   __cheri_callback void (*fn)(),
   bool *outLeakedSwitcherCapability);
 __cheri_compartment("stack_integrity_thread") void exhaust_thread_stack();
+__cheri_compartment("stack_integrity_thread") void exhaust_thread_stack_spill(
+  __cheri_callback void (*fn)());
 __cheri_compartment("stack_integrity_thread") void set_csp_permissions_on_fault(
   PermissionSet newPermissions);
 __cheri_compartment("stack_integrity_thread") void set_csp_permissions_on_call(
diff --git a/tests/static_sealing-test.cc b/tests/static_sealing-test.cc
index 046d704..09a7407 100644
--- a/tests/static_sealing-test.cc
+++ b/tests/static_sealing-test.cc
@@ -19,6 +19,5 @@
 {
 	// Get a pointer to it and ask for it to be unsealed.
 	Sealed<TestType> value{STATIC_SEALED_VALUE(test)};
-	test_static_sealed_object(value);
-	return 0;
+	return test_static_sealed_object(value);
 }
diff --git a/tests/static_sealing.h b/tests/static_sealing.h
index 5a3402b..99858dd 100644
--- a/tests/static_sealing.h
+++ b/tests/static_sealing.h
@@ -10,5 +10,5 @@
 	int value;
 };
 
-void __cheri_compartment("static_sealing_inner")
+int __cheri_compartment("static_sealing_inner")
   test_static_sealed_object(Sealed<TestType>);
diff --git a/tests/static_sealing_inner.cc b/tests/static_sealing_inner.cc
index 872bf6f..b8d56a7 100644
--- a/tests/static_sealing_inner.cc
+++ b/tests/static_sealing_inner.cc
@@ -4,10 +4,11 @@
 #define TEST_NAME "Static sealing (inner compartment)"
 #include "static_sealing.h"
 #include "tests.hh"
+#include <fail-simulator-on-error.h>
 
 using namespace CHERI;
 
-void test_static_sealed_object(Sealed<TestType> obj)
+int test_static_sealed_object(Sealed<TestType> obj)
 {
 	// Get our static sealing key.
 	SKey       key = STATIC_SEALING_TYPE(SealingType);
@@ -48,4 +49,5 @@
 	                                  Permission::Global}>(unsealed, 1)),
 	     "Incorrect permissions on unsealed statically sealed object {}",
 	     unsealed);
+	return 0;
 }
diff --git a/tests/test-runner.cc b/tests/test-runner.cc
index 0c85f14..c9f3acb 100644
--- a/tests/test-runner.cc
+++ b/tests/test-runner.cc
@@ -24,7 +24,7 @@
 		// On Sail, report the number of instructions, the cycle count is
 		// meaningless.
 		__asm__ volatile("csrr %0, minstret" : "=r"(cycles));
-#elifdef IBEX
+#elif defined(IBEX)
 		__asm__ volatile("csrr %0, mcycle" : "=r"(cycles));
 #else
 		__asm__ volatile("rdcycle %0" : "=r"(cycles));
@@ -54,7 +54,9 @@
 			crashDetected = true;
 		}
 		else
+		{
 			debug_log("{} finished in {} cycles", msg, cycles - startCycles);
+		}
 	}
 } // namespace