Matteo Busi
Skip Abstract Section
Abstract
Computer systems often provide hardware support for isolation mechanisms such as privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken, the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features brings a risk of introducing new software-based side-channel attacks.
This article studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. Our solution is heavily based on techniques from research on programming languages. More specifically, we propose to use the programming language concept of full abstraction as a general formal criterion for the security of a processor extension. We instantiate the proposed criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility. This is a very relevant instantiation, as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor and evaluate the cost of our design in terms of performance and hardware size.
- Martín Abadi. 1999. Protection in programming-language translations. In Secure Internet Programming, Security Issues for Mobile and Distributed Objects(Lecture Notes in Computer Science, Vol. 1603), Jan Vitek and Christian Damsgaard Jensen (Eds.). Springer, 19–34.Google Scholar
- Carmine Abate, Roberto Blanco, Ştefan Ciobâcă, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault. 2020. Trace-relating compiler correctness and secure compilation. In Proceedings of the 29th European Symposium on Programming: Programming Languages and Systems, Held as Part of the European Joint Conferences on Theory and Practice of Software. Springer, 1–28. DOI: https://doi.org/10.1007/978-3-030-44914-8_1Google Scholar
- Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. 2019. Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium. IEEE, 256–271.Google ScholarCross Ref
- Pieter Agten, Raoul Strackx, Bart Jacobs, and Frank Piessens. 2012. Secure compilation to modern processors. In Proceedings of the 25th IEEE Computer Security Foundations Symposium. IEEE Computer Society, 171–185.Google ScholarDigital Library
- Amal Ahmed and Matthias Blume. 2008. Typed closure conversion preserves observational equivalence. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional programming. Association for Computing Machinery, 157–168.Google ScholarDigital Library
- Amal Ahmed and Matthias Blume. 2011. An equivalence-preserving CPS translation via multi-language semantics. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. Association for Computing Machinery, 431–444.Google ScholarDigital Library
- Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2020. Formal verification of a constant-time preserving C compiler. Proc. ACM Prog. Lang. 4, POPL (2020), 7:1–7:30. DOI: https://doi.org/10.1145/3371075Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2018. Secure compilation of side-channel countermeasures: The case of cryptographic “constant-time.” In Proceedings of the 31st IEEE Computer Security Foundations Symposium. IEEE, 328–343.Google ScholarCross Ref
- Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. 2018. Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution. In Proceedings of the 27th USENIX Security Symposium.USENIX Association, 991–1008. Retrieved from https://www.usenix.org/conference/usenixsecurity18/presentation/bulck.Google Scholar
- Jo Van Bulck, David Oswald, Eduard Marin, Abdulla Aldoseri, Flavio D. Garcia, and Frank Piessens. 2019. A tale of two worlds: Assessing the vulnerability of enclave shielding runtimes. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 1741–1758. DOI: https://doi.org/10.1145/3319535.3363206Google Scholar
- Jo Van Bulck, Frank Piessens, and Raoul Strackx. 2017. SGX-Step: A practical attack framework for precise enclave execution control. In Proceedings of the 2nd Workshop on System Software for Trusted Execution. ACM, 4:1–4:6. DOI: https://doi.org/10.1145/3152701.3152706Google ScholarDigital Library
- Jo Van Bulck, Nico Weichbrodt, Rüdiger Kapitza, Frank Piessens, and Raoul Strackx. 2017. Telling your secrets without page faults: Stealthy page table-based attacks on enclaved execution. In Proceedings of the 26th USENIX Security Symposium.USENIX Association, 1041–1056. Retrieved from https://www.usenix.org/conference/usenixsecurity17/technical-sessions/pre sentation/van-bulck.Google Scholar
- Matteo Busi, Job Noorman, Jo Van Bulck, Letterio Galletta, Pierpaolo Degano, Jan Tobias Mühlberg, and Frank Piessens. 2020. Provably secure isolation for interruptible enclaved execution on small microprocessors. In Proceedings of the 33rd IEEE Computer Security Foundations Symposium. IEEE, 262–276.Google Scholar
- Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019. A systematic evaluation of transient execution attacks and defenses. In Proceedings of the 28th USENIX Security Symposium. USENIX Association, 249–266. Retrieved from https://www.usenix.org/conference/usenixsecurity19/presentation/canella.Google Scholar
- Guoxing Chen, Sanchuan Chen, Yuan Xiao, Yinqian Zhang, Zhiqiang Lin, and Ten H. Lai. 2019. SgxPectre attacks: Stealing Intel secrets from SGX enclaves via speculative execution. In Proceedings of the IEEE European Symposium on Security and Privacy. IEEE, 142–157.Google Scholar
- Carlos Tomé Cortiñas, Marco Vassena, and Alejandro Russo. 2020. Securing asynchronous exceptions. In Proceedings of the 33rd IEEE Computer Security Foundations Symposium. IEEE, 214–229. DOI: https://doi.org/10.1109/CSF49147.2020.00023Google Scholar
- Victor Costan and Srinivas Devadas. 2016. Intel SGX explained. IACR Cryptology ePrint Archive 2016 (2016), 86. Retrieved from http://eprint.iacr.org/2016/086.Google Scholar
- Ruan de Clercq, Frank Piessens, Dries Schellekens, and Ingrid Verbauwhede. 2014. Secure interrupts on low-end microcontrollers. In Proceedings of the IEEE 25th International Conference on Application-specific Systems, Architectures and Processors. IEEE Computer Society, 147–152. DOI: https://doi.org/10.1109/ASAP.2014.6868649Google ScholarCross Ref
- Dominique Devriese and Frank Piessens. 2010. Noninterference through secure multi-execution. In Proceedings of the 31st IEEE Symposium on Security and Privacy. IEEE Computer Society, 109–124. DOI: https://doi.org/10.1109/SP.2010.15Google ScholarDigital Library
- Craig Disselkoen, Radha Jagadeesan, Alan Jeffrey, and James Riely. 2019. The code that never ran: Modeling attacks on speculative evaluation. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 1238–1255. DOI: https://doi.org/10.1109/SP.2019.00047Google ScholarCross Ref
- Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th Symposium on Operating Systems Principles. ACM, 287–305. DOI: https://doi.org/10.1145/3132747.3132782Google ScholarDigital Library
- Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. 2013. Fully abstract compilation to JavaScript. In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 371–384.Google ScholarDigital Library
- Qian Ge, Yuval Yarom, David Cock, and Gernot Heiser. 2018. A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J. Cryptog. Eng. 8, 1 (2018), 1–27. DOI: https://doi.org/10.1007/s13389-016-0141-6Google ScholarCross Ref
- Travis Goodspeed. 2008. Practical attacks against the MSP430 BSL. In Proceedings of the 25th Chaos Communications Congress.Verlag Art d’Ameublement, Bielefeld.Google Scholar
- Johannes Götzfried, Tilo Müller, Ruan de Clercq, Pieter Maene, Felix Freiling, and Ingrid Verbauwhede. 2015. Soteria: Offline software protection within low-cost embedded devices. In Proceedings of the 31st Computer Security Applications Conference. ACM, 241–250. DOI: https://doi.org/10.1145/2818000.2856129Google ScholarDigital Library
- Daniel Gruss. 2017. Software-based Microarchitectural Attacks. Ph.D. Dissertation. Graz University of Technology.Google Scholar
- Roberto Guanciale, Musard Balliu, and Mads Dam. 2020. InSpectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. IEEE, 1853–1869. DOI: https://doi.org/10.1145/3372297.3417246Google ScholarDigital Library
- Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, and Andrés Sánchez. 2020. Spectector: Principled detection of speculative information flows. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 1–19. DOI: https://doi.org/10.1109/SP40000.2020.00011Google ScholarCross Ref
- Wenjian He, Wei Zhang, Sanjeev Das, and Yang Liu. 2018. SGXlinger: A new side-channel attack vector based on interrupt latency against enclave execution. In Proceedings of the 36th IEEE International Conference on Computer Design. IEEE Computer Society, 108–114. DOI: https://doi.org/10.1109/ICCD.2018.00025Google ScholarCross Ref
- Texas Instruments. 2016. MSP430x1xx Family: User Guide. Retrieved from http://www.ti.com/lit/ug/slau049f/slau049f.pdf.Google Scholar
- Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. 2016. Beyond good and evil: Formalizing the security guarantees of compartmentalizing compilation. In Proceedings of the IEEE 29th Computer Security Foundations Symposium. IEEE, 45–60. DOI: https://doi.org/10.1109/CSF.2016.11Google Scholar
- Vineeth Kashyap, Ben Wiedermann, and Ben Hardekopf. 2011. Timing- and termination-sensitive secure information flow: Exploring a new approach. In Proceedings of the 32nd IEEE Symposium on Security and Privacy. IEEE Computer Society, 413–428. DOI: https://doi.org/10.1109/SP.2011.19Google ScholarDigital Library
- Yoongu Kim, Ross Daly, Jeremie Kim, Chris Fallin, Ji-Hye Lee, Donghyuk Lee, Chris Wilkerson, Konrad Lai, and Onur Mutlu. 2014. Flipping bits in memory without accessing them: An experimental study of DRAM disturbance errors. In Proceedings of the ACM/IEEE 41st International Symposium on Computer Architecture. IEEE Computer Society, 361–372. DOI: https://doi.org/10.1109/ISCA.2014.6853210Google ScholarDigital Library
- Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting speculative execution. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 1–19. DOI: https://doi.org/10.1109/SP.2019.00002Google ScholarCross Ref
- Patrick Koeberl, Steffen Schulz, Ahmad-Reza Sadeghi, and Vijay Varadharajan. 2014. TrustLite: A security architecture for tiny embedded devices. In Proceedings of the 9th Eurosys Conference. ACM, 10:1–10:14. DOI: https://doi.org/10.1145/2592798.2592824Google ScholarDigital Library
- Sangho Lee, Ming-Wei Shih, Prasun Gera, Taesoo Kim, Hyesoon Kim, and Marcus Peinado. 2017. Inferring fine-grained control flow inside SGX enclaves with branch shadowing. In Proceedings of the 26th USENIX Security Symposium. USENIX Association, 557–574. Retrieved from https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/lee-sangho.Google Scholar
- Xavier Leroy. 2009. A formally verified compiler back-end. J. Autom. Reason. 43, 4 (2009), 363–446. DOI: https://doi.org/10.1007/s10817-009-9155-4Google ScholarDigital Library
- Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading kernel memory from user space. In Proceedings of the 27th USENIX Security Symposium. USENIX Association, 973–990. Retrieved from https://www.usenix.org/conference/usenixsecurity18/presentation/lipp.Google Scholar
- Nancy A. Lynch and Mark R. Tuttle. 1989. An introduction to input/output automata. CWI Quart. 2 (1989), 219–246.Google Scholar
- Jonathan M. McCune, Yanlin Li, Ning Qu, Zongwei Zhou, Anupam Datta, Virgil D. Gligor, and Adrian Perrig. 2010. TrustVisor: Efficient TCB reduction and attestation. In Proceedings of the 31st IEEE Symposium on Security and Privacy. IEEE Computer Society, 143–158. DOI: https://doi.org/10.1109/SP.2010.17Google ScholarDigital Library
- Frank McKeen, Ilya Alexandrovich, Alex Berenzon, Carlos V. Rozas, Hisham Shafi, Vedvyas Shanbhogue, and Uday R. Savagaonkar. 2013. Innovative instructions and software model for isolated execution. In Proceedings of the 2nd Workshop on Hardware and Architectural Support for Security and Privacy. ACM, 10. DOI: https://doi.org/10.1145/2487726.2488368Google Scholar
- Daniel Moghimi, Jo Van Bulck, Nadia Heninger, Frank Piessens, and Berk Sunar. 2020. CopyCat: Controlled instruction-level attacks on enclaves. In Proceedings of the 29th USENIX Security Symposium. USENIX Association, 469–486.Google Scholar
- Kit Murdock, David Oswald, Flavio D. Garcia, Jo Van Bulck, Daniel Gruss, and Frank Piessens. 2020. Plundervolt: Software-based fault injection attacks against Intel SGX. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P’20). IEEE, 1466–1482.Google ScholarCross Ref
- Job Noorman, Pieter Agten, Wilfried Daniels, Raoul Strackx, Anthony Van Herrewege, Christophe Huygens, Bart Preneel, Ingrid Verbauwhede, and Frank Piessens. 2013. Sancus: Low-cost trustworthy extensible networked devices with a zero-software trusted computing base. In Proceedings of the 22nd USENIX Security Symposium. 479–494. Retrieved from https://www.usenix.org/conference/usenixsecurity13/technical-sessions/presentation/noorman.Google Scholar
- Job Noorman, Jo Van Bulck, Jan Tobias Mühlberg, Frank Piessens, Pieter Maene, Bart Preneel, Ingrid Verbauwhede, Johannes Götzfried, Tilo Müller, and Felix Freiling. 2017. Sancus 2.0: A low-cost security architecture for IoT Devices. ACM Trans. Priv. Secur. 20, 3 (July 2017). DOI: https://doi.org/10.1145/3079763Google ScholarDigital Library
- Ivan Oliveira Nunes, Karim Eldefrawy, Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. 2019. VRASED: A verified hardware/software co-design for remote attestation. In Proceedings of the 28th USENIX Security Symposium. USENIX Association, 1429–1446.Google Scholar
- Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. 2015. Secure compilation to protected module architectures. ACM Trans. Prog. Lang. Syst. 37, 2 (2015), 6:1–6:50.Google ScholarDigital Library
- Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv. 51, 6 (2019). DOI: https://doi.org/10.1145/3280984Google ScholarDigital Library
- Marco Patrignani and Dave Clarke. 2015. Fully abstract trace semantics for protected module architectures. Comput. Lang., Sys. Struct. 42 (2015), 22–45.Google ScholarDigital Library
- Marco Patrignani and Deepak Garg. 2017. Secure compilation and hyperproperty preservation. In Proceedings of the 30th IEEE Computer Security Foundations Symposium. IEEE Computer Society, 392–404.Google ScholarCross Ref
- Marco Patrignani and Marco Guarnieri. 2019. Exorcising spectres with secure compilers. CoRR abs/1910.08607 (2019).Google Scholar
- Michael Schwarz, Samuel Weiser, and Daniel Gruss. 2019. Practical enclave malware with Intel SGX. CoRR abs/1902.03256 (2019).Google Scholar
- Michael Schwarz, Samuel Weiser, Daniel Gruss, Clémentine Maurice, and Stefan Mangard. 2017. Malware guard extension: Using SGX to conceal cache attacks. In Proceedings of the International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment. Springer, 3–24.Google ScholarCross Ref
- Adrian Tang, Simha Sethumadhavan, and Salvatore J. Stolfo. 2017. CLKSCREW: Exposing the perils of security-oblivious energy management. In Proceedings of the 26th USENIX Security Symposium. USENIX Association, 1057–1074. Retrieved from https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/tang.Google Scholar
- Jo Van Bulck. 2020. Microarchitectural Side-channel Attacks for Privileged Software Adversaries. Ph.D. Dissertation. KU Leuven, Leuven, Belgium. Retrieved from https://lirias.kuleuven.be/3047121.Google Scholar
- Jo Van Bulck, Frank Piessens, and Raoul Strackx. 2018. Nemesis: Studying microarchitectural timing leaks in rudimentary CPU interrupt logic. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM, 178–195. DOI: https://doi.org/10.1145/3243734.3243822Google Scholar
- Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan. 2021. Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5, POPL (Jan. 2021). DOI: https://doi.org/10.1145/3434330Google Scholar
- Marco Vassena, Alejandro Russo, Pablo Buiras, and Lucas Waye. 2018. MAC. A verified static information-flow control library. J. Logic. Algeb. Meth. Prog. 95 (2018), 148–180.Google ScholarCross Ref
- Nico Weichbrodt, Anil Kurmus, Peter R. Pietzuch, and Rüdiger Kapitza. 2016. AsyncShock: Exploiting synchronisation bugs in Intel SGX enclaves. In Proceedings of the European Symposium on Research in Computer Security. Springer, 440–457. DOI: https://doi.org/10.1007/978-3-319-45744-4_22Google ScholarCross Ref
- Yuanzhong Xu, Weidong Cui, and Marcus Peinado. 2015. Controlled-channel attacks: Deterministic side channels for untrusted operating systems. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 640–656. DOI: https://doi.org/10.1109/SP.2015.45Google ScholarDigital Library
- Drew Zagieboylo, G. Edward Suh, and Andrew C. Myers. 2019. Using information flow to design an ISA that controls timing channels. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium. IEEE, 272–287. DOI: https://doi.org/10.1109/CSF.2019.00026Google Scholar
- Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. 2015. A hardware design language for timing-sensitive information-flow security. In Proceedings of the 20th International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, 503–516. DOI: https://doi.org/10.1145/2694344.2694372Google Scholar
Index Terms
- Securing Interruptible Enclaved Execution on Small Microprocessors
Recommendations
Verifying the Security of Enclaved Execution Against Interrupt-based Side-channel Attacks
TIS'19: Proceedings of ACM Workshop on Theory of Implementation Security WorkshopComputing platforms sometimes provide hardware support for enclaves or trusted execution environments. On such platforms, security critical code can execute in an enclave or secure world, isolated from all other software on the platform.
But the past ...
Intel Software Guard Extensions: Introduction and Open Research Challenges
SPRO '16: Proceedings of the 2016 ACM Workshop on Software PROtectionHardware-enhanced security is an important pillar of secure systems in general and software protection in particular. This presentation will survey the recently announced Intel Software Guard Extensions (Intel SGX) as well as innovative usages for ...
Exorcising Spectres with Secure Compilers
CCS '21: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Securityttackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using Spectre attacks. To mitigate these attacks, popular compilers deployed a wide range of countermeasures whose security, ...
Comments