Skip to Main content Skip to Navigation
Conference papers

Securing Compilation Against Memory Probing

Frédéric Besson 1 Alexandre Dang 1 Thomas Jensen 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : A common security recommendation is to reduce the in-memory lifetime of secret values, in order to reduce the risk that an attacker can obtain secret data by probing memory. To mitigate this risk, secret values can be overwritten, at source level, after their last use. The problem we address here is how to ensure that a compiler preserve these mitigation efforts and thus that secret values are not easier to obtain at assembly level than at source level. We propose a formal definition of Information Flow Preserving program Transformations in which we model the information leak of a program using the notion of Attacker Knowledge. Program transformations are validated by relating the knowledge of the attacker before and after the transformation. We consider two classic compiler passes (Dead Store Elimination and Register Allocation) and show how to validate and, if needed, modify these transformations in order to be information flow preserving.
Document type :
Conference papers
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Alexandre Dang <>
Submitted on : Tuesday, October 23, 2018 - 11:17:08 AM
Last modification on : Saturday, July 11, 2020 - 3:15:43 AM
Long-term archiving on: : Thursday, January 24, 2019 - 1:28:25 PM


Files produced by the author(s)



Frédéric Besson, Alexandre Dang, Thomas Jensen. Securing Compilation Against Memory Probing. PLAS '18 - 13th Workshop on Programming Languages and Analysis for Security, Oct 2018, Toronto, Canada. pp.29-40, ⟨10.1145/3264820.3264822⟩. ⟨hal-01901765⟩



Record views


Files downloads