@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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)},
pages = {530--545},
doi = {10.1109/EuroSP.2017.16},
month = apr,
publisher = {IEEE Computer Society},
title = {Symbolic Models for Isolated Execution Environments},
year = 2017,
acronym = {{EuroSP}'17},
nmonth = 4,
url = {https://hal.inria.fr/hal-01533708/document},
}