How Can Capability Systems Make Computers Safer?

TL;DR

Capability-based hardware can make computer systems more trustworthy by replacing ordinary pointers with protected, non-forgeable references that carry bounds and access attributes. Combined with virtual memory, efficient domain crossing, formal analysis, and fine-grained compartmentalization, this architecture can isolate vulnerable code and limit what compromised components or malicious attachments are able to affect.

Transcript

Um, I wanted to begin with a little background. And in particular, um, some of the nasty stuff that, uh, is going on, uh, recently. And then I'll go into some slides on the work that we've been doing for the past, uh, four and a half years. Um, the first comment is that, uh, as was said, I am a, uh, system-oriented person. I'm delighted to see some... Read More

Key Insights

• Computer security currently has weakness in both breadth and depth because components, systems, and networking can each become weak links. Spending heavily to install complex information systems can therefore lead to further spending merely to protect the resulting infrastructure and sensitive information.
• Fine-grained compartmentalization limits damage by placing vulnerable operations, such as decompression code, into separate domains. If the isolated code is compromised, its restricted privileges and separation can prevent it from interfering with the application’s main loop or unrelated parts of the system.
• Application isolation can be adapted to the threat model rather than imposed in one fixed arrangement. A mail system might isolate every message, place all attachments in a sandbox, or separate networking functions such as HTTP, FTP, and SSL into distinct compartments.
• Existing software-only compartmentalization has practical limits because hardware that was not designed for security restricts how many compartments can be created and what those compartments can do. Earlier approaches also made granular memory protection and software compartmentalization inefficient, inadequate, or difficult to program.
• The hybrid architecture combines virtual memory and capabilities while separating virtualization from protection. It began with a formally specified MIPS64 design, then added capability registers and instructions to support fine-grained protection within an address space and efficient transitions between isolated domains.
• Capabilities replace ordinary data pointers with protected references containing bounds and protection attributes. When compiling C, pointers can be converted into capability-based references, although the proposed migration path does not require every program or developer to adopt that conversion immediately.
• Tagged capabilities are non-forgeable protected tokens for memory or objects. Their attributes describe permitted access, while object-capability attributes can be user-defined. Tagged memory allows the hardware to distinguish valid capabilities, although storing tags requires different engineering choices for FPGA and ASIC implementations.
• Formal analysis is integrated into the hardware development chain through SRI tools, including a model checker, an SMT solver, and formal verification proof tools. These tools analyze the formal hardware specification as it is converted through Verilog into an FPGA implementation.

Questions & Answers

Q: How can capability systems make computers more secure?

Capability systems make computers more secure by replacing ordinary pointers with protected references that contain bounds and access attributes. Hardware checks these references and prevents them from being forged. This supports spatial memory protection, reduces the threat from buffer overflows, and lets software place components into fine-grained compartments with limited authority and efficient transitions between domains.

Q: What is a capability in computer system security?

A capability is a protected token that refers to an object or an area of virtual memory and includes relevant protection attributes. Capability tags are designed to be non-forgeable, so software cannot simply manufacture unauthorized references. For object capabilities, the attributes relate to the referenced object and can be user-defined in the manner described by the earlier provably secure system work.

Q: How does compartmentalization limit software vulnerabilities?

Compartmentalization separates vulnerable code from the rest of an application and grants it only the privileges it needs. Decompression code, for example, can run outside the main loop in another domain. If that code contains a flaw, the compartment boundary limits what it can access or modify, reducing its ability to damage unrelated application components.

Q: How could a mail system isolate malicious attachments?

A mail system could place attachments inside a sandbox that has no privileges capable of causing broader harm. It could also isolate each message in its own compartment so messages cannot interfere with one another. The appropriate structure depends on what needs protection, but the central idea is to restrict risky content before it interacts with privileged application functions.

Q: Why combine virtual memory with capability protection?

Virtual memory and capabilities serve related but distinct purposes in the proposed architecture. The design separates virtualization from protection while retaining both mechanisms. Virtual memory remains isolated in a form intended to support proofs about the hardware specification, while capabilities provide fine-grained, per-pointer protection, bounds checking, and efficient context switching or domain crossing within an address space.

Q: How does the architecture prevent buffer overflows?

The architecture implements bounds checking and spatial protection for capability-based memory references. Because each protected reference carries information defining the memory it may access, hardware can prevent references from moving outside their authorized bounds. The seminar argues that this makes the buffer-overflow problem disappear in the same broad sense that protected memory mechanisms avoided it in Multics.

Q: Can existing C software migrate to capability hardware?

C software can migrate by converting ordinary pointers into capability-based references during compilation. The programming-language work described in the seminar examines the implications of that conversion. Adoption is not presented as mandatory for every program at once, so the architecture provides a migration path that permits software to use capability calls while allowing other code to remain unchanged initially.

Q: How are formal methods used in the capability project?

Formal methods are placed directly in the hardware build chain. SRI tools, including a model checker, an SMT solver, and formal verification proof tools, operate on the hardware specification as it is converted through Verilog into the FPGA. This process is intended to support verification of hardware properties instead of treating formal analysis as a separate, after-the-fact activity.

Summary & Key Takeaways

• Modern computer systems suffer from weaknesses across components, systems, and networks, leaving many potential weak links. The proposed response is fine-grained compartmentalization, which separates vulnerable code, protocols, messages, or attachments into restricted domains. Each compartment receives limited privileges, reducing its ability to interfere with unrelated data or system components.

• The hybrid architecture combines conventional virtual memory with capability-based protection inside an address space. Built by extending a formally specified MIPS64 design, it adds capability registers and instructions for bounds checking, spatial protection, protected references, and efficient domain crossing. An FPGA implementation demonstrates ideas that were impractical on earlier hardware platforms.

• The project connects hardware, operating systems, and programming languages through a practical migration path. C pointers can be converted into capability references, while existing code need not adopt that conversion immediately. Formal tools are incorporated into the hardware build chain, supporting analysis from the specification through its conversion into an FPGA implementation using Verilog.