research-article

Open access

Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing

Authors:

Alexander Thomas,

Pranav Gaddamadugu,

Anjo Vahldiek-Oberwagner,

Sanjit A. Seshia,

Krste AsanovicAuthors Info & Claims

CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security

Pages 1871 - 1885

https://doi.org/10.1145/3548606.3560595

Published: 07 November 2022 Publication History

Abstract

Hardware enclaves rely on a disjoint memory model, which maps each physical address to an enclave to achieve strong memory isolation. However, this severely limits the performance and programmability of enclave programs. While some prior work proposes enclave memory sharing, it does not provide a formal model or verification of their designs. This paper presents Cerberus, a formal approach to secure and efficient enclave memory sharing. To reduce the burden of formal verification, we compare different sharing models and choose a simple yet powerful sharing model. Based on the sharing model, Cerberus extends an enclave platform such that enclave memory can be made immutable and shareable across multiple enclaves via additional operations. We use incremental verification starting with an existing formal model called the Trusted Abstract Platform (TAP). Using our extended TAP model, we formally verify that Cerberus does not break or weaken the security guarantees of the enclaves despite allowing memory sharing. More specifically, we prove the Secure Remote Execution (SRE) property on our formal model. Finally, the paper shows the feasibility of Cerberus by implementing it in an existing enclave platform, RISC-V Keystone.

References

[1]

[n.d.]. AWS SageMaker. https://aws.amazon.com/pm/sagemaker.

[2]

[n.d.]. Fission.io. https://fission.io/.

[3]

[n.d.]. Huggingface. https://huggingface.co/.

[4]

[n.d.]. OpenFaaS. https://www.openfaas.com/.

[5]

[n.d.]. Ray Serve. https://www.ray.io/ray-serve.

[6]

2013. ARM TrustZone. https://www.arm.com/products/security-on-arm/trustz one.

[7]

2017. RV8 Benchmark. https://github.com/michaeljclark/rv8-bench.

[8]

2020. HiFive Unleashed. https://www.sifive.com/boards/hifive-unleashed.

[9]

2021. Gramine. https://github.com/gramineproject/gramine.

[10]

Adil Ahmad, Juhee Kim, Jaebaek Seo, Insik Shin, Pedro Fonseca, and Byoungyoung Lee. 2021. Chancel: efficient multi-client isolation under adversarial pro- grams. In Proc. of Network and Distributed System Security Symposium (NDSS).

[11]

Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. 2016. Cogent: Verifying High-Assurance File System Implementations. In Proc. of Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS).

Digital Library

[12]

Krste Asanović Andrew Waterman. 2021. The RISC-V Instruction Set Manual Volume II: Privileged Architecture. https://github.com/riscv/riscv-isa-manual/releases/download/Priv-v1.12/riscv-privileged-20211203.pdf.

[13]

Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22) (Lecture Notes in Computer Science). Springer. http://www.cs.stanford.edu/~barrett/pubs/BBB22.pdf

Digital Library

[14]

Mike Barnett, Bor-Yuh Evan Chang, Robert DeLIne, Bart Jacobs, and Rustan Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO 2005 (fmco 2005 ed.). Springer Berlin Heidelberg. https://www.micros oft.com/en-us/research/publication/boogie-a-modular-reusable-verifier-for- object-oriented-programs/

[15]

George S. Boolos, John P. Burgess, and Richard C. Jeffrey. 2007. The Undecidability of First-Order Logic (5 ed.). Cambridge University Press, 126--136. https://doi.or g/10.1017/CBO9780511804076.012

[16]

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 Proc. of USENIX Security Symposium.

[17]

Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Marina Minkin, Daniel Moghimi, Frank Piessens, Michael Schwarz, Berk Sunar, Jo Van Bulck, and Yuval Yarom. 2019. Fallout: Leaking Data on Meltdown-resistant CPUs. In Proc. of ACM SIGSAC Conference on Computer and Communications Security (CCS).

Digital Library

[18]

Chia che Tsai, Donald E. Porter, and Mona Vij. 2017. Graphene-SGX: A Practical Library OS for Unmodified Applications on SGX. In Proc. of USENIX Anual Technical Conference (ATC).

[19]

Kevin Cheang, Cameron Rasmussen, Sanjit Seshia, and Pramod Subramanyan. 2019. A Formal Approach to Secure Speculation. In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019. 288--303. https://doi.org/10.1109/CSF.2019.00027

