Description
We propose a new formal criterion for secure compilation, providing strong end-to-end security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others until it becomes compromised by exhibiting undefined behavior, opening the door for an attacker to take control over the component and to use the component's privileges to attack the remaining uncompromised components. More precisely, we ensure that dynamically compromised components cannot break the safety properties of the system at the target level any more than equally privileged components without undefined behavior already could in the source language. To illustrate this model, we build a secure compilation chain for an unsafe language with buffers, procedures, and components. We compile this to a simple RISC abstract machine with built-in compartmentalization and provide machine-checked proofs in Coq showing 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 tag-based reference monitoring."
Practical infos
Next sessions
-
Les jeux vidéo de l’écran au réel : enjeux juridiques et (géo)politiques au prisme de la cybersécurité
Speaker : Léandre Lebon, Sandrine Turgis - Univ Rennes, IODE
Protection des droits d’auteur, lutte contre les techniques de triche, interactions avec la guerre et les conflits hybrides, enjeux de démocratie ... Sous l’angle de la cybersécurité les enjeux juridiques et (géo)politiques des jeux video sont nombreux. Cette présentation du groupe de travail sur les jeux video (GTJV) permettra d’alimenter la réflexion sur l’articulation entre jeux video et[…]-
Law
-
-
The Quest for my Perfect MATE. Investigate MATE: Man-at-the-End attacker (followed by a hands-on application).
Speaker : Mohamed Sabt, Etienne Nedjaï - Univ Rennes, IRISA
Shannon sought security against an attacker with unlimited computational powers: if an information source conveys some information, then Shannon’s attacker will surely extract that information. Diffie and Hellman refined Shannon’s attacker model by taking into account the fact that the real attackers are computationally limited. This idea became one of the greatest new paradigms in computer[…]