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
Inria Saclay - Ile de France, DAVID - Données et algorithmes pour une ville intelligente et durable - DAVID
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

https://hal.inria.fr/hal-01396291
Contributor : Steve Kremer <>
Submitted on : Thursday, February 2, 2017 - 4:56:38 PM
Last modification on : Friday, March 6, 2020 - 11:42:02 AM
Document(s) archivé(s) le : Friday, May 5, 2017 - 11:12:20 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01396291, version 1

Citation

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⟩

Share

Metrics

Record views

1002

Files downloads

474