Capability Architecture

Overview

A capability architecture is a computer system design in which memory references are represented as capabilities: unforgeable, bounded tokens that combine an address with permissions (and typically bounds, type, and validity metadata). Capabilities are used to enforce fine-grained memory access control, support software compartmentalization, and provide strong memory-safety primitives at the hardware level. The capability-architecture concept subsumes a family of concrete designs, including the CHERI capability-system architecture, capability-enhanced instruction-set extensions for RISC-V and Arm, and token-capability approaches for embedded platforms.

Definition and Core Properties

A capability architecture associates each protected reference with hardware-checked metadata so that any memory access must be authorized by a capability rather than by an arbitrary address. Common architectural ingredients include:

A capability representation (often a fat pointer carrying bounds, permissions, and a tag bit).
Architectural state (registers, instruction encodings) that propagate and transform capabilities under hardware enforcement.
Compiler and runtime support for deriving, restricting, and revoking capabilities.
Operating-system and hypervisor support for partitioning address spaces and isolating software components.

Capability architectures are typically described as hybrid when they extend an existing commodity ISA (e.g., RISC-V or AArch64) with capability extensions rather than replacing it.

Notable Capability Architectures

CHERI — A hybrid capability-system architecture that introduces capability-based protection for scalable software compartmentalization (Watson et al., 2015).
RV-CURE — A RISC-V capability architecture that implements full-system memory safety through a data-pointer tagging (DPT) compiler technique and lightweight BOOM-based hardware extensions. Reported SPEC 2017 C/C++ slowdown is 10.8% with strong memory-safety guarantees, evaluated on an FPGA prototype running Linux.
Morello — A capability-enhanced prototype Arm architecture, the subject of formal verification efforts demonstrating the feasibility of verified security for capability hardware (Bauereiss et al., 2021).
Embedded/RTOS token capabilities — A capability architecture for embedded systems that combines a token-capability approach suitable for untrusted OS construction with protections against malicious peripherals, evaluated on an FPGA around legacy hardware components.

Threat Model and Use Cases

Capability architectures have been proposed to address several classes of vulnerability:

Memory safety violations in application and system software, which remain persistent despite decades of mitigation effort.
Software compartmentalization, where mutually distrustful components must be isolated within a single address space.
Embedded-device threats spanning application bugs, OS-kernel bugs, and malicious peripherals; recent designs aim to cover all three vectors simultaneously.

Formal Verification of Capability Architectures

Because capability hardware mediates security-critical invariants, several capability-architecture designs have been targets of formal verification and ISA-specification research, including:

End-to-end formal verification of a RISC-V processor extended with capability pointers (Gao, FMCAD 2021).
Verified security for the Morello capability-enhanced prototype Arm architecture (Bauereiss, UCAM 2021).
ISA-specification and machine-verification techniques that provide building blocks for formally specifying capability instructions.

These efforts use architectural semantics frameworks (operational ARMv8 models, executable x86 simulators, CakeML verified compilation, and validated ISA models) to reason about the soundness of capability enforcement.

Design Considerations

Across concrete designs, recurring design considerations include:

Performance overhead vs. memory-safety coverage (RV-CURE reports ~10.8% SPEC 2017 slowdown while enforcing capability checks on every tagged-pointer access).
Hardware integration cost, e.g., implementing a capability-execution pipeline in parallel with the existing memory-execution pipeline to avoid intrusive modifications.
Compatibility with existing ISAs, toolchains, and OSes, motivating hybrid extensions over clean-slate designs.
TCB minimization, particularly in embedded settings where subsystems (scheduler, allocator, DMA drivers, peripherals) are treated as fully untrusted components.