Skip to Main content Skip to Navigation
Conference papers

Symbolic Models for Isolated Execution Environments

Charlie Jacomme 1 Steve Kremer 2 Guillaume Scerri 3, 4
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 PETRUS - Personal Trusted cloud
DAVID - Données et algorithmes pour une ville intelligente et durable - DAVID, Inria Saclay - Ile de France
Abstract : Isolated Execution Environments (IEEs), such as ARM TrustZone and Intel SGX, offer the possibility to execute sensitive code in isolation from other malicious programs, running on the same machine, or a potentially corrupted OS. A key feature of IEEs is the ability to produce reports binding cryptographically a message to the program that produced it, typically ensuring that this message is the result of the given program running on an IEE. We present a symbolic model for specifying and verifying applications that make use of such features. For this we introduce the S$\ell$APIC process calculus, that allows to reason about reports issued at given locations. We also provide tool support, extending the SAPIC/TAMARIN toolchain and demonstrate the applicability of our framework on several examples implementing secure outsourced computation (SOC), a secure licensing protocol and a one-time password protocol that all rely on such IEEs.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Steve Kremer Connect in order to contact the contributor
Submitted on : Thursday, February 2, 2017 - 4:56:38 PM
Last modification on : Thursday, January 20, 2022 - 5:31:56 PM
Long-term archiving on: : Friday, May 5, 2017 - 11:12:20 AM


Files produced by the author(s)



Charlie Jacomme, Steve Kremer, Guillaume Scerri. Symbolic Models for Isolated Execution Environments. 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), Apr 2017, Paris, France. ⟨10.1109/EuroSP.2017.16⟩. ⟨hal-01396291⟩



Les métriques sont temporairement indisponibles