CHERI
CHERI capabilities, with their permissions and region bound addresses, embedded significantly more information than a simple integer pointer. As a result, their memory footprint is also significant. For this reason, effort has been spent into researching a compressed CHERI capability format to reduce this memory footprint.
To achieve this goal, the main approach has been to leverage the observation that the address pointed at and the top and base addresses of the covered region will share upper bits, scaling with the size of the covered region. This enables us to store only one full integer address, and use techniques akin to floating point to re-derive the other two, with minimal alignement requirement trade-offs.
Departure from historical CHERI 256-bit format
Foundational work
CHERI was initially developed using a 256-bit format capable of storing a full 64-bit address, 64-bit base and 64-bit length as well as other metadata. The significant memory footprint of these capabilities motivated research into a potential compressed CHERI capability format.
Initial design space exploration for compression of capability bounds was conducted in High-performance memory safety: optimizing the CHERI capability machine, with multiple exploratory prototypes developed in the L3 MIPS model. Early mentions of this research are found in the CHERI Instruction-Set Architecture document from September 2015, with later versions of the document being updated as the research gets refined. Further optimisations of a compressed format were also explored in Capability memory protection for embedded systems, also leveraging the compression technique in the context of small 64-bit capabilities with 32-bit addresses.
CHERI Concentrate
The CHERI Concentrate format from CHERI Concentrate: Practical Compressed Capabilities crystallised the research conducted to compress CHERI capabilities. In this publication, we mention HOL4 artifacts which we constructed to serve as proofs:
With the appropriate packages installed, these proofs can be run using Holmake:
Holmake boundsTheory.uo
Holmake compressTheory.uo
The techniques in use for CHERI capability compression in CHERI Concentrate support both 128-bit capabilities with 64-bit addresses and 64-bit capabilities with 32-bit addresses.
Current CHERI architectures
The historical work towards CHERI concentrate was conducted on the MIPS architecture.
Today, CHERI's development has shifted to the RISC-V architecture (see CHERI-RISC-V), with a RISC-V extension under ratification.
There also exists an Arm-based platform supporting CHERI: Morello (see Arm Morello), with a publicly available specification document.
The compression formats present in these new architectures are implementing the same core compressions techniques from this stream of research, especially for bounds compression.