Symbolic Models for Isolated Execution Environments

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.
Type de document :
Communication dans un congrès
Cătălin Hriţcu. 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), Apr 2017, Paris, France. Springer, Proceedings of the 2nd IEEE European Symposium on Security and Privacy
Liste complète des métadonnées


https://hal.inria.fr/hal-01396291
Contributeur : Steve Kremer <>
Soumis le : jeudi 2 février 2017 - 16:56:38
Dernière modification le : vendredi 16 juin 2017 - 01:09:13
Document(s) archivé(s) le : vendredi 5 mai 2017 - 11:12:20

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01396291, version 1

Citation

Charlie Jacomme, Steve Kremer, Guillaume Scerri. Symbolic Models for Isolated Execution Environments. Cătălin Hriţcu. 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), Apr 2017, Paris, France. Springer, Proceedings of the 2nd IEEE European Symposium on Security and Privacy. <hal-01396291>

Partager

Métriques

Consultations de
la notice

424

Téléchargements du document

47