Caplifive Released
What Is Capstone?
Capstone is a new capability-based instruction set architecture (ISA) that provides a unified hardware-software interface to support a wide range of security features, including spatial and temporal memory safety, enclaved trusted execution environments, and extensible privilege hierarchies.
@inproceedings {yu2023capstone,
author = {Jason Zhijingcheng Yu and Conrad Watt and Aditya Badole and Trevor E. Carlson and Prateek Saxena},
title = {Capstone: A Capability-based Foundation for Trustless Secure Memory Access},
booktitle = {32nd USENIX Security Symposium (USENIX Security 23)},
year = {2023},
isbn = {978-1-939133-37-3},
address = {Anaheim, CA},
pages = {787--804},
url = {https://www.usenix.org/conference/usenixsecurity23/presentation/yu-jason},
publisher = {USENIX Association},
month = aug,
}
Projects
Capstone includes several sub-projects listed below. Click for more information.
├── Capstone ▼
Capability-based memory isolation is a promising new architectural primitive. Software can access low-level memory only via capability handles rather than raw pointers, which provides a natural interface to enforce security restrictions. Existing architectural capability designs such as CHERI provide spatial safety, but fail to extend to other memory models that security-sensitive software designs may desire. In this paper, we propose Capstone, a more expressive architectural capability design that supports multiple existing memory isolation models in a trustless setup, i.e., without relying on trusted software components. We show how Capstone is well-suited for environments where privilege boundaries are fluid (dynamically extensible), memory sharing/delegation are desired both temporally and spatially, and where such needs are to be balanced with availability concerns. Capstone can also be implemented efficiently. We present an implementation sketch and through evaluation show that its overhead is below 50% in common use cases. We also prototype a functional emulator for Capstone and use it to demonstrate the runnable implementations of six real-world memory models without trusted software components: three types of enclave-based TEEs, a thread scheduler, a memory allocator, and Rust-style memory safety—all within the interface of Capstone.
Resources
├── Caplifive ▼
Permission-based access control on virtual memory references are the predominant way for hardware to enforce isolation in existing systems. Hardware capabilities offer an alternative to virtual memory access control (or VMAC). It promises context independence and reduces trusted ambient authorities compared to VMAC. Despite its conceptual strengths, it is challenging for existing capability-based designs to provide compatibility and interoperability for existing VMAC-based software stacks, hindering their adoption. Prior attempts to bridge the gap between capabilities and VMAC sacrifice the inherent strengths of capabilities and require substantial changes to existing software stacks. They predominantly rely on what we call virtual-memory-backed capabilities (VMBC) which exposes capability abstractions directly to VMAC-based software. In contrast, this paper proposes the idea of caplification, which adapts memory protection data structures to translate VMAC-based memory accesses into capability-based ones. This brings the benefits of capability-based isolation to VMAC-based software stacks and enables incremental adoption of the capability-based programming model. We concretize the idea of caplification in CapliFive, a hardware and software design that achieves compatibility and interoperability between capabilities and VMAC. It provides capability-based isolation primitives for software across an existing VMAC-based software stack while requiring only minimal local changes. Our prototype implementation and case studies demonstrate the benefits CapliFive brings to VMAC-based software, including nestable two-way isolated sandboxing and lower communication overhead. CapliFive also enables incremental adoption of a pure capability-based model.
Resources
├── CapsLock ▼
The Rust programming language enforces three basic Rust principles, namely ownership, borrowing, and AXM (Aliasing Xor Mutability) to prevent security bugs such as memory safety violations and data races. However, Rust projects often have mixed code, i.e., code that also uses unsafe Rust, FFI (Foreign Function Interfaces), and inline assembly for low-level control. The Rust compiler is unable to statically enforce Rust principles in mixed Rust code which can lead to many security vulnerabilities. In this paper, we propose CapsLock, a security enforcement mechanism that can run at the level of machine code and detect Rust principle violations at run-time in mixed code. CapsLock is kept simple enough to be implemented into recent capability-based hardware abstractions that provide low-cost spatial memory safety. CapsLock introduces a novel revoke-on-use mechanism for capability-based designs, wherein accessing a memory object via a capability implicitly invalidates certain other capabilities pointing to it, thereby also providing temporal memory safety automatically, without requiring software to explicitly specify such invalidation. Thus, CapsLock is the first mechanism capable of providing cross-language enforcement of Rust principles. We implemented a prototype of CapsLock on QEMU. Evaluation results show that CapsLock is highly compatible with existing Rust code (capable of passing 95.5% of the built-in test cases of the 100 most popular crates) and flags Rust principle violations in real-world Rust projects that use FFI or inline assembly. We discovered 8 previously unknown bugs in such crates in our experiments.
Resources
├── AnvilHDL ▼
Hardware description languages (HDLs) are crucial to hardware designs and face unique challenges due to the characteristics that differentiate hardware from software. Hardware designs compute on stateless signals which change with their underlying registers. Popular HDLs do not provide support for stable (unchanged) values and leave it entirely to the hardware designer to decide whether a value remains unchanged. At the same time, hardware systems are typically highly parallel, involving multiple modules communicating with one another through shared signals. When designed with existing HDLs, the communicating modules lack an explicit contract on these shared signals. This makes timing hazards common during the hardware design process, where one module mutates a register, while another module still expects a value that depends on it to remain stable. In this work, we propose Anvil, an HDL which prevents such timing hazards while providing cycle-level timing control and support for expressing designs with dynamic timing behaviours. Anvil provides a type system that captures the timing characteristics of register mutations and value use, and statically enforces that registers are never mutated when dependent values still need to be stable. Across modules that may share values, Anvil provides safe composition guarantees by capturing the timing constraints on the shared values in a timing contract. The timing contract in Anvil is dynamic in the sense that it allows the latency of a signal to vary during run-time. We implement Anvil and show its safety and expressiveness with four hardware designs implemented in Anvil.
Resources
News
RISC-V Security HC Meeting Talk Slides
Capstone Specification Released
Contribute to Capstone
We welcome the community to contribute to Capstone. Please feel free to submit a pull request or open an issue on our GitHub repositories. You are also welcome to chat on our forum or directly contact us via email.