CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle

El-Korashy, Akram and Tsampas, Stelios and Patrignani, Marco and Devriese, Dominique and Garg, Deepak and Piessens, Frank
(2021) CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle.
In: 34th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

main-csf21.pdf - Accepted Version

Download (475kB) | Preview


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.


Actions (login required)

View Item View Item