{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T15:52:55Z","timestamp":1781020375481,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":87,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T00:00:00Z","timestamp":1760313600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["2303639,2443589,2039656"],"award-info":[{"award-number":["2303639,2443589,2039656"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3764860.3768333","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"108-117","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["From Rust Till Run: Extending Memory Safety From Rust to Cryptographic Assembly"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-1767","authenticated-orcid":false,"given":"Shai","family":"Caspin","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5405-9129","authenticated-orcid":false,"given":"Nikhil","family":"Pimpalkhare","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1479-8917","authenticated-orcid":false,"given":"Amit","family":"Levy","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49890-3_24"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3176258.3176330"},{"key":"e_1_3_2_1_4_1","unstructured":"Amazon Web Services. 2024. AWS LibCrypto."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428204"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP).","author":"Athalye Anish","unstructured":"Anish Athalye, Henry Corrigan-Gibbs, M Frans Kaashoek, Joseph Tassarotti, and Nickolai Zeldovich. [n. d.]. Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. In Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP)."},{"key":"e_1_3_2_1_10_1","volume-title":"Principles of Security and Trust: 7th International Conference, POST","author":"de Amorim Arthur Azevedo","year":"2018","unstructured":"Arthur Azevedo de Amorim, C\u0103t\u0103lin Hri\u0163cu, and Benjamin C Pierce. 2018. The meaning of memory safety. In Principles of Security and Trust: 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 7. Springer, 79--105."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_1_12_1","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Bang Inyoung","year":"2023","unstructured":"Inyoung Bang, Martin Kayondo, Hyungon Moon, and Yunheung Paek. 2023. TRUST: A Compilation Framework for In-process Isolation to Protect Safe Rust against Untrusted Code. In 32nd USENIX Security Symposium (USENIX Security 23). Baltimore, MD: USENIX Association."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_1_14_1","volume-title":"9th USENIX Workshop on Offensive Technologies (WOOT 15)","author":"Bazhaniuk Oleksandr","year":"2015","unstructured":"Oleksandr Bazhaniuk, John Loucaides, Lee Rosenbaum, Mark R Tuttle, and Vincent Zimmer. 2015. Symbolic Execution for {BIOS} Security. In 9th USENIX Workshop on Offensive Technologies (WOOT 15)."},{"key":"e_1_3_2_1_15_1","volume-title":"O'Hearn","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. 2005. Symbolic Execution with Separation Logic. In Programming Languages and Systems, Kwangkeun Yi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 52--68."},{"key":"e_1_3_2_1_16_1","volume-title":"24th USENIX Security Symposium (USENIX Security 15)","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Q Ye Katherine, and Andrew W Appel. 2015. Verified correctness and security of {OpenSSL} {HMAC}. In 24th USENIX Security Symposium (USENIX Security 15). 207--221."},{"key":"e_1_3_2_1_17_1","volume-title":"Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages.","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R Lorch, et al. 2017. Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3634737.3657012"},{"key":"e_1_3_2_1_20_1","volume-title":"Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson.","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K Rustan M Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying {High-Performance} Cryptographic Assembly Code. In 26th USENIX security symposium (USENIX security 17). 917--934."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_31"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2019.2937214"},{"key":"e_1_3_2_1_23_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Brown Fraser","year":"2020","unstructured":"Fraser Brown, Deian Stefan, and Dawson Engler. 2020. Sys: A {Static\/Symbolic} Tool for Finding Good Bugs in Good (Browser) Code. In 29th USENIX Security Symposium (USENIX Security 20). 199--216."},{"key":"e_1_3_2_1_24_1","first-page":"209","article-title":"Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs.. In OSDI, Vol. 8. 209--224.","journal-title":"OSDI"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_3_2_1_26_1","volume-title":"Fact: A flexible, constant-time programming language. In 2017 IEEE Cybersecurity Development (SecDev)","author":"Cauligi Sunjay","year":"2017","unstructured":"Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, and Deian Stefan. 2017. Fact: A flexible, constant-time programming language. In 2017 IEEE Cybersecurity Development (SecDev). IEEE, 69--76."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Can Cebeci Yonghao Zou Diyu Zhou George Candea and Cl\u00e9ment Pit-Claudel. 2024. Practical Verification of System-Software Components Written in Standard C. (2024).","DOI":"10.1145\/3694715.3695980"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"e_1_3_2_1_29_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Costan Victor","year":"2016","unstructured":"Victor Costan, Ilia Lebedev, and Srinivas Devadas. 2016. Sanctum: Minimal hardware extensions for strong software isolation. In 25th USENIX Security Symposium (USENIX Security 16). 857--874."},{"key":"e_1_3_2_1_30_1","volume-title":"1999 ACM SIGPLAN Workshop on Compiler Support for System Software Atlanta, GA, USA. 25--35","author":"Crary K","year":"1999","unstructured":"K Crary, Neal Glew, Dan Grossman, Richard Samuels, F Smith, D Walker, S Weirich, and S Zdancewic. 1999. 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_1_31_1","unstructured":"Will Crichton. 2018. Memory Safety in Rust. https:\/\/stanford-cs242.github.io\/f18\/lectures\/05-1-rust-memory-safety.html"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639136"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563037"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2016.43"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_5"},{"key":"e_1_3_2_1_37_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Distefano Dino","unstructured":"Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. 2006. A Local Shape Analysis Based on Separation Logic. In Tools and Algorithms for the Construction and Analysis of Systems, Holger Hermanns and Jens Palsberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 287--302."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421477"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314590"},{"key":"e_1_3_2_1_42_1","unstructured":"Google. 2024. BoringSSL."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674640"},{"key":"e_1_3_2_1_45_1","unstructured":"Ralf Jung. 2020. Understanding and evolving the Rust programming language. (2020)."},{"key":"e_1_3_2_1_46_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages 2, POPL (2017), 1--34."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492321.3519582"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3144555.3144562"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_1_53_1","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Li Xupeng","year":"2022","unstructured":"Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and verification of the arm confidential compute architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). 465--484."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17143-7_33"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_1_57_1","volume-title":"A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries. arXiv preprint arXiv:2404.11671","author":"McCormack Ian","year":"2024","unstructured":"Ian McCormack, Joshua Sunshine, and Jonathan Aldrich. 2024. A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries. arXiv preprint arXiv:2404.11671 (2024)."},{"key":"e_1_3_2_1_58_1","unstructured":"Denis Merigoux Franziskus Kiefer and Karthikeyan Bhargavan. 2021. Hacspec: succinct executable verifiable specifications for high-assurance cryptography embedded in Rust. Ph. D. Dissertation. Inria."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA358572"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_2_1_61_1","volume-title":"SHAKE, EdDSA, and other NIST-approved algorithms","author":"Mouha Nicky","unstructured":"Nicky Mouha and Christopher Celi. 2023. A vulnerability in implementations of SHA-3, SHAKE, EdDSA, and other NIST-approved algorithms. Springer, 3--28."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_3_2_1_63_1","unstructured":"OpenSSL Foundation. 2024. OpenSSL."},{"key":"e_1_3_2_1_64_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with {SymCC}: Don't interpret, compile!. In 29th USENIX Security Symposium (USENIX Security 20). 181--198."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589250.3596143"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485832.3485903"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_2_1_69_1","volume-title":"19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25)","author":"Schuermann Leon","year":"2025","unstructured":"Leon Schuermann, Jack Toubes, Tyler Potyondy, Pat Pannuto, Mae Milano, and Amit Levy. 2025. Building Bridges: Safe Interactions with Foreign Languages through Omniglot. In 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25), Boston, MA: USENIX Association."},{"key":"e_1_3_2_1_70_1","volume-title":"Proceedings of the ACM on Programming Languages 4, POPL","author":"Song Youngju","year":"2019","unstructured":"Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur. 2019. CompCertM: CompCert with C-assembly linking and lightweight modular verification. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1--31."},{"key":"e_1_3_2_1_71_1","volume-title":"with contributions from the Rust Community","author":"Klabnik Steve","year":"2024","unstructured":"Steve Klabnik and Carol Nichols, with contributions from the Rust Community. 2024. The Rust Programming Language - Understanding Ownership. https:\/\/doc.rust-lang.org\/book\/ch04-00-understanding-ownership.html"},{"key":"e_1_3_2_1_72_1","unstructured":"The Rav1d Maintainers. 2024. Rav1d AV1 Decoder."},{"key":"e_1_3_2_1_73_1","unstructured":"The Rust Contributors. 2023. The Rust Reference - Unsafety. https:\/\/doc.rust-lang.org\/reference\/unsafety.html"},{"key":"e_1_3_2_1_74_1","unstructured":"The Rust Contributors. 2023. The Rustonomicon. https:\/\/doc.rust-lang.org\/nomicon\/"},{"key":"e_1_3_2_1_75_1","unstructured":"The Rust Contributors. 2023. The Rustonomicon - How Safe and Unsafe Interact. https:\/\/doc.rust-lang.org\/nomicon\/safe-unsafe-meaning.html"},{"key":"e_1_3_2_1_76_1","unstructured":"The Rust Contributors. 2024. The Rust Reference - Inline Assembly. https:\/\/doc.rust-lang.org\/reference\/inline-assembly.html"},{"key":"e_1_3_2_1_77_1","unstructured":"The RustCrypto Organization. 2024. RustCrypto. https:\/\/github.com\/RustCrypto"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507657"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640408"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629175.1629203"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016848.1016875"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016848.1016875"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.80"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3628160"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563345"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3764860.3768333","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768333","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:19:57Z","timestamp":1763054397000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":87,"alternative-id":["10.1145\/3764860.3768333","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768333","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}