[20]

Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, and Gernot Heiser. 2017. The Cogent Case for Property-Based Testing. In Proc. of Workshop on Programming Languages and Operating Systems (PLOS) (Shanghai, China). 7. https://doi.org/10.1145/3144555.3144556

Digital Library

[21]

Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In 2008 21st IEEE Computer Security Foundations Symposium. 51--65. https://doi.org/10.1109/ CSF.2008.7

[22]

Victor Costan and Srinivas Devadas. 2016. Intel SGX Explained. Cryptology ePrint Archive, Report 2016/086.

[23]

Victor Costan, Ilia Lebedev, and Srinivas Devadas. 2016. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In Proc. of USENIX Security Symposium.

[24]

Leonardo De Moura and Nikolaj Bjorner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS'08/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337--340.

[25]

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proc. of Symposium on Operating Systems Principles (SOSP).

Digital Library

[26]

Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware-Software Contracts for Secure Speculation. In 2021 IEEE Symposium on Security and Privacy (SP). 1868--1883. https://doi.org/10.1109/SP40001.2021.00036

[27]

Mohit Kumar Jangid, Guoxing Chen, Yinqian Zhang, and Zhiqiang Lin. 2021. Towards Formal Verification of State Continuity for Enclave Programs. In Proc. of USENIX Security Symposium. https://www.usenix.org/conference/usenixsecu rity21/presentation/jangid

[28]

David Kaplan. 2017. AMD SEV-ES. http://support.amd.com/TechDocs/Protectin gVMRegisterStatewithSEV-ES.pdf.

[29]

David Kaplan, Jeremy Powell, and Tom Woller. 2016. http://amd-dev.wpengine.n etdna-cdn.com/wordpress/media/2013/12/AMD _ Memory_ Encryption _ White paper_v7-Public.pdf.

[30]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal Verification of an OS Kernel. In Proc. of Symposium on Operating Systems Principles (SOSP).

Digital Library

[31]

Paul Kocher, 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 Proc. of IEEE Symposium on Security and Privacy (S&P).

[32]

Elisavet Kozyri, Stephen Chong, and Andrew C. Myers. 2022. Expressing Information Flow Properties. Foundations and Trends in Privacy and Security 3, 1 (2022), 1--102. https://doi.org/10.1561/3300000008

[33]

Dmitrii Kuvaiskii, Oleksii Oleksenko, Sergei Arnautov, Bohdan Trach, Pramod Bhatotia, Pascal Felber, and Christof Fetzer. 2017. SGXBOUNDS: Memory safety for shielded execution. In Proc. of the Twelfth European Conference on Computer Systems (EuroSys).

Digital Library

[34]

Ilia Lebedev, Kyle Hogan, Jules Drean, David Kohlbrenner, Dayeol Lee, Krste Asanović, Dawn Song, and Srinivas Devadas. 2019. Sanctorum: A lightweight security monitor for secure enclaves. In Proc. of Design, Automation & Test in Europe Conference & Exhibition (DATE).

[35]

Dayeol Lee, Dongha Jung, Ian T. Fang, Chia-Che Tsai, and Raluca Ada Popa. 2020. An Off-Chip Attack on Hardware Enclaves via the Memory Bus. In Proc. of USENIX Security Symposium.

[36]

Dayeol Lee, David Kohlbrenner, Shweta Shinde, Krste Asanović, and Dawn Song. 2020. Keystone: An Open Framework for Architecting Trusted Execution Environments. In Proc. of European Conference on Computer Systems (EuroSys).

Digital Library

[37]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Proc. of Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Dakar, Senegal). 23.

[38]

Mingyu Li, Yubin Xia, and Haibo Chen. 2021. Confidential Serverless Made Efficient with Plug-in Enclaves. In Proc. of International Symposium on Computer Architecture (ISCA).

Digital Library

[39]

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 Proc. of USENIX Security Symposium.

[40]

Ross Mcilroy, Jaroslav Sevcik, Tobias Tebbi, Ben L Titzer, and Toon Verwaest. 2019. Spectre is here to stay: An analysis of side-channels and speculative execution. arXiv preprint arXiv:1902.05178 (2019).

[41]

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 HASP.

[42]

Marcela S Melara, Michael J Freedman, and Mic Bowman. 2019. EnclaveDom: Privilege separation for large-TCB applications in trusted execution environments. arXiv preprint arXiv:1907.13245 (2019).

[43]

