Secure compilation preserves security properties of programs when they are transformed from an abstract specification (e.g. source language) to a refined model (e.g. assembly). For confidentiality, compilation must prevent unintended leakage of secret data thus preserving the information flow of the abstract model. This is challenging for several reasons. Current accounts of refinement (e.g., trace inclusion) do not support confidentiality properties well. Refinement may be used to eliminate underspecification and nondeterminism, it can change data representation, and it may expose new state information of the execution environment (such as caches, multiples cores, pipelines, buses, speculative execution, and so on). These features may introduce side channels, since they can provide an observer with information it did not have access to at an abstract model level, and in this way cause confidentiality properties to be violated. In practice, for some systems an implementation step may even have to consider storage channels: the introduction of completely new behaviours caused by hardware bugs, architectural flaws, or violation of assumptions such as memory coherence that are implicit at more abstract levels.1 We introduce techniques to show that also in such cases, with proper countermeasures in place that suitably isolate effects of the newly introduced features, it can be possible to identify a notion of refinement that preserves confidentiality in a meaningful sense. The key idea is to use the abstract model as a specification of the permitted information flow, and then to ensure that this flow induces an upper bound on the corresponding flow in the refined model. We formalize this notion in term knowledge: if the progression of observer knowledge on all refined computations is the same or weaker than the one on corresponding abstract ones then the refined model does not leak more information than the abstract model, hence we say it is a Confidentiality-Preserving Refinement (CPR). This allows us to transfer arbitrary information flow properties of the abstract model to the refined model, even if the abstract model allows communications.
Sun 13 JanDisplayed time zone: Belfast change
16:00 - 18:00
|Short Talks Session|
|Modular Security Guarantees for Low-Level Languages with Stack Traversal|
|(Un)Encrypted Computing and Indistinguishability Obfuscation|