CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle ...
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). In...
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference Object |
| Language: | unknown |
| Published: |
CISPA
2023
|
| Subjects: | |
| Online Access: | https://dx.doi.org/10.60882/cispa.24613692 https://publications.cispa.de/articles/conference_contribution/CapablePtrs_Securely_Compiling_Partial_Programs_Using_the_Pointers-as-Capabilities_Principle/24613692 |
| Summary: | 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 ... |
|---|