Formally Secure Compilation Despite Dynamic Compromise
| Autor: | Abate, Carmine, Azevedo de Amorim, Arthur, Blanco, Roberto, Evans, Ana Nora, Fachini, Guglielmo, Hritcu, Catalin, Laurent, Théo, Pierce, Benjamin C., Stronati, Marco, Tolmach, Andrew |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), University of Trento [Trento], Carnegie Mellon University [Pittsburgh] (CMU), University of Virginia, École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL), University of Pennsylvania, Portland State University [Portland] (PSU), ERC SECOMP, DARPA SSITH/HOPE, European Project: 715753,H2020,SECOMP(2017), Programming securely with cryptography (PROSECCO ), University of Virginia [Charlottesville], École normale supérieure - Paris (ENS Paris), University of Pennsylvania [Philadelphia] |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | 25th ACM Conference on Computer and Communications Security (CCS) 25th ACM Conference on Computer and Communications Security (CCS), Oct 2018, Toronto, Canada. pp.1351--1368, ⟨10.1145/3243734.3243745⟩ Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security |
| DOI: | 10.1145/3243734.3243745⟩ |
| Popis: | International audience; We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds.Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly specified privileges. It articulates how each component should be protected from all the others---in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees---in particular, its internal invariants are protected from compromised components---up to the point when this component itself becomes compromised, after which we assume an attacker can take complete control and use this component's privileges to attack other components. More precisely, a secure compilation chain must ensure that a dynamically compromised component cannot break the safety properties of the system at the target level any more than an arbitrary attacker-controlled component (with the same interface and privileges, but without undefined behaviors) already could at the source level.To illustrate the model, we construct a secure compilation chain for a small unsafe language with buffers, procedures, and components, targeting a simple abstract machine with built-in compartmentalization. We give a careful proof (mostly machine-checked in Coq) that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|