Ahmad Moghimi, Gorka Irazoqui, and Thomas Eisenbarth. 2017. CacheZoom: How SGX Amplifies the Power of Cache Attacks. In CHES.

[44]

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Serval: Scaling Symbolic Evaluation for Automated Verification of Systems Code. In Proc. of Symposium on Operating Systems Principles (SOSP).

Digital Library

[45]

Olga Ohrimenko, Felix Schuster, Cedric Fournet, Aastha Mehta, Sebastian Nowozin, Kapil Vaswani, and Manuel Costa. 2016. Oblivious Multi-Party Machine Learning on Trusted Processors. In Proc. of USENIX Security Symposium.

[46]

Bryan Parno, Jacob R. Lorch, John R. Douceur, James Mickens, and Jonathan M. McCune. 2011. Memoir: Practical State Continuity for Protected Modules. In Proc. of IEEE Symposium on Security and Privacy (S&P).

[47]

Nelly Porter and Jason Garms. 2019. Advancing confidential computing with Asylo and the Confidential Computing Challenge. https://cloud.google.com/blo g/products/identity-security/advancing-confidential-computing-with-asylo- and-the-confidential-computing-challenge.

[48]

Christian Priebe, Kapil Vaswani, and Manuel Costa. 2018. EnclaveDB - A Secure Database using SGX. In Proc. of IEEE Symposium on Security and Privacy (S&P).

[49]

C. R. Reddy and D. W. Loveland. 1978. Presburger Arithmetic with Bounded Quantifier Alternation. In Proceedings of the Tenth Annual ACM Symposium on Theory of Computing (San Diego, California, USA) (STOC '78). Association for Computing Machinery, New York, NY, USA, 320--325. https://doi.org/10.1145/80 0133.804361

[50]

John Rushby. 1982. Proof of Separability: A Verification Technique for a Class of Security Kernels. In Proc. 5th International Symposium on Programming (Lecture Notes in Computer Science, Vol. 137). Springer-Verlag, Turin, Italy, 352--367

[51]

Muhammad Usama Sardar, Saidgani Musaev, and Christof Fetzer. 2021. Demysti- fying Attestation in Intel Trust Domain Extensions via Formal Verification. IEEE Access 9 (2021), 83067--83079. https://doi.org/10.1109/ACCESS.2021.3087421

[52]

Michael Schwarz, Samuel Weiser, Daniel Gruss, Clémentine Maurice, and Stefan Mangard. 2017. Malware Guard Extension: Using SGX to Conceal Cache Attacks. In Proc. of Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA).

[53]

Sanjit A. Seshia and Pramod Subramanyan. 2018. UCLID5: Integrating Modeling, Verification, Synthesis and Learning. In 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). 1--10. https://doi.org/10.1109/MEMCOD.2018.8556946

[54]

Thomas Arthur Leck Sewell, Magnus O Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In Proc. of ACM SIGPLAN Conference on Programming language design and implementation (PLDI).

Digital Library

[55]

Youren Shen, Hongliang Tian, Yu Chen, Kang Chen, Runji Wang, Yi Xu, Yubin Xia, and Shoumeng Yan. 2020. Occlum: Secure and Efficient Multitasking Inside a Single Enclave of Intel SGX. In Proc. of Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS).

Digital Library

[56]

Rohit Sinha, Sriram Rajamani, Sanjit Seshia, and Kapil Vaswani. 2015. Moat: Verifying Confidentiality of Enclave Programs. In Proc. of ACM SIGSAC Conference on Computer and Communications Security (CCS).

Digital Library

[57]

Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas Devadas, and Sanjit A. Seshia. 2017. A Formal Foundation for Secure Remote Execution of Enclaves. In Proc. of ACM SIGSAC Conference on Computer and Communications Security (CCS).

[58]

Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Proc. of ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming; Software (Indianapolis, Indiana, USA). 18. https: //doi.org/10.1145/2509578.2509586

Digital Library

[59]

Jo Van Bulck, Daniel Moghimi, Michael Schwarz, Moritz Lipp, Marina Minkin, Daniel Genkin, Yarom Yuval, Berk Sunar, Daniel Gruss, and Frank Piessens. 2020. LVI: Hijacking Transient Execution through Microarchitectural Load Value Injection. In Proc. of IEEE Symposium on Security and Privacy (S&P).

[60]

Stephan van Schaik, Alyssa Milburn, Sebastian Österlund, Pietro Frigo, Giorgi Maisuradze, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2019. RIDL: Rogue In-flight Data Load. In Proc. of IEEE Symposium on Security and Privacy (S&P).

[61]

Robert Wahbe, Steven Lucco, Thomas E Anderson, and Susan L Graham. 1993. Efficient software-based fault isolation. In Proc. of Symposium on Operating Systems Principles (SOSP).

Digital Library

[62]

Wenhao Wang, Guoxing Chen, Xiaorui Pan, Yinqian Zhang, XiaoFeng Wang, Vincent Bindschaedler, Haixu Tang, and Carl A. Gunter. 2017. Leaky Cauldron on the Dark Land: Understanding Memory Side-Channel Hazards in SGX. In Proc. of ACM SIGSAC Conference on Computer and Communications Security (CCS).

[63]

Ofir Weisse, Valeria Bertacco, and Todd Austin. 2017. Regaining lost cycles with HotCalls: A fast interface for SGX secure enclaves. In ISCA.

[64]

Yuanzhong Xu, Weidong Cui, and Marcus Peinado. 2015. Controlled-Channel Attacks: Deterministic Side Channels for Untrusted Operating Systems. In Proc. of IEEE Symposium on Security and Privacy (S&P).

Digital Library

[65]

Zhijingcheng Yu, Shweta Shinde, Trevor E Carlson, and Prateek Saxena. 2022. Elasticlave: An Efficient Memory Model for Enclaves. In Proc. of USENIX Security Symposium.

[66]

S. Zdancewic and A.C. Myers. 2003. Observational determinism for concurrent program security. In 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings. 29--43. https://doi.org/10.1109/CSFW.2003.1212703

[67]

Kaiyang Zhao, Sishuai Gong, and Pedro Fonseca. 2021. On-Demand-Fork: A Microsecond Fork for Memory-Intensive and Latency-Sensitive Applications. In Proc. of the Sixteenth European Conference on Computer Systems (EuroSys).

Digital Library

Cited By

Zeng FZhang ZChang RYu CZhang ZZhao Y(2023)Lark: Verified Cross-Domain Access Control for Trusted Execution Environments2023 IEEE 34th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE59848.2023.00031(160-171)Online publication date: 9-Oct-2023
https://doi.org/10.1109/ISSRE59848.2023.00031

Index Terms

Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models
    2. Trust frameworks
  2. Systems security
    1. Operating systems security
      1. Trusted computing

Recommendations

An integrated environment for HDL verification
IVC '95: Proceedings of the 4th IEEE International Verilog HDL Conference

The functional verification of a digital design is an expensive step in the design process. As designs become more complex, simulation is challenged throughout the design and verification process, both at the low level (implementation verification), to ...
A cross-process Spectre attack via cache on RISC-V processor with trusted execution environment
Abstract
The trust execution environment (TEE) provides a safe region, also known as a secret enclave, for executing private programs that need protection. This work proposed a cross-process exploitation scheme for conducting the cache side-channel attack,...
Graphical abstract

Display Omitted
Highlights
- Replicate cache side-channel attack variants on an FPGA with the RISC-V processor’s configuration.
- Implement a cross-process side-channel attack via cache scenario for the first time on the RISC-V platform.
- Experiment with cache ...
Using DEv-PROMELA for Modelling and Verification of Software
SIGSIM-PADS '16: Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation

Efficient modelling and verification of models need an accurate representation of systems. Especially, PROMELA cannot represent time as quantitative properties. That means some properties depending on time cannot be checked with SPIN model-checker. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security

November 2022

3598 pages

ISBN:9781450394505

DOI:10.1145/3548606

General Chairs:
Heng Yin
University of California, Riverside
,
Angelos Stavrou
Virginia Tech
,
Program Chairs:
Cas Cremers
CISPA Helmholtz Center for Information Security
,
Elaine Shi
Carnegie Mellon University

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2022

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS '22

Sponsor:

SIGSAC

CCS '22: 2022 ACM SIGSAC Conference on Computer and Communications Security

November 7 - 11, 2022

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
1,263
Total Downloads

Downloads (Last 12 months)583
Downloads (Last 6 weeks)46

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zeng FZhang ZChang RYu CZhang ZZhao Y(2023)Lark: Verified Cross-Domain Access Control for Trusted Execution Environments2023 IEEE 34th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE59848.2023.00031(160-171)Online publication date: 9-Oct-2023
https://doi.org/10.1109/ISSRE59848.2023.00031

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents