{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:26:52Z","timestamp":1766442412500,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":66,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T00:00:00Z","timestamp":1763769600000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-22-1-0511"],"award-info":[{"award-number":["FA9550-22-1-0511"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["3134.014"],"award-info":[{"award-number":["3134.014"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765116","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:37:25Z","timestamp":1763854645000},"page":"141-155","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Securing Cryptographic Software via Typed Assembly Language"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-5638-5164","authenticated-orcid":false,"given":"Shixin","family":"Song","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0514-923X","authenticated-orcid":false,"given":"Tingzhen","family":"Dong","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0770-0344","authenticated-orcid":false,"given":"Kosi","family":"Nwabueze","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2615-637X","authenticated-orcid":false,"given":"Julian","family":"Zanders","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"Google, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6206-9674","authenticated-orcid":false,"given":"Mengjia","family":"Yan","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"volume-title":"Cryptographers' Track at the RSA Conference","author":"Acii\u00e7mez Onur","key":"e_1_3_2_2_1_1","unstructured":"Onur Acii\u00e7mez, \u00c7etin Kaya Ko\u00e7, and Jean-Pierre Seifert. 2007. Predicting secret keys via branch prediction. In Cryptographers' Track at the RSA Conference. Springer, 225-242."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00066"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.44"},{"key":"e_1_3_2_2_6_1","first-page":"933","volume-title":"Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","volume":"2","author":"Olmos Santiago Arranz","year":"2025","unstructured":"Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Gregoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, and Zhiyuan Zhang. 2025. Protecting cryptographic code against Spectre-RSB:(and, in fact, all known Spectre variants). In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2. 933-948."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2019.00020"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363194"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024716.2024718"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303952"},{"key":"e_1_3_2_2_12_1","unstructured":"Chandler Carruth. n.d.. Speculative load hardening. https:\/\/llvm.org\/docs\/SpeculativeLoadHardening.html"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314605"},{"volume-title":"Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. 2053-2067","author":"Choudhary Rutvik","key":"e_1_3_2_2_16_1","unstructured":"Rutvik Choudhary, Alan Wang, Zirui Neil Zhao, Adam Morrison, and Christopher W. Fletcher. 2023. Declassiflow: A static analysis for modeling non-speculative knowledge to relax speculative execution security measures. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. 2053-2067."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480068"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.19"},{"key":"e_1_3_2_2_19_1","first-page":"7161","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Daniel Lesly-Ann","year":"2023","unstructured":"Lesly-Ann Daniel, Marton Bognar, Job Noorman, S\u00e9bastien Bardin, Tamara Rezk, and Frank Piessens. 2023. ProSpeCT: Provably secure speculation for the Constant-Time policy. In 32nd USENIX Security Symposium (USENIX Security 23). 7161-7178."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978374"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296957.3173204"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3316781.3317914"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292563"},{"key":"e_1_3_2_2_25_1","unstructured":"Google. n.d.. BoringSSL. https:\/\/boringssl.googlesource.com\/boringssl"},{"key":"e_1_3_2_2_26_1","first-page":"955","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Gras Ben","year":"2018","unstructured":"Ben Gras, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2018. Translation leak-aside buffer: Defeating cache side-channel protections with TLB attacks. In 27th USENIX Security Symposium (USENIX Security 18). 955-972."},{"key":"e_1_3_2_2_27_1","volume-title":"International Workshop on Types in Compilation. Springer, 117-145","author":"Grossman Dan","year":"2000","unstructured":"Dan Grossman and Greg Morrisett. 2000. Scalable certification for typed assembly language. In International Workshop on Types in Compilation. Springer, 117-145."},{"key":"e_1_3_2_2_28_1","volume-title":"International Conference on Information Security and Cryptology. Springer, 176-192","author":"Gro\u00dfsch\u00e4dl Johann","year":"2009","unstructured":"Johann Gro\u00dfsch\u00e4dl, Elisabeth Oswald, Dan Page, and Michael Tunstall. 2009. Side-channel analysis of cryptographic software via early-terminating multiplications. In International Conference on Information Security and Cryptology. Springer, 176-192."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978356"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_2_32_1","unstructured":"Jann Horn. 2018. Speculative execution variant 4: Speculative store bypass. https:\/\/project-zero.issues.chromium.org\/issues\/42450580. (2018)."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560672"},{"key":"e_1_3_2_2_34_1","volume-title":"Speculative buffer overflows: Attacks and defenses. arXiv preprint arXiv:1807.03757","author":"Kiriansky Vladimir","year":"2018","unstructured":"Vladimir Kiriansky and Carl Waldspurger. 2018. Speculative buffer overflows: Attacks and defenses. arXiv preprint arXiv:1807.03757 (2018)."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_2_36_1","volume-title":"12th USENIX Workshop on Offensive Technologies (WOOT 18)","author":"Koruyeh Esmaeil Mohammadian","year":"2018","unstructured":"Esmaeil Mohammadian Koruyeh, Khaled N Khasawneh, Chengyu Song, and Nael Abu-Ghazaleh. 2018. Spectre returns! Speculation attacks using the return stack buffer. In 12th USENIX Workshop on Offensive Technologies (WOOT 18)."},{"key":"e_1_3_2_2_37_1","first-page":"1397","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Loughlin Kevin","year":"2021","unstructured":"Kevin Loughlin, Ian Neal, Jiacheng Ma, Elisa Tsai, Ofir Weisse, Satish Narayanasamy, and Baris Kasikci. 2021. DOLMA: Securing speculation with the principle of transient non-observability. In 30th USENIX Security Symposium (USENIX Security 21). 1397-1414."},{"key":"e_1_3_2_2_38_1","unstructured":"Jason Lowe-Power Abdul Mutaal Ahmad Ayaz Akram Mohammad Alian Rico Amslinger Matteo Andreozzi Adri\u00e0 Armejach Nils Asmussen Srikant Bharadwaj Gabe Black Gedare Bloom Bobby R. Bruce Daniel Rodrigues Carvalho Jer\u00f3nimo Castrill\u00f3n Lizhong Chen Nicolas Derumigny Stephan Diestelhorst Wendy Elsasser Marjan Fariborz Amin Farmahini Farahani Pouya Fotouhi Ryan Gambord Jayneel Gandhi Dibakar Gope Thomas Grass Bagus Hanindhito Andreas Hansson Swapnil Haria Austin Harris Timothy Hayes Adrian Herrera Matthew Horsnell Syed Ali Raza Jafri Radhika Jagtap Hanhwi Jang Reiley Jeyapaul Timothy M. Jones Matthias Jung Subash Kannoth Hamidreza Khaleghzadeh Yuetsu Kodama Tushar Krishna Tommaso Marinelli Christian Menard Andrea Mondelli Tiago M\u00fcck Omar Naji Krishnendra Nathella Hoa Nguyen Nikos Nikoleris Lena E. Olson Marc S. Orr Binh Pham Pablo Prieto Trivikram Reddy Alec Roelke Mahyar Samani Andreas Sandberg Javier Setoain Boris Shingarov Matthew D. Sinclair Tuan Ta Rahul Thakur Giacomo Travaglini Michael Upton Nilay Vaish Ilias Vougioukas Zhengrong Wang Norbert Wehn Christian Weis David A. Wood Hongil Yoon and \u00c9der F. Zulian. 2020. The gem5 simulator: Version 20.0. CoRR Vol. abs\/2007.03152 (2020). arXiv:2007.03152 https:\/\/arxiv.org\/abs\/2007.03152"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-018-0611-9"},{"key":"e_1_3_2_2_41_1","volume-title":"1999 ACM SIGPLAN Workshop on Compiler Support for System Software","author":"Morrisett Greg","year":"1999","unstructured":"Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. 1999 a. TALx86: A realistic typed assembly language. In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software (Atlanta, GA, USA). 25-35."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA358572"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00048"},{"key":"e_1_3_2_2_45_1","first-page":"1433","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Narayan Shravan","year":"2021","unstructured":"Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, et al., 2021. Swivel: Hardening WebAssembly against Spectre. In 30th USENIX Security Symposium (USENIX Security 21). 1433-1450."},{"key":"e_1_3_2_2_46_1","first-page":"1","volume-title":"USA","author":"Osvik Dag Arne","year":"2006","unstructured":"Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: The case of AES. In Topics in Cryptology-CT-RSA 2006: The Cryptographers' Track at the RSA Conference 2006, San Jose, CA, USA, February 13-17, 2005. Proceedings. Springer, 1-20."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_2_48_1","first-page":"565","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Pessl Peter","year":"2016","unstructured":"Peter Pessl, Daniel Gruss, Cl\u00e9mentine Maurice, Michael Schwarz, and Stefan Mangard. 2016. DRAMA: Exploiting DRAM addressing for Cross-CPU attacks. In 25th USENIX Security Symposium (USENIX Security 16). 565-581."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833774"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2020.24271"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29959-0_14"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243736"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179355"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179418"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"crossref","unstructured":"Shixin Song Tingzhen Dong Kosi Nwabueze Julian Zanders Andres Erbsen Adam Chlipala and Mengjia Yan. 2025. Securing cryptographic software via typed assembly language (extended version). arXiv:2509.08727 [cs.CR] https:\/\/arxiv.org\/abs\/2509.08727","DOI":"10.1145\/3719027.3765116"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434330"},{"volume-title":"Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 2421-2434","author":"Wang Wenhao","key":"e_1_3_2_2_57_1","unstructured":"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 Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 2421-2434."},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358306"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.45"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00042"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00004"},{"key":"e_1_3_2_2_62_1","first-page":"719","volume-title":"23rd USENIX Security Symposium (USENIX Security 14)","author":"Yarom Yuval","year":"2014","unstructured":"Yuval Yarom and Katrina Falkner. 2014. FLUSH RELOAD: A high resolution, low noise, L3 cache side-channel attack. In 23rd USENIX Security Symposium (USENIX Security 14). 719-732."},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-017-0152-y"},{"volume-title":"2020 ACM\/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). IEEE, 707-720","author":"Yu Jiyong","key":"e_1_3_2_2_64_1","unstructured":"Jiyong Yu, Namrata Mantri, Josep Torrellas, Adam Morrison, and Christopher W. Fletcher. 2020. Speculative data-oblivious execution: Mobilizing safe prediction for safe and efficient speculative execution. In 2020 ACM\/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). IEEE, 707-720."},{"volume-title":"Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Microarchitecture. 954-968","author":"Yu Jiyong","key":"e_1_3_2_2_65_1","unstructured":"Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, and Christopher W. Fletcher. 2019. Speculative taint tracking (STT): A comprehensive protection for speculatively accessed data. In Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Microarchitecture. 954-968."},{"key":"e_1_3_2_2_66_1","first-page":"7125","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Zhang Zhiyuan","year":"2023","unstructured":"Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, and Yuval Yarom. 2023. Ultimate SLH: Taking speculative load hardening to the next level. In 32nd USENIX Security Symposium (USENIX Security 23). 7125-7142."}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Taipei Taiwan","acronym":"CCS '25"},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765116","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:22:08Z","timestamp":1766442128000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":66,"alternative-id":["10.1145\/3719027.3765116","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765116","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}