Cryptology ePrint Archive: Report 2017/070

Symbolic Models for Isolated Execution Environments

Charlie Jacomme and 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.

Category / Keywords: cryptographic protocols / isolated execution environments, trusted hardware, symbolic models, automated verification

Original Publication (with major differences): 2nd IEEE European Symposium on Security and Privacy

Date: received 31 Jan 2017

Contact author: steve kremer at inria fr

Available format(s): PDF | BibTeX Citation

Version: 20170131:214802 (All versions of this report)

Short URL: ia.cr/2017/070

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]