SPOOC: Symbolic Models for Isolated Execution Environments

Symbolic Models for Isolated Execution Environments

Charlie Jacomme, Steve Kremer, and Guillaume Scerri. Symbolic Models for Isolated Execution Environments. In Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pp. 530–545, IEEE Computer Society, Paris, France, April 2017.

Download

[PDF] [PDF (long version)]

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.

BibTeX

@inproceedings{JKS-eurosp17,
  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.},
  address =	 {Paris, France},
  author =	 {Jacomme, Charlie and Kremer, Steve and Scerri,
                  Guillaume},
  booktitle =	 {{P}roceedings of the 2nd IEEE European Symposium on
                  Security and Privacy (EuroS\&P'17)},
  month =	 apr,
  publisher =	 {IEEE Computer Society},
  title =	 {Symbolic Models for Isolated Execution Environments},
  pages =	 {530--545},
  year =	 2017,
  acronym =	 {{EuroSP}'17},
  nmonth =	 4,
}