Visible to the public Biblio

Filters: Author is Besson, Frédéric  [Clear All Filters]
2019-12-02
Besson, Frédéric, Dang, Alexandre, Jensen, Thomas.  2019.  Information-Flow Preservation in Compiler Optimisations. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :230–23012.

Correct compilers perform program transformations preserving input/output behaviours of programs. Yet, correctness does not prevent program optimisations from introducing information-flow leaks that would make the target program more vulnerable to side-channel attacks than the source program. To tackle this problem, we propose a notion of Information-Flow Preserving (IFP) program transformation which ensures that a target program is no more vulnerable to passive side-channel attacks than a source program. To protect against a wide range of attacks, we model an attacker who is granted arbitrary memory accesses for a pre-defined set of observation points. We propose a compositional proof principle for proving that a transformation is IFP. Using this principle, we show how a translation validation technique can be used to automatically verify and even close information-flow leaks introduced by standard compiler passes such as dead-store elimination and register allocation. The technique has been experimentally validated on the CompCert C compiler.