CHERI Concentrate: Practical Compressed Capabilities

We present CHERI Concentrate, a new fat-pointer compression scheme applied to CHERI, the most developed capability-pointer system at present. Capability fat pointers are a primary candidate to enforce fine-grained and non-bypassable security properties in future computer systems, although increased...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computers 2019-10, Vol.68 (10), p.1455-1469
Main Authors: Woodruff, Jonathan, Joannou, Alexandre, Xia, Hongyan, Fox, Anthony, Norton, Robert M., Chisnall, David, Davis, Brooks, Gudka, Khilan, Filardo, Nathaniel W., Markettos, A. Theodore, Roe, Michael, Neumann, Peter G., Watson, Robert N. M., Moore, Simon W.
Format: Article
Language:English
Subjects:
Capabilities
compression
computer architecture
Delay
Delays
Encoding
fat pointers
Format
memory safety
Microprocessors
Pipelines
Quantitative analysis
Registers
RISC
Safety
Semantics
Software
Source code
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present CHERI Concentrate, a new fat-pointer compression scheme applied to CHERI, the most developed capability-pointer system at present. Capability fat pointers are a primary candidate to enforce fine-grained and non-bypassable security properties in future computer systems, although increased pointer size can severely affect performance. Thus, several proposals for capability compression have been suggested elsewhere that do not support legacy instruction sets, ignore features critical to the existing software base, and also introduce design inefficiencies to RISC-style processor pipelines. CHERI Concentrate improves on the state-of-the-art region-encoding efficiency, solves important pipeline problems, and eases semantic restrictions of compressed encoding, allowing it to protect a full legacy software stack. We present the first quantitative analysis of compiled capability code, which we use to guide the design of the encoding format. We analyze and extend logic from the open-source CHERI prototype processor design on FPGA to demonstrate encoding efficiency, minimize delay of pointer arithmetic, and eliminate additional load-to-use delay. To verify correctness of our proposed high-performance logic, we present a HOL4 machine-checked proof of the decode and pointer-modify operations. Finally, we measure a 50 to 75 percent reduction in L2 misses for many compiled C-language benchmarks running under a commodity operating system using compressed 128-bit and 64-bit formats, demonstrating both compatibility with and increased performance over the uncompressed, 256-bit format.
ISSN:0018-9340
1557-9956
DOI:10.1109/TC.2019.2914037