CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
This addresses security for compilers in systems like CHERI, enabling safe integration of legacy code with untrusted components, though it is incremental as it builds on existing PAC principles.
The paper tackles the problem of securing partial programs compiled using the pointers-as-capabilities principle by proving full abstraction for a model compiler, showing it can provide security guarantees even when linked to attacker code, and implements it for C on CHERI with performance overhead proportional to cross-compilation-unit calls.
Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to CHERI compiler, for example, achieves memory safety by following a principle called "pointers as capabilities" (PAC). Informally, PAC says that a compiler should represent a source language pointer as a machine code capability. But the security properties of PAC compilers are not yet well understood. We show that memory safety is only one aspect, and that PAC compilers can provide significant additional security guarantees for partial programs: the compiler can provide security guarantees for a compilation unit, even if that compilation unit is later linked to attacker-provided machine code. As such, this paper is the first to study the security of PAC compilers for partial programs formally. We prove for a model of such a compiler that it is fully abstract. The proof uses a novel proof technique (dubbed TrICL, read trickle), which should be of broad interest because it reuses the whole-program compiler correctness relation for full abstraction, thus saving work. We also implement our scheme for C on CHERI, show that we can compile legacy C code with minimal changes, and show that the performance overhead of compiled code is roughly proportional to the number of cross-compilation-unit function calls.