Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
| Autor: | Sander Huyghebaert, Alix Trieu, Dominique Devriese, Lars Birkedal, Amin Timany, Armaël Guéneau, Thomas Van Strydonck, Aïna Linn Georges |
|---|---|
| Přispěvatelé: | Software Languages Lab, Informatics and Applied Informatics, Faculty of Sciences and Bioengineering Sciences |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Stack-based memory allocation
Technology Computer science Calling convention 02 engineering and technology computer.software_genre CHERI universal contracts local capabilities Privilege separation 0202 electrical engineering electronic engineering information engineering Code (cryptography) Feature (machine learning) Safety Risk Reliability and Quality Block (data storage) Science & Technology Revocation 020207 software engineering Computer Science Software Engineering uninitialized capabilities STATE 020202 computer hardware & architecture program logic capability revocation Computer Science Operating system capability safety capability machines computer Software Program logic |
| Zdroj: | Georges, A L, Guéneau, A, Van Strydonck, T, Timany, A, Trieu, A, Huyghebaert, S, Devriese, D & Birkedal, L 2021, ' Efficient and provable local capability revocation using uninitialized capabilities ', Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, 6 . https://doi.org/10.1145/3434287 |
| Popis: | Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of authority-carrying values known as capabilities. The CHERI capability machine offers local capabilities, which could be used as a cheap but restricted form of capability revocation. Unfortunately, local capability revocation is unrealistic in practice because large amounts of stack memory need to be cleared as a security precaution. In this paper, we address this shortcoming by introducing uninitialized capabilities : a new form of capabilities that represent read/write authority to a block of memory without exposing the memory’s initial contents. We provide a mechanically verified program logic for reasoning about programs on a capability machine with the new feature and we formalize and prove capability safety in the form of a universal contract for untrusted code. We use uninitialized capabilities for making a previously-proposed secure calling convention efficient and prove its security using the program logic. Finally, we report on a proof-of-concept implementation of uninitialized capabilities on the CHERI capability machine. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|