Symbolic Models for Isolated Execution Environments

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 metadatas

Cited literature [20 references]  Display  Hide  Download
Contributor : Steve Kremer <>
Submitted on : Thursday, February 2, 2017 - 4:56:38 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Friday, May 5, 2017 - 11:12:20 AM


Files produced by the author(s)


  • HAL Id : hal-01396291, version 1


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. ⟨hal-01396291⟩



Record views


Files downloads