Paper 2017/070

Symbolic Models for Isolated Execution Environments

Charlie Jacomme, Steve Kremer, and Guillaume Scerri

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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Major revision. 2nd IEEE European Symposium on Security and Privacy
Keywords
isolated execution environmentstrusted hardwaresymbolic modelsautomated verification
Contact author(s)
steve kremer @ inria fr
History
2017-01-31: received
Short URL
https://ia.cr/2017/070
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/070,
      author = {Charlie Jacomme and Steve Kremer and Guillaume Scerri},
      title = {Symbolic Models for Isolated Execution Environments},
      howpublished = {Cryptology {ePrint} Archive, Paper 2017/070},
      year = {2017},
      url = {https://eprint.iacr.org/2017/070}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.