spike-impl.adoc

Spike Implementation of the Capstone-RISC-V ISA

Compressed Capability Format

• If the type field of the capability is 0 (linear), 1 (non-linear), 2 (revocation) or 3 (uninitialised):

Figure 1. capability format for linear, non-linear, revocation and uninitialised capabilities

• If the type field of the capability is 4 (sealed), 5 (sealed-return), 6 (exit):

Figure 2. capability format for sealed, sealed-return and exit capabilities

Fields and Compression Mechanism

The relation between the fields of the capability and bits of the compressed capability format is shown in the following table:

Table 1. Decoding correspondence of linear, non-linear, revocation and uninitialized capability format

Field	Bits	Compressed	Additional Data Structure
valid	node-id	-	Revocation Tree
type	type	No	-
cursor	cursor	No	-
base	bound	Yes	-
end	bound	Yes	-
perms	perm	No	-

Note: the compression mechanism of the format

The compression mechanism of the base and end fields is the same as the one used in the compressed capability format of the CHERI ISAv8.

Table 2. Decoding correspondence of sealed, sealed-return and exit capability format

Field	Bits	Compressed	Additional Data Structure
valid	node-id	-	Revocation Tree
type	type	No	-
cursor	offset, base	Yes	-
base	base	No	-
async	async	No	-
reg	reg	No	-

Note: the compression mechanism of the format

The compression mechanism of the cursor field is straightforward: cursor = sign_extend(offset) + base.

Implementation of the valid field

In Spike, an additional data structure called revocation tree is used to maintain the valid field of the capability. The idea of the revocation tree is introduced in our USENIX Security '23 paper. In the compressed capability format, a node-id is kept as part of the capability to indicate a node in the revocation tree. A reference count is maintained for each node in the revocation tree to indicate the number of capabilities that are currently pointing to the node. <t relation is maintained as a partial order on the revocation tree to indicate the revocation order of the capabilities. An Insufficient system resources (30) exception will be raised if the allocation of a new node in the revocation tree fails.