Skip to Main content Skip to Navigation
Conference papers

Modular Software Fault Isolation as Abstract Interpretation

Frédéric Besson 1 Thomas Jensen 1 Julien Lepiller 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Software Fault Isolation (SFI) consists in transforming un-trusted code so that it runs within a specific address space, (called the sandbox) and verifying at load-time that the binary code does indeed stay inside the sandbox. Security is guaranteed solely by the SFI verifier whose correctness therefore becomes crucial. Existing verifiers enforce a very rigid, almost syntactic policy where every memory access and every control-flow transfer must be preceded by a sandboxing instruction sequence, and where calls outside the sandbox must implement a sophisticated protocol based on a shadow stack. We propose to define SFI as a defensive semantics, with the purpose of deriving semantically sound verifiers that admit flexible and efficient implementations of SFI. We derive an executable analyser, that works on a per-function basis, which ensures that the defensive semantics does not go wrong, and hence that the code is well isolated. Experiments show that our analyser exhibits the desired flexibility: it validates correctly sandboxed code, it catches code breaking the SFI policy, and it can validate programs where redundant instrumentations are optimised away.
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download
Contributor : Thomas Jensen <>
Submitted on : Friday, October 12, 2018 - 10:15:26 AM
Last modification on : Saturday, July 11, 2020 - 3:15:17 AM
Long-term archiving on: : Sunday, January 13, 2019 - 1:31:32 PM


Files produced by the author(s)



Frédéric Besson, Thomas Jensen, Julien Lepiller. Modular Software Fault Isolation as Abstract Interpretation. SAS 2018 - 25th International Static Analysis Symposium, Aug 2018, Freiburg, Germany. pp.166-186, ⟨10.1007/978-3-319-99725-4_12⟩. ⟨hal-01894116⟩



Record views


Files downloads