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
-
[CANCELLED] Black-Box Collision Attacks on Widely Deployed Perceptual Hash Functions and Their Consequences
Speaker : Diane Leblanc-Albarel - KU Leuven
[CANCELLED] Perceptual hash functions identify multimedia content by mapping similar inputs to similar outputs. They are widely used for detecting copyright violations and illegal content but lack transparency, as their design details are typically kept secret. Governments are considering extending the application of these functions to Client-Side Scanning (CSS) for end-to-end encrypted services:[…]-
Cryptography
-
SoSysec
-
Protocols
-
-
A non-comparison oblivious sort and its application to private k-NN
Speaker : Sofiane Azogagh - UQÀM
Sorting is a fundamental subroutine of many algorithms and as such has been studied for decades. A well-known result is the Lower Bound Theorem, which states that no comparison-based sorting algorithm can do better than O(nlog(n)) in the worst case. However, in the fifties, new sorting algorithms that do not rely on comparisons were introduced such as counting sort, which can run in linear time[…]-
Cryptography
-
SoSysec
-
Privacy
-
Databases
-
Secure storage
-