The Open-Source Privacy Project Making Untrusted Devices Work Together Securely

Authors: (1) Mathias Brossard, Systems Group, Arm Research; (2) Guilhem Bryant, Systems Group, Arm Research; (3) Basma El Gaabouri, Systems Group, Arm Research; (4) Xinxin Fan, IoTeX.io; (5) Alexandre Ferreira, Systems Group, Arm Research; (6) Edmund Grimley-Evans, Systems Group, Arm Research; (7) Christopher Haster, Systems Group, Arm Research; (8) Evan Johnson, University of California, San Diego; (9) Derek Miller, Systems Group, Arm Research; (10) Fan Mo, Imperial College London; (11) Dominic P. Mulligan, Systems Group, Arm Research; (12) Nick Spinale, Systems Group, Arm Research; (13) Eric van Hensbergen, Systems Group, Arm Research; (14) Hugo J. M. Vincent, Systems Group, Arm Research; (15) Shale Xiong, Systems Group, Arm Research. Authors: Authors: (1) Mathias Brossard, Systems Group, Arm Research; (2) Guilhem Bryant, Systems Group, Arm Research; (3) Basma El Gaabouri, Systems Group, Arm Research; (4) Xinxin Fan, IoTeX.io; (5) Alexandre Ferreira, Systems Group, Arm Research; (6) Edmund Grimley-Evans, Systems Group, Arm Research; (7) Christopher Haster, Systems Group, Arm Research; (8) Evan Johnson, University of California, San Diego; (9) Derek Miller, Systems Group, Arm Research; (10) Fan Mo, Imperial College London; (11) Dominic P. Mulligan, Systems Group, Arm Research; (12) Nick Spinale, Systems Group, Arm Research; (13) Eric van Hensbergen, Systems Group, Arm Research; (14) Hugo J. M. Vincent, Systems Group, Arm Research; (15) Shale Xiong, Systems Group, Arm Research. Editor's note: this is part 6 of 6 of a study detailing the development of a framework to help people collaborate securely. Read the rest below. Editor's note: this is part 6 of 6 of a study detailing the development of a framework to help people collaborate securely. Read the rest below. Editor's note: this is part 6 of 6 of a study detailing the development of a framework to help people collaborate securely. Read the rest below. Editor's note: this is part 6 of 6 of a study detailing the development of a framework to help people collaborate securely. Read the rest below. Table of Links Abstract and 1 Introduction 2 Hardware-backed Confidential Computing 3 IceCap 4 Veracruz 4.1 Attestation 4.2 Programming model 4.3 Ad hoc acceleration 4.4 Threat model 5 Evaluation and 5.1 Case-study: deep learning 5.2 Case-study: video object detection 5.3 Further comparisons 6 Closing remarks and References Abstract and 1 Introduction Abstract and 1 Introduction 2 Hardware-backed Confidential Computing 2 Hardware-backed Confidential Computing 3 IceCap 3 IceCap 4 Veracruz 4.1 Attestation 4.2 Programming model 4.3 Ad hoc acceleration 4.4 Threat model 4 Veracruz 4.1 Attestation 4.2 Programming model 4.3 Ad hoc acceleration 4.4 Threat model 4.1 Attestation 4.2 Programming model 4.3 Ad hoc acceleration 4.4 Threat model 5 Evaluation and 5.1 Case-study: deep learning 5.2 Case-study: video object detection 5.3 Further comparisons 5 Evaluation and 5.1 Case-study: deep learning 5.2 Case-study: video object detection 5.3 Further comparisons 5.2 Case-study: video object detection 5.2 Case-study: video object detection 5.3 Further comparisons 5.3 Further comparisons 6 Closing remarks and References 6 Closing remarks and References 6 Closing remarks We have introduced Veracruz, a framework for designing and deploying privacy-preserving delegated computations among a group of mutually mistrusting principals, using isolates as a “neutral ground” to protect computations from prying or interference. In addition to supporting a number of hardware-backed Confidential Computing technologies— such as AWS Nitro Enclaves and Arm Confidential Computing Architecture Realms—Veracruz also supports pragmatic “software isolates” through IceCap. IceCap makes use of the high-assurance seL4 microkernel, on Armv8-A platforms without any other explicit support for Confidential Computing, to provide strong isolation guarantees for virtual machines. Veracruz, with IceCap, provides a uniform programming and attestation model across emerging and “legacy” hardware platforms, easing the deployment of delegated computations. Both projects are open-source [45,89], and Veracruz is adopted by the LF’s Confidential Computing Consortium. Related work Isolates have been used to protect a zoo of computations of interest, e.g., ML [20, 54, 72, 83, 85] and genomic computations [21, 56, 59], and have been used to emulate or speed up cryptographic techniques such as functional encryption [36] and secure multi-party computations [35,40,76]. These can be seen as use-cases, specialized with a particular policy and program, of Veracruz. Related work OpenEnclave [73] provides a common development platform for SGX Enclaves and TrustZone trusted applications. Veracruz provides a higher-level of abstraction than OpenEnclave, and includes various support libraries, client code, and attestation protocols to ease the provisioning of programs into an isolate. Veracruz also supports a wider range of isolates, including both hardware- and software-isolates. OpenEnclave Previous work [52] suggested a framework similar to Veracruz, but never implemented it. Google Oak [39], Profian Enarx [77], Apache Teaclave [5], Fortanix Confidential Computing Manager [37] and SCONE [8] are similar to Veracruz, though significant differences exist. Oak’s emphasis is information flow control, while Enarx, Fortanix, and SCONE protect the integrity of legacy computations, either requiring recompilation to Wasm, or supporting containerized workloads under SGX, respectively. Apache Teaclave is the most similar project, discussed in §5, and we perform significantly better. The proxy attestation service, and our certificate-based attestation protocol, especially suitable for clients on resource-constrained devices, is also unique. Protected KVM (pKVM) [31,34] is an attempt to minimize the TCB of KVM, enabling virtualization-based confidential computing on mobile platform, and similar in spirit to IceCap. pKVM, with an EL2 kernel specifically designed for the task, may have higher performance than IceCap, but will not benefit from the formal verification effort invested in seL4. Protected KVM (pKVM) OPERA [23] places a proxy between client code and the Intel Attestation Service, exposing the same EPID protocol to clients as the web-service exposes. The Veracruz proxy exposes a potentially different protocol to client code, compared to the native protocol, due to the variety of isolates Veracruz supports. Intel’s Data Center Attestation Primitives (DCAP), also serves similar use-cases, reducing the number of calls to an external attestation service when authenticating attestation tokens, though is limited to use with Intel SGX. OPERA Ongoing and future work The proxy attestation service, which currently signs each generated certificate with the same key, could sign certificates for different isolation technologies with different keys, each associated with a different root CA certificate. With this, a global policy could choose which technology to support based on the selection of root CA certificate embedded in the policy, and if multiple isolation technologies were to be supported, more than one root CA certificate could be embedded. The proxy attestation server could also maintain multiple Root CA certificates, arranged into a “decision tree of certificates”, with the server choosing a CA certificate to use when signing the isolate’s certificate from the tree, following a path from the root described by characteristics of the isolate technology itself (e.g., name of the manufacturer, whether memory encryption is supported, and so on). Again, the certificate associated with the security profile of the desired isolation technology can be embedded in the policy. Ongoing and future work We also aim to bound the intensional and extensional properties of programs provisioned into Veracruz. Pragmatically, cryptographic operations are perhaps most sensitive to timing attacks, and we aim to provide a limited defense by supplying a constant-time cryptography implementation—using mbedtls [60]—via the native module facility discussed in §4.3. Moreover, we aim to explore the use of a statically verified, constant-time virtual machine to gives users the option to statically verify timing properties of their programs—an area of significant recent academic interest—though likely at the cost of limiting their program to constant-time constructs, which is intractable for general-purpose programming. Using FaCT [19] Veracruz could provide flexible, verifiably constant-time components such as virtual machines or domain specific functions, while the CT-Wasm [95] extension for Wasm also provides verifiable, constant-time guarantees as a set of secrecy-aware types and bytecode instructions. CT-Wasm has not yet adopted by the Wasm committee. We are also continuing work on statically verifying the Software Fault Isolation (SFI, henceforth) safety of sandboxed applications. SFI systems, such as Wasm, add runtime checks to loads, stores, and control flow transfers to ensure sandboxed code cannot escape from its address space region, though bugs in SFI compilers can (and do) incorrectly remove these checks and introduce bugs that let untrusted code escape its sandbox [12,43]. To address this—following other SFI systems [65, 99, 102]—we have built a static verifier for binary code executed by Veracruz, implemented as an extension of VeriWasm [49], an open-source SFI verifier for compiled Wasm code. To adapt VeriWasm to Veracruz, we added support for AArch64, and ported VeriWasm from the Lucet [17] toolchain to Wasmtime, as used by Veracruz. We plan to further extend VeriWasm to check other properties besides software fault isolation, e.g., Spectre [70] resistance. Finally, observe that the provisioned program, π, is either kept classified by its owner, or is declassified to a subset of the other principals in the computation (maybe all). In the former case, other principals either must either implicitly trust that π behaves in a particular way, or establish some other mechanism bounding the behavior of the program, outof-band of Veracruz. We aim for a middle ground, allowing a program owner to declassify runtime properties of the program, enforced by Veracruz, while retaining secrecy of the program binary (using e.g., [66]). References [1] Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dandelion Mané, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. TensorFlow: Large-scale machine learning on heterogeneous systems, 2015. Software available from tensorflow.org. [2] Alexandru Agache, Marc Brooker, Alexandra Iordache, Anthony Liguori, Rolf Neugebauer, Phil Piwonka, and Diana-Maria Popa. Firecracker: Lightweight virtualization for serverless applications. In NSDI, 2020. [3] Bytecode Alliance. WebAssembly Micro Runtime main development repository. https://github. com/bytecodealliance/wasm-micro-runtime. Accessed 2022-02-01. [4] D.P. Anderson and G. Fedak. The computational and storage potential of volunteer computing. In Sixth IEEE International Symposium on Cluster Computing and the Grid (CCGRID’06), volume 1, pages 73–80, 2006. [5] Apache Teaclave main development repository. https://github.com/apache/ incubator-teaclave. Accessed 2022-01-26. [6] Arm Confidential Compute Architecture (Arm CCA). https://www.arm. com/architecture/security-features/ arm-confidential-compute-architecture. Accessed 2022-01-20. [7] Arm TrustZone technology for Cortex-A and CortexM. https://developer.arm.com/ip-products/ security-ip/trustzone. Accessed 2022-01-26. [8] Sergei Arnautov, Bohdan Trach, Franz Gregor, Thomas Knauth, André Martin, Christian Priebe, Joshua Lind, Divya Muthukumaran, Dan O’Keeffe, Mark Stillwell, David Goltzsche, David M. Eyers, Rüdiger Kapitza, Peter R. Pietzuch, and Christof Fetzer. SCONE: Secure Linux containers with Intel SGX. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, pages 689–703, 2016. [9] AWS Nitro Enclaves user guide: Cryptographic attestation. https://docs.aws.amazon.com/ enclaves/latest/user/set-up-attestation. html. Accessed 2022-01-12. [10] Eugene Bagdasaryan, Andreas Veit, Yiqing Hua, Deborah Estrin, and Vitaly Shmatikov. How to backdoor federated learning. In International Conference on Artificial Intelligence and Statistics, pages 2938–2948. PMLR, 2020. [11] Junjie Bai, Fang Lu, Ke Zhang, et al. ONNX: the Open Neural Network Exchange format. https:// github.com/onnx/onnx. Accessed 2022-01-24. [12] Alexandre Bartel and John Doe. Twenty years of escaping the Java sandbox. In Phrack, 2018. [13] Ferdinand Brasser, Urs Müller, Alexandra Dmitrienko, Kari Kostiainen, Srdjan Capkun, and Ahmad-Reza Sadeghi. Software Grand Exposure: SGX cache attacks are practical. In 11th USENIX Workshop on Offensive Technologies (WOOT 17), Vancouver, BC, August 2017. USENIX Association. [14] Ernie Brickell and Jiangtao Li. Enhanced Privacy ID from bilinear pairing for hardware authentication and attestation. In 2010 IEEE Second International Conference on Social Computing, pages 768–775, 2010. [15] Ernie Brickell and Jiangtao Li. Enhanced privacy ID: A direct anonymous attestation scheme with enhanced revocation capabilities. IEEE Trans. Dependable Secur. Comput., 9(3):345–360, 2012. [16] Jo Van Bulck, Nico Weichbrodt, Rüdiger Kapitza, Frank Piessens, and Raoul Strackx. Telling your secrets without page faults: Stealthy page table-based attacks on enclaved execution. In 26th USENIX Security Symposium (USENIX Security 17), pages 1041– 1056, Vancouver, BC, August 2017. USENIX Association. [17] Bytecode Alliance. Lucet. https://github.com/ bytecodealliance/lucet. Accessed 2022-01-25. [18] The CapDL domain specific language documentation. https://docs.sel4.systems/projects/ capdl/. Accessed 2022-01-25. [19] Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, and Deian Stefan. FaCT: A DSL for timing-sensitive computation. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, page 174–189, New York, NY, USA, 2019. Association for Computing Machinery. [20] Swarup Chandra, Vishal Karande, Zhiqiang Lin, Latifur Khan, Murat Kantarcioglu, and Bhavani Thuraisingham. Securing data analytics on SGX with randomization. In Simon N. Foley, Dieter Gollmann, and Einar Snekkenes, editors, Computer Security – ESORICS 2017, pages 352–369, Cham, 2017. Springer International Publishing. [21] Feng Chen, Chenghong Wang, Wenrui Dai, Xiaoqian Jiang, Noman Mohammed, Md Momin Al Aziz, Md Nazmus Sadat, Cenk Sahinalp, Kristin Lauter, and Shuang Wang. PRESAGE: PRivacy-preserving gEnetic testing via SoftwAre Guard Extension. BMC Med Genomics, 10(Suppl 2):48, Jul 2017. [22] Guoxing Chen, Sanchuan Chen, Yuan Xiao, Yinqian Zhang, Zhiqiang Lin, and Ten H. Lai. SgxPectre: Stealing Intel secrets from SGX Enclaves via speculative execution. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P), pages 142–157, 2019. [23] Guoxing Chen, Yinqian Zhang, and Ten-Hwang Lai. OPERA: Open remote attestation for Intel’s secure enclaves. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS ’19, page 2317–2331, New York, NY, USA, 2019. Association for Computing Machinery. [24] Zitai Chen, Georgios Vasilakis, Kit Murdock, Edward Dean, David Oswald, and Flavio D. Garcia. VoltPillager: Hardware-based fault injection attacks against Intel SGX enclaves using the SVID voltage scaling interface. In 30th USENIX Security Symposium (USENIX Security 21), pages 699–716. USENIX Association, August 2021. [25] The Linux Foundation’s Confidential Computing Consortium (CCC) homepage. https:// confidentialcomputing.io. Accessed 2022-01- 27. [26] cONNXr: a pure C runtime for ONNX. https:// github.com/alrevuelta/cONNXr. Accessed 2022- 01-24. [27] Lucian Constantin. Intel SGX users need CPU microcode patch to block PLATYPUS secrets-leaking attack. https:// www.csoonline.com/article/3596564/ intel-sgx-users-need-cpu-microcode-patch-to-block-plhtml. Accessed 2022-01-24. [28] D. Cooper, S. Santesson, S. Farrell, S. Boeyen, R. Housley, and W. Polk. Internet X.509 public key infrastructure certificate and certificate revocation list (CRL) profile. RFC 5280, RFC Editor, May 2008. [29] Victor Costan and Srinivas Devadas. Intel SGX explained. IACR Cryptology ePrint Archive, 2016, 2016. [30] Fergus Dall, Gabrielle De Micheli, Thomas Eisenbarth, Daniel Genkin, Nadia Heninger, Ahmad Moghimi, and Yuval Yarom. Cachequote: Efficiently recovering long-term secrets of SGX EPID via cache attacks. IACR Trans. Cryptogr. Hardw. Embed. Syst., 2018(2):171–191, 2018. [31] Will Deacon. Virtualization for the masses: Exposing KVM on Android. In The KVM Forum, 2022. Accessed 2022-01-28. [32] Jeffrey Dean and Sanjay Ghemawat. MapReduce: Simplified data processing on large clusters. In Sixth Symposium on Operating System Design and Implementation (OSDI), pages 137–150, San Francisco, CA, 2004. [33] Ran Duan, Long Li, Chan Zhao, Shi Jia, Yu Ding, Yulong Zhang, Huibo Wang, Yueqiang Cheng, Lenx Wei, and Tanghui Chen. Rust SGX SDK. https://github.com/apache/ incubator-teaclave-sgx-sdk, Jun 2020. Accessed 2020-04-15. [34] Jake Edge. KVM for Android. https://lwn.net/ Articles/836693/, 2020. Accessed 2022-01-27. [35] Susanne Felsen, Ágnes Kiss, Thomas Schneider, and Christian Weinert. Secure and private function evaluation with Intel SGX. In Proceedings of the 2019 ACM SIGSAC Conference on Cloud Computing Security Workshop, CCSW’19, page 165–181, New York, NY, USA, 2019. Association for Computing Machinery. [36] Ben Fisch, Dhinakaran Vinayagamurthy, Dan Boneh, and Sergey Gorbunov. IRON: Functional encryption using Intel SGX. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17, page 765–782, New York, NY, USA, 2017. Association for Computing Machinery. [37] Fortanix Confidential Computing Manager homepage. https://support.fortanix.com/hc/en-us. Accessed 2022-01-27. [38] Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. Time protection: The missing os abstraction. In Proceedings of the Fourteenth EuroSys Conference 2019, EuroSys ’19, New York, NY, USA, 2019. Association for Computing Machinery. [39] Google project Oak. https://github.com/ project-oak/oak. Accessed 2020-04-15. [40] Debayan Gupta, Benjamin Mood, Joan Feigenbaum, Kevin Butler, and Patrick Traynor. Using Intel Software Guard Extensions for efficient two-party secure function evaluation. In Jeremy Clark, Sarah Meiklejohn, Peter Y.A. Ryan, Dan Wallach, Michael Brenner, and Kurt Rohloff, editors, Financial Cryptography and Data Security, pages 302–318, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. [41] Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. Bringing the web up to speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, page 185–200, New York, NY, USA, 2017. Association for Computing Machinery. [42] Shai Halevi. Advanced cryptography: Promise and challenges. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS), CCS ’18, page 647, New York, NY, USA, 2018. Association for Computing Machinery. [43] L. Hansen. Mark the jump_table_entry instruction as loading. https://github.com/ bytecodealliance/cranelift/pull/805. Accessed 2022-01-25. [44] Tianlin Huo, Xiaoni Meng, Wenhao Wang, Chunliang Hao, Pei Zhao, Jian Zhai, and Mingshu Li. Bluethunder: A 2-level directional predictor based side-channel attack against SGX. IACR Trans. Cryptogr. Hardw. Embed. Syst., 2020(1):321–347, 2020. [45] The IceCap development repository. URL redacted for double-blind review. Accessed 2022-01-27. [46] Intel Trust Domain Extensions (Intel TDX): White paper (v4). https://www.intel.com/content/ dam/develop/external/us/en/documents/ tdx-whitepaper-v4.pdf. Accessed 2022-01-25. [47] Ucam. https://ucam.iotex.io/. Accessed 2022- 01-27. [48] Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Sorin Lerner, Tyler McMullen, Stefan Savage, and Deian Stefan. Довер´яй, но провер´яй: SFI safety for native-compiled Wasm. In NDSS. Internet Society, 2021. [49] Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Sorin Lerner, Tyler McMullen, Stefan Savage, and Deian Stefan. Trust, but verify: SFI safety for native-compiled Wasm. In Network and Distributed System Security Symposium (NDSS). Internet Society, 2021. [50] David Kaplan, Jeremy Powell, and Tom Woller. AMD memory encryption: white paper (v7). https://developer.amd.com/wordpress/media/ 2013/12/AMD_Memory_Encryption_Whitepaper_ v7-Public.pdf, 2016. Accessed 2022-01-25. [51] Avi Kivity, Yaniv Kamay, Dor Laor, Uri Lublin, and Anthony Liguori. KVM: the Linux virtual machine monitor. In In Proceedings of the 2007 Ottawa Linux Symposium (OLS’-07, 2007. [52] Patrick Koeberl, Vinay Phegade, Anand Rajan, Thomas Schneider, Steffen Schulz, and Maria Zhdanova. Time to rethink: Trust brokerage using Trusted Execution Environments. In Mauro Conti, Matthias Schunter, and Ioannis G. Askoxylakis, editors, Trust and Trustworthy Computing - 8th International Conference, TRUST 2015, Heraklion, Greece, August 24-26, 2015, Proceedings, volume 9229 of Lecture Notes in Computer Science, pages 181–190. Springer, 2015. [53] The Kubernetes project homepage. https:// kubernetes.io/docs/home/. Accessed 2022-01- 25. [54] Roland Kunkel, Do Le Quoc, Franz Gregor, Sergei Arnautov, Pramod Bhatotia, and Christof Fetzer. TensorSCONE: a secure TensorFlow framework using Intel SGX. CoRR, abs/1902.04413, 2019. [55] Ihor Kuz, Gerwin Klein, Corey Lewis, and Adam Walker. capDL: A language for describing capabilitybased systems. In Proceedings of the 1 st ACM AsiaPacific Workshop on Systems (APSys), pages 31–36, 06 2010. [56] C. Lambert, M. Fernandes, J. Decouchant, and P. Esteves-Verissimo. MaskAl: Privacy preserving masked reads alignment using Intel SGX. In 2018 IEEE 37th Symposium on Reliable Distributed Systems (SRDS), pages 113–122, 2018. [57] Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. Gradient-based learning applied to document recognition. Proceedings of the IEEE, 86(11):2278–2324, 1998. [58] Jaehyuk Lee, Jinsoo Jang, Yeongjin Jang, Nohyun Kwak, Yeseul Choi, Changho Choi, Taesoo Kim, Marcus Peinado, and Brent Byunghoon Kang. Hacking in darkness: Return-oriented programming against secure enclaves. In Proceedings of the 26th USENIX Conference on Security Symposium, SEC’17, page 523–539, USA, 2017. USENIX Association. [59] Avradip Mandal, John C. Mitchell, Hart Montgomery, and Arnab Roy. Data oblivious genome variants search on Intel SGX. In Joaquin Garcia-Alfaro, Jordi Herrera-Joancomartí, Giovanni Livraga, and Ruben Rios, editors, Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 296–310, Cham, 2018. Springer International Publishing. [60] MbedTLS cryptography library. https://www. trustedfirmware.org/projects/mbed-tls/. Accessed 2022-01-25. [61] The Microsoft SEAL fully-homomorphic encryption library development repository (v3.7). https:// github.com/Microsoft/SEAL. Accessed 2022-01- 26. [62] Fan Mo, Hamed Haddadi, Kleomenis Katevas, Eduard Marin, Diego Perino, and Nicolas Kourtellis. PPFL: privacy-preserving federated learning with trusted execution environments. In Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services, pages 94–108, 2021. [63] Fan Mo, Ali Shahin Shamsabadi, Kleomenis Katevas, Soteris Demetriou, Ilias Leontiadis, Andrea Cavallaro, and Hamed Haddadi. Darknetz: towards model privacy at the edge using trusted execution environments. In Proceedings of the 18th International Conference on Mobile Systems, Applications, and Services, pages 161–174, 2020. [64] Ahmad Moghimi, Gorka Irazoqui, and Thomas Eisenbarth. Cachezoom: How SGX amplifies the power of cache attacks. In Wieland Fischer and Naofumi Homma, editors, Cryptographic Hardware and Embedded Systems (CHES), volume 10529 of Lecture Notes in Computer Science, pages 69–90. Springer, 2017. [65] Greg Morrisett, Gang Tan, Joseph Tassarotti, JeanBaptiste Tristan, and Edward Gan. RockSalt: better, faster, stronger SFI for the x86. In Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, pages 395–404, 2012. [66] Dominic P. Mulligan and Nick Spinale. The Supervisionary proof-checking kernel, or: a work-in-progress towards proof-generating code (extended abstract). https://dominicpm.github.io/publications/ mulligan-supervisionary-2022.pdf, 2022. [67] Kit Murdock, David Oswald, Flavio D. Garcia, Jo Van Bulck, Daniel Gruss, and Frank Piessens. Plundervolt: Software-based fault injection attacks against Intel SGX. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P’20), 2020. [68] Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. sel4: From general purpose to a proof of information flow enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013, pages 415–429, 2013. [69] Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, and Gerwin Klein. Noninterference for operating system kernels. In Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings, pages 126–142, 2012. [70] Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, and Deian Stefan. Swivel: Hardening WebAssembly against Spectre. In USENIX Security Symposium. USENIX, August 2021. [71] M. Nystrom and B. Kaliski. PKCS #10: Certification request syntax specification version 1.7. RFC 2986, RFC Editor, November 2000. [72] Olga Ohrimenko, Felix Schuster, Cédric Fournet, Aastha Mehta, Sebastian Nowozin, Kapil Vaswani, and Manuel Costa. Oblivious multi-party machine learning on trusted processors. In Proceedings of the 25th USENIX Conference on Security Symposium, SEC’16, page 619–636, USA, 2016. USENIX Association. [73] The OpenEnclave development repository. https:// github.com/openenclave/openenclave. Accessed 2022-01-27. [74] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32, pages 8024–8035. Curran Associates, Inc., 2019. [75] The PolyBench/C benchmarking suite homepage. http://web.cs.ucla.edu/~pouchet/software/ polybench/. Accessed 2022-01-28. [76] Bernardo Portela, Manuel B M Barbosa, Ferdinand Brasser, Bernardo Portela, Ahmad-Reza Sadeghi, Guillaume Scerri, and Bogdan Warinschi. Secure multiparty computation from SGX. In Financial Cryptography and Data Security 2017. International Financial Cryptography Association, April 2017. [77] Profian Enarx development repository. https:// github.com/enarx/enarx. Accessed 2022-01-26. [78] Joseph Redmon. Darknet: open source neural network framework written in C and CUDA. https:// github.com/pjreddie/darknet, 2013–2016. Accessed 2022-01-24. [79] Joseph Redmon and Ali Farhadi. YOLOv3: An incremental improvement. arXiv, 2018. [80] Andreas Rossberg, Ben L. Titzer, Andreas Haas, Derek L. Schuff, Dan Gohman, Luke Wagner, Alon Zakai, J. F. Bastien, and Michael Holman. Bringing the web up to speed with WebAssembly. Commun. ACM, 61(12):107–115, 2018. [81] seL4 inter-process communication (IPC) documentation. https://docs.sel4.systems/Tutorials/ ipc.html. Accessed 2022-01-25. [82] Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, and Gerwin Klein. sel4 enforces integrity. In Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pages 325–340, 2011. [83] Fahad Shaon, Murat Kantarcioglu, Zhiqiang Lin, and Latifur Khan. SGX-BigMatrix: A practical encrypted data analytic framework with trusted processors. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17, page 1211–1228, New York, NY, USA, 2017. Association for Computing Machinery. [84] Adrian Tang, Simha Sethumadhavan, and Salvatore Stolfo. CLKSCREW: Exposing the perils of SecurityOblivious energy management. In 26th USENIX Security Symposium (USENIX Security 17), pages 1057– 1074, Vancouver, BC, August 2017. USENIX Association. [85] Florian Tramèr and Dan Boneh. Slalom: Fast, verifiable and private execution of neural networks in trusted hardware. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019. [86] H. Tschofenig, S. Frost, M. Brossard, A. Shaw, and T. Fossati. Arm’s Platform Security Architecture (PSA) attestation token, Nov 2019. Accessed 2020- 04-15. [87] Jo Van Bulck, Frank Piessens, and Raoul Strackx. SGX-Step: A practical attack framework for precise enclave execution control. In Proceedings of the 2nd Workshop on System Software for Trusted Execution, SysTEX’17, New York, NY, USA, 2017. Association for Computing Machinery. [88] Jo Van Bulck, Frank Piessens, and Raoul Strackx. Nemesis: Studying microarchitectural timing leaks in rudimentary CPU interrupt logic. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS ’18, page 178–195, New York, NY, USA, 2018. Association for Computing Machinery. [89] The Veracruz development repository. URL redacted for double-blind review. Accessed 2022-01-27. [90] The WASMI WebAssembly interpreter. https:// docs.rs/wasmi. Accessed 2022-01-27. [91] Wasmtime: a just-in-time compiler for WebAssembly. https://wasmtime.dev. Accessed 2020-04-15. [92] Robert N. M. Watson, Jonathan Anderson, Ben Laurie, and Kris Kennaway. A taste of Capsicum: practical capabilities for UNIX. Commun. ACM, 55(3):97– 104, 2012. [93] Conrad Watt. Mechanising and verifying the WebAssembly specification. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 53–65, 2018. [94] Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. Two mechanisations of WebAssembly 1.0. In Proceedings of the 24th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, 2021. [95] Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan. CT-Wasm: Type-driven secure cryptography for the Web ecosystem. Proc. ACM Program. Lang., 3(POPL), jan 2019. [96] The WebAssembly project homepage. https:// webassembly.org/. Accessed 2022-01-20. [97] The WebAssembly System Interface (Wasi) homepage. https://wasi.dev. Accessed 2022-01-27. [98] Yuanzhong Xu, Weidong Cui, and Marcus Peinado. Controlled-channel attacks: Deterministic side channels for untrusted operating systems. In 2015 IEEE Symposium on Security and Privacy, pages 640–656, 2015. [99] Bennet Yee, David Sehr, Gregory Dardyk, J Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. Native client: A sandbox for portable, untrusted x86 native code. In 2009 30th IEEE Symposium on Security and Privacy, pages 79–93. IEEE, 2009. [100] The Zephyr project homepage. https://www. zephyrproject.org/. Accessed 2022-01-31. [101] Ning Zhang, Kun Sun, Deborah Shands, Wenjing Lou, and Y. Thomas Hou. Trusense: Information leakage from TrustZone. In 2018 IEEE Conference on Computer Communications, INFOCOM 2018, Honolulu, HI, USA, April 16-19, 2018, pages 1097–1105. IEEE, 2018. [102] Lu Zhao, Guodong Li, Bjorn De Sutter, and John Regehr. Armor: fully verified software fault isolation. In Proceedings of the ninth ACM international conference on Embedded software, pages 289–298, 2011. This paper is available on arxiv under CC BY 4.0 DEED license. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv