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...
Published in: | 2021 IEEE 34th Computer Security Foundations Symposium (CSF) |
---|---|
Main Authors: | , , , , , |
Other Authors: | |
Format: | Conference Object |
Language: | English |
Published: |
IEEE
2021
|
Subjects: | |
Online Access: | https://hdl.handle.net/11572/336481 https://doi.org/10.1109/CSF51468.2021.00036 |
id |
ftutrentoiris:oai:iris.unitn.it:11572/336481 |
---|---|
record_format |
openpolar |
spelling |
ftutrentoiris:oai:iris.unitn.it:11572/336481 2024-02-11T10:09:08+01:00 CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle El-Korashy, Akram Tsampas, Stelios Patrignani, Marco Devriese, Dominique Garg, Deepak Piessens, Frank El-Korashy, Akram Tsampas, Stelio Patrignani, Marco Devriese, Dominique Garg, Deepak Piessens, Frank 2021 https://hdl.handle.net/11572/336481 https://doi.org/10.1109/CSF51468.2021.00036 eng eng IEEE place:Piscataway, NJ USA info:eu-repo/semantics/altIdentifier/isbn/978-1-7281-7607-9 info:eu-repo/semantics/altIdentifier/wos/WOS:000719322000018 ispartofbook:34th IEEE Computer Security Foundations Symposium, {CSF} 2021, Dubrovnik,Croatia, June 21-25, 2021 CSF firstpage:1 lastpage:16 numberofpages:16 serie:PROCEEDINGS IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM https://hdl.handle.net/11572/336481 doi:10.1109/CSF51468.2021.00036 info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85117798888 https://doi.org/10.1109/CSF51468.2021.00036 info:eu-repo/semantics/closedAccess Capability machines full abstraction secure compilation info:eu-repo/semantics/conferenceObject 2021 ftutrentoiris https://doi.org/10.1109/CSF51468.2021.00036 2024-01-23T23:12:29Z 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. Conference Object The Pointers Università degli Studi di Trento: CINECA IRIS 2021 IEEE 34th Computer Security Foundations Symposium (CSF) 1 16 |
institution |
Open Polar |
collection |
Università degli Studi di Trento: CINECA IRIS |
op_collection_id |
ftutrentoiris |
language |
English |
topic |
Capability machines full abstraction secure compilation |
spellingShingle |
Capability machines full abstraction secure compilation El-Korashy, Akram Tsampas, Stelios Patrignani, Marco Devriese, Dominique Garg, Deepak Piessens, Frank CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle |
topic_facet |
Capability machines full abstraction secure compilation |
description |
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. |
author2 |
El-Korashy, Akram Tsampas, Stelio Patrignani, Marco Devriese, Dominique Garg, Deepak Piessens, Frank |
format |
Conference Object |
author |
El-Korashy, Akram Tsampas, Stelios Patrignani, Marco Devriese, Dominique Garg, Deepak Piessens, Frank |
author_facet |
El-Korashy, Akram Tsampas, Stelios Patrignani, Marco Devriese, Dominique Garg, Deepak Piessens, Frank |
author_sort |
El-Korashy, Akram |
title |
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle |
title_short |
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle |
title_full |
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle |
title_fullStr |
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle |
title_full_unstemmed |
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle |
title_sort |
capableptrs: securely compiling partial programs using the pointers-as-capabilities principle |
publisher |
IEEE |
publishDate |
2021 |
url |
https://hdl.handle.net/11572/336481 https://doi.org/10.1109/CSF51468.2021.00036 |
genre |
The Pointers |
genre_facet |
The Pointers |
op_relation |
info:eu-repo/semantics/altIdentifier/isbn/978-1-7281-7607-9 info:eu-repo/semantics/altIdentifier/wos/WOS:000719322000018 ispartofbook:34th IEEE Computer Security Foundations Symposium, {CSF} 2021, Dubrovnik,Croatia, June 21-25, 2021 CSF firstpage:1 lastpage:16 numberofpages:16 serie:PROCEEDINGS IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM https://hdl.handle.net/11572/336481 doi:10.1109/CSF51468.2021.00036 info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85117798888 https://doi.org/10.1109/CSF51468.2021.00036 |
op_rights |
info:eu-repo/semantics/closedAccess |
op_doi |
https://doi.org/10.1109/CSF51468.2021.00036 |
container_title |
2021 IEEE 34th Computer Security Foundations Symposium (CSF) |
container_start_page |
1 |
op_container_end_page |
16 |
_version_ |
1790608874153181184 |