{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:19Z","timestamp":1784200219716,"version":"3.55.0"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    Confidential computing (CC), designed for security-critical scenarios, uses remote attestation to guarantee code integrity on cloud servers. However, CC alone cannot provide assurance of high-level security properties (e.g., no data leak) on the code. In this paper, we introduce a novel framework,\n                    <jats:sc>Agora<\/jats:sc>\n                    , scrupulously designed to provide a trustworthy and open verification platform for CC. To prompt trustworthiness, we observe that certain verification tasks can be delegated to untrusted entities, while the corresponding (smaller) validators are securely housed within the trusted computing base (TCB). Moreover, through a novel blockchain-based bounty task manager, it also utilizes crowdsourcing to remove trust in complex theorem provers. These synergistic techniques successfully ameliorate the TCB size burden associated with two procedures: binary analysis and theorem proving. To prompt openness,\n                    <jats:sc>Agora<\/jats:sc>\n                    supports a versatile assertion language that allows verification of various security policies. Moreover, the design of\n                    <jats:sc>Agora<\/jats:sc>\n                    enables untrusted parties to participate in any complex processes out of\n                    <jats:sc>Agora<\/jats:sc>\n                    \u2019s TCB. By implementing verification workflows for software-based fault isolation, information flow control, and side-channel mitigation policies, our evaluation demonstrates the efficacy of\n                    <jats:sc>Agora<\/jats:sc>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3763099","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1372-1399","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Agora: Trust Less and Open More in Verification for Confidential Computing"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9922-4351","authenticated-orcid":false,"given":"Hongbo","family":"Chen","sequence":"first","affiliation":[{"name":"Indiana University Bloomington, Bloomington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3497-7848","authenticated-orcid":false,"given":"Quan","family":"Zhou","sequence":"additional","affiliation":[{"name":"The Pennsylvania State University, University Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8866-2097","authenticated-orcid":false,"given":"Sen","family":"Yang","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3241-9530","authenticated-orcid":false,"given":"Sixuan","family":"Dang","sequence":"additional","affiliation":[{"name":"Duke University, Durham, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9907-0988","authenticated-orcid":false,"given":"Xing","family":"Han","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1942-6872","authenticated-orcid":false,"given":"Danfeng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Duke University, Durham, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8525-4514","authenticated-orcid":false,"given":"Fan","family":"Zhang","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0607-4946","authenticated-orcid":false,"given":"XiaoFeng","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"2275","volume-title":"32nd USENIX Security Symposium (USENIX Security)","author":"Akgul Omer","year":"2023","unstructured":"Omer Akgul, Taha Eghtesad, Amit Elazari, Omprakash Gnawali, Jens Grossklags, Michelle L Mazurek, Daniel Votipka, and Aron Laszka. 2023. Bug hunters\u2019 perspectives on the challenges and benefits of the bug bounty ecosystem. In 32nd USENIX Security Symposium (USENIX Security), Vol. 2301. USENIX Association, USA, 2275\u20132291."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Irem Aktug and Katsiaryna Naliuka. 2008. ConSpec\u2014a formal language for policy specification. Science of Computer Programming 74 1-2 (2008) 2\u201312. doi:10.1016\/j.scico.2008.09.004","DOI":"10.1016\/j.scico.2008.09.004"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Andrew W Appel. 2001. Foundational proof-carrying code. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. IEEE 247\u2013256. doi:10.1109\/LICS.2001.932501","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and Edward W. Felten. 1999. Proof-carrying authentication. In Proceedings of the 6th ACM Conference on Computer and Communications Security (CCS). 52\u201362. doi:10.1145\/319709.319718","DOI":"10.1145\/319709.319718"},{"key":"e_1_3_2_7_2","unstructured":"Apple Inc. 2024. App Review - App Store - Apple Developer. https:\/\/developer.apple.com\/app-store\/review\/. (Accessed on 01\/23\/2024)."},{"key":"e_1_3_2_8_2","unstructured":"Arbitrum. 2023. Arbitrum - Scaling Ethereum. https:\/\/arbitrum.io\/."},{"key":"e_1_3_2_9_2","unstructured":"ARM. 2021. Arm CCA Security Model 1.0. https:\/\/developer.arm.com\/documentation\/DEN0096\/latest."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"e_1_3_2_13_2","unstructured":"Fr\u00e9d\u00e9ric Besson Pascal Fontaine and Laurent Th\u00e9ry. 2011. A flexible proof format for SMT: A proposal. In First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068405222445"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Ajay Brahmakshatriya Piyus Kedia Derrick P McKee Deepak Garg Akash Lal Aseem Rastogi Hamed Nemati Anmol Panda and Pratik Bhatu. 2019. Confllvm: A compiler for enforcing data confidentiality in low-level code. In Proceedings of the Fourteenth EuroSys Conference 2019. 1\u201315. doi:10.1145\/3302424.3303952","DOI":"10.1145\/3302424.3303952"},{"key":"e_1_3_2_16_2","unstructured":"Lorenz Breidenbach Phil Daian Florian Tram\u00e8r and Ari Juels. 2018. Enter the hydra: Towards principled bug bounties and {Exploit-Resistant} smart contracts. In 27th USENIX Security Symposium (USENIX Security). 1335\u20131352."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Sunjay Cauligi Craig Disselkoen Klaus v Gleissenthall Dean Tullsen Deian Stefan Tamara Rezk and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 913\u2013926. doi:10.1145\/3385412.3385970","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_18_2","first-page":"4733","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Chen Hongbo","year":"2023","unstructured":"Hongbo Chen, Haobin Hiroki Chen, Mingshen Sun, Kang Li, Zhaofeng Chen, and XiaoFeng Wang. 2023. A verified confidential computing as a service framework for privacy preservation. In 32nd USENIX Security Symposium (USENIX Security 23). USENIX Association, USA, 4733\u20134750."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Hongbo Chen Quan Zhou Sen Yang Sixuan Dang Xing Han Danfeng Zhang Fan Zhang and XiaoFeng Wang. 2025. Artifact for Paper \"Agora: Trust Less and Open More in Verification for Confidential Computing\" in OOPSLA 2025. doi:10.5281\/zenodo.16922992","DOI":"10.5281\/zenodo.16922992"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Hongbo Chen Quan Zhou Sen Yang Sixuan Dang Xing Han Danfeng Zhang Fan Zhang and XiaoFeng Wang. 2025. Supplementary Material for Paper \"Agora: Trust Less and Open More in Verification for Confidential Computing\" in OOPSLA 2025. doi:10.5281\/zenodo.17083160","DOI":"10.5281\/zenodo.17083160"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Raymond Cheng Fan Zhang Jerne jKos Warren He Nicholas Hynes Noah Johnson Ari Juels Andrew Miller and Dawn Song. 2019. Ekiden: A platform for confidentiality-preserving trustworthy and performant smart contracts. In 4th IEEE European Symposium on Security and Privacy (EuroS&P). IEEE IEEE Computer Society Los Alamitos CA USA 185\u2013200. doi:10.1109\/EuroSP.2019.00023","DOI":"10.1109\/EuroSP.2019.00023"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Zakaria Chihani Dale Miller and Fabien Renaud. 2017. A semantic framework for proof evidence. Journal of Automated Reasoning 59 (2017) 287\u2013330. doi:10.1007\/s10817-016-9380-6","DOI":"10.1007\/s10817-016-9380-6"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Christopher Colby Peter Lee George C Necula Fred Blau Mark Plesko and Kenneth Cline. 2000. A certifying compiler for Java. ACM SIGPLAN Notices 35 5 (2000) 95\u2013107. doi:10.1145\/349299.349315","DOI":"10.1145\/349299.349315"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Emilio Coppa Daniele Cono D\u2019Elia and Camil Demetrescu. 2017. Rethinking pointer reasoning in symbolic execution. In 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE 613\u2013618. doi:10.1109\/ASE.2017.8115671","DOI":"10.1109\/ASE.2017.8115671"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_18"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57231-9_6"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Amir Dembo Sreeram Kannan Ertem Nusret Tas David Tse Pramod Viswanath Xuechao Wang and Ofer Zeitouni. 2020. Everything is a race and nakamoto always wins. In Proceedings of the 27th ACM SIGSAC Conference on Computer and Communications Security (CCS). 859\u2013878. doi:10.1145\/3372297.3417290","DOI":"10.1145\/3372297.3417290"},{"key":"e_1_3_2_29_2","unstructured":"Thomas Dullien and Sebastian Porst. 2009. REIL: A platform-independent intermediate representation of disassembled code for static code analysis. Proceeding of CanSecWest (2009) 1\u20137."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_31_2","unstructured":"Moritz Eckert Antonio Bianchi Ruoyu Wang Yan Shoshitaishvili Christopher Kruegel and Giovanni Vigna. 2018. {HeapHopper}: Bringing bounded model checking to heap implementation security. In 27th USENIX Security Symposium (USENIX Security). 99\u2013116."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24609-1_10"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Thomas Eiter Michael Fink and Stefan Woltran. 2007. Semantical characterizations and complexity of equivalences in answer set programming. ACM Transactions on Computational Logic (TOCL) 8 3 (2007) 17\u2013es. doi:10.1145\/1243996.1244000","DOI":"10.1145\/1243996.1244000"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_2_35_2","unstructured":"Ethereum. 2023. Networks \u2223 ethereum.org. https:\/\/ethereum.org\/en\/developers\/docs\/networks\/."},{"key":"e_1_3_2_36_2","unstructured":"Ethereum. 2025. Solidity \u2014 Solidity 0.8.29 documentation. https:\/\/docs.soliditylang.org\/en\/v0.8.29\/."},{"key":"e_1_3_2_37_2","unstructured":"Erhu Feng Xu Lu Dong Du Bicheng Yang Xueqiang Jiang Yubin Xia Binyu Zang and Haibo Chen. 2021. Scalable Memory Protection in the {PENGLAI} Enclave. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI)). 275\u2013294."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190325"},{"key":"e_1_3_2_39_2","unstructured":"Matthew Finifter Devdatta Akhawe and David Wagner. 2013. An empirical study of vulnerability rewards programs. In 22nd USENIX Security Symposium (USENIX Security). 273\u2013288."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Joseph A Goguen and Jos\u00e9 Meseguer. 1982. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy. IEEE 11\u201311. doi:10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_41_2","unstructured":"Google Inc. 2024. Prepare your app for review - Play Console Help. https:\/\/support.google.com\/googleplay\/androiddeveloper\/answer\/9859455?hl=en. (Accessed on 01\/23\/2024)."},{"key":"e_1_3_2_42_2","unstructured":"HackerOne. 2023. Bug Bounty Programs \u2223 Complete List \u2223 HackerOne. https:\/\/hackerone.com\/bug-bounty-programs."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_10"},{"key":"e_1_3_2_44_2","unstructured":"Jochen Hoenicke and Tanja Schindler. 2022. A Simple Proof Format for SMT.. In SMT. 54\u201370."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"key":"e_1_3_2_46_2","unstructured":"Intel. 2021. Intel\u00ae Trust Domain Extensions (Intel\u00ae TDX). https:\/\/cdrdv2.intel.com\/v1\/dl\/getContent\/690419."},{"key":"e_1_3_2_47_2","unstructured":"Intel. 2022. Product Brief: Intel\u00ae Software Guard Extensions. https:\/\/cdrdv2.intel.com\/v1\/dl\/getContent\/723693? explicitVersion=true."},{"key":"e_1_3_2_48_2","unstructured":"IPFS. 2023. IPFS powers the Distributed Web. https:\/\/ipfs.tech\/."},{"key":"e_1_3_2_49_2","unstructured":"iximeow. [n. d.]. iximeow\/yaxpeax-x86: x86 decoders for the yaxpeax project. https:\/\/github.com\/iximeow\/yaxpeaxx86."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Andrew Johnson Lucas Waye Scott Moore and Stephen Chong. 2015. Exploring and enforcing security guarantees via program dependence graphs. ACM SIGPLAN Notices 50 6 (2015) 291\u2013302. doi:10.1145\/2813885.2737957","DOI":"10.1145\/2813885.2737957"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","unstructured":"Evan Johnson David Thien Yousef Alhessi Shravan Narayan Fraser Brown Sorin Lerner Tyler McMullen Stefan Savage and Deian Stefan. 2021. \u0414\u043e\u0432\u0435\u0440\u044f\u0439 \u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0439: SFI safety for native-compiled Wasm. In 28th Network and Distributed Systems Security (NDSS) Symposium.","DOI":"10.14722\/ndss.2021.24078"},{"key":"e_1_3_2_52_2","unstructured":"David Kaplan Jeremy Powell and Tom Woller. 2020. AMD SEV-SNP: Strengthening VM Isolationwith Integrity Protection and More. Technical Report. Technical Report. Advanced Micro Devices Inc."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Florent Kirchner Nikolai Kosmatov Virgile Prevosto Julien Signoles and Boris Yakobowski. 2015. Frama-C: A software analysis perspective. Formal aspects of computing 27 (2015) 573\u2013609. doi:10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"Simon Koch Malte Wessels Benjamin Altpeter Madita Olvermann and Martin Johns. 2022. Keeping privacy labels honest. Proceedings on Privacy Enhancing Technologies 4 486-506 (2022) 2\u20132. doi:10.56553\/popets-2022-0119","DOI":"10.56553\/popets-2022-0119"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Joshua A Kroll Gordon Stewart and Andrew W Appel. 2014. Portable software fault isolation. In 2014 IEEE 27th Computer Security Foundations Symposium (CSF). IEEE 18\u201332. doi:10.1109\/CSF.2014.10","DOI":"10.1109\/CSF.2014.10"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","unstructured":"Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In International symposium on code generation and optimization 2004. CGO 2004. IEEE 75\u201386. doi:10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_57_2","unstructured":"Mengyuan Li Yinqian Zhang Huibo Wang Kang Li and Yueqiang Cheng. 2021. {CIPHERLEAKS}: Breaking Constanttime Cryptography on {AMD} {SEV} via the Ciphertext Side Channel. In 30th USENIX Security Symposium (USENIX Security). 717\u2013732."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Weijie Liu Wenhao Wang Hongbo Chen XiaoFeng Wang Yaosong Lu Kai Chen Xinyu Wang Qintao Shen Yi Chen and Haixu Tang. 2021. Practical and Efficient in-Enclave Verification of Privacy Compliance. In 2021 51st Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE 413\u2013425. doi:10.1109\/DSN48987.2021.00052","DOI":"10.1109\/DSN48987.2021.00052"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Muhammad Numair Mansur Maria Christakis Valentin W\u00fcstholz and Fuyuan Zhang. 2020. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In Proceedings of the 28th ACM joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE). 701\u2013712. doi:10.1145\/3368089.3409763","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_2_60_2","unstructured":"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)."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","unstructured":"Andrew C Myers. 1999. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 228\u2013241. doi:10.1145\/292540.292561","DOI":"10.1145\/292540.292561"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"George C Necula. 1997. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 106\u2013119. doi:10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/238721.238781"},{"key":"e_1_3_2_64_2","unstructured":"Automata Network. 2025. Automata DCAP Attestation. https:\/\/github.com\/automata-network\/automata-dcapattestation. Accessed: 2025-02-16."},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Jiwon Park Dominik Winterer Chengyu Zhang and Zhendong Su. 2021. Generative type-aware mutation for testing SMT solvers. Proceedings of the ACM on Programming Languages 5 OOPSLA (2021) 1\u201319. doi:10.1145\/3485529","DOI":"10.1145\/3485529"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"Fran\u00e7ois Pottier and Vincent Simonet. 2002. Information flow inference for ML. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 319\u2013330. doi:10.1145\/503272.503302","DOI":"10.1145\/503272.503302"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","unstructured":"Fred B Schneider. 2000. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC) 3 1 (2000) 30\u201350. doi:10.1145\/353323.353382","DOI":"10.1145\/353323.353382"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","unstructured":"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 Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems. 955\u2013970. doi:10.1145\/3373376.3378469","DOI":"10.1145\/3373376.3378469"},{"key":"e_1_3_2_70_2","doi-asserted-by":"crossref","unstructured":"Ming-Wei Shih Sangho Lee Taesoo Kim and Marcus Peinado. 2017. T-SGX: Eradicating Controlled-Channel Attacks Against Enclave Programs. In NDSS.","DOI":"10.14722\/ndss.2017.23193"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","unstructured":"Yan Shoshitaishvili Ruoyu Wang Christopher Salls Nick Stephens Mario Polino Andrew Dutcher John Grosen Siji Feng Christophe Hauser Christopher Kruegel et al. 2016. Sok:(state of) the art of war: Offensive techniques in binary analysis. In 37th IEEE Symposium on Security and Privacy (S&P). IEEE 138\u2013157. doi:10.1109\/SP.2016.17","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_2_72_2","unstructured":"SMT-COMP. 2023. Fparith Single Query \u2223 SMT-COMP. https:\/\/smt-comp.github.io\/2023\/results\/fparith-single-query."},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"e_1_3_2_74_2","unstructured":"Hao Sun and Zhendong Su. 2024. Validating the {eBPF} verifier via state embedding. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). 615\u2013628."},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","unstructured":"Gang Tan. 2017. Principles and Implementation Techniques of Software-Based Fault Isolation. Foundations and Trends\u00ae in Privacy and Security 1 3 (2017) 137\u2013198. doi:10.1561\/3300000013","DOI":"10.1561\/3300000013"},{"key":"e_1_3_2_76_2","unstructured":"The Capstone Engine Project. 2013\u20132025. Capstone Engine. http:\/\/www.capstone-engine.org. Accessed: July 22 2025."},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","unstructured":"Florian Tramer Fan Zhang Huang Lin Jean-Pierre Hubaux Ari Juels and Elaine Shi. 2017. Sealed-glass proofs: Using transparent enclaves to prove and sell knowledge. In 2nd IEEE European Symposium on Security and Privacy (EuroS&P). IEEE 19\u201334. doi:10.1109\/EuroSP.2017.28","DOI":"10.1109\/EuroSP.2017.28"},{"key":"e_1_3_2_78_2","unstructured":"trs-rs 2023. GitHub - joshrule\/term-rewriting-rs: a Rust implementation of first-order term rewriting systems (TRS). https:\/\/github.com\/joshrule\/term-rewriting-rs."},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","unstructured":"Jo Van Bulck Daniel Moghimi Michael Schwarz Moritz Lippi Marina Minkin Daniel Genkin Yuval Yarom Berk Sunar Daniel Gruss and Frank Piessens. 2020. LVI: Hijacking transient execution through microarchitectural load value injection. In 41st IEEE Symposium on Security and Privacy (S&P). 54\u201372. doi:10.1109\/SP40000.2020.00089","DOI":"10.1109\/SP40000.2020.00089"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00003"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","unstructured":"Robert Wahbe Steven Lucco Thomas E Anderson and Susan L Graham. 1993. Efficient software-based fault isolation. In Proceedings of the 14th ACM Symposium on Operating Systems Principles (SOSP). 203\u2013216. doi:10.1145\/168619.168635","DOI":"10.1145\/168619.168635"},{"key":"e_1_3_2_82_2","unstructured":"WALA. 2014. T. J. Watson Libraries for Analysis (WALA). https:\/\/github.com\/wala\/WALA."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134038"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","unstructured":"Yuting Wang Xiangzhe Xu Pierre Wilke and Zhong Shao. 2020. CompCertELF: verified separate compilation of C programs into ELF object files. Proceedings of the ACM on Programming Languages 4 OOPSLA (2020) 1\u201328. doi:10.1145\/3428265","DOI":"10.1145\/3428265"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"e_1_3_2_86_2","unstructured":"Gavin Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper 151 2014 (2014) 1\u201332."},{"key":"e_1_3_2_87_2","unstructured":"Yue Xiao Zhengyi Li Yue Qin Xiaolong Bai Jiale Guan Xiaojing Liao and Luyi Xing. 2023. Lalaine: Measuring and Characterizing {Non-Compliance} of Apple Privacy Labels. In 32nd USENIX Security Symposium (USENIX Security). 1091\u20131108."},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","unstructured":"Wenjie Xiong and Jakub Szefer. 2021. Survey of transient execution attacks and their mitigations. ACM Computing Surveys (CSUR) 54 3 (2021) 1\u201336. doi:10.1145\/3442479","DOI":"10.1145\/3442479"},{"key":"e_1_3_2_89_2","unstructured":"Bin Zeng Gang Tan and \u00dalfar Erlingsson. 2013. Strato: A Retargetable Framework for Low-Level Inlined-Reference Monitors. In 22nd USENIX Security Symposium (USENIX Security). 369\u2013382."},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","unstructured":"Bin Zeng Gang Tan and Greg Morrisett. 2011. Combining control-flow integrity and static analysis for efficient and validated data sandboxing. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS). 29\u201340. doi:10.1145\/2046707.2046713","DOI":"10.1145\/2046707.2046713"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813704"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763099","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:12:15Z","timestamp":1784196735000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":90,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763099"],"URL":"https:\/\/doi.org\/10.1145\/3763099","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}