Skip to Main content Skip to Navigation

Secure Compilation for Memory Protection

Alexandre Dang 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Our society has been growingly dependent on computer systems and this tendency will not slow down in the incoming years. Similarly, interests over cybersecurity have been increasing alongside the possible consequences brought by successful attacks on these systems. This thesis tackles the issue of security of systems and especially focuses on compilation to achieve its goal. Compilation is the process of translating source programs written by humans to machine code readable by our systems. We explore the two possible behaviours of a secure compiler which are enforcement and preservation. First, we have developed CompCertSFI, a compiler which enforces the isolation of modules into closed memory areas called sandboxes. These modules are then unable to access memory regions outside of their sandbox which prevents any malicious module from corrupting other entities of the system. On the topic of security preservation, we defined a notion of Information Flow Preserving transformation to make sure that a program does get less secure during compilation. Our property is designed to preserve security against side-channel attacks. This new category of attacks uses physical mediums such as time or power consumption which are taken into account by current compilers.
Document type :
Complete list of metadatas

Cited literature [119 references]  Display  Hide  Download
Contributor : Alexandre Dang <>
Submitted on : Friday, October 23, 2020 - 3:13:57 PM
Last modification on : Sunday, October 25, 2020 - 3:09:44 AM


Files produced by the author(s)


  • HAL Id : tel-02976694, version 1


Alexandre Dang. Secure Compilation for Memory Protection. Computer Science [cs]. Inria Rennes; Université Rennes 1, 2019. English. ⟨tel-02976694⟩



Record views


Files downloads