Visible to the public Information-Flow Preservation in Compiler Optimisations

TitleInformation-Flow Preservation in Compiler Optimisations
Publication TypeConference Paper
Year of Publication2019
AuthorsBesson, Frédéric, Dang, Alexandre, Jensen, Thomas
Conference Name2019 IEEE 32nd Computer Security Foundations Symposium (CSF)
KeywordsCompCert C compiler, compiler, compiler optimisations, compiler security, compositionality, correct compilers, I-O Systems, i-o systems security, IFP, information flow, information-flow leaks, information-flow preservation, information-flow preserving program transformation, Metrics, Micromechanical devices, optimising compilers, Optimization, passive side-channel attacks, program optimisations, Program processors, program transformations, program verification, pubcrawl, Resiliency, Scalability, security, Semantics, side-channel, side-channel attacks, source program, standard compiler passes, Standards, target program

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.

Citation Keybesson_information-flow_2019