(2021) CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle.
|
Text
main-csf21.pdf - Accepted Version Download (475kB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Marco Patrignani (MP) |
| Conference: | CSF IEEE Computer Security Foundations Symposium (was CSFW) |
| Depositing User: | Marco Patrignani |
| Date Deposited: | 22 Jul 2021 11:34 |
| Last Modified: | 22 Jul 2021 11:34 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3453 |
Actions
Actions (login required)
 |
View Item |