{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:24:27Z","timestamp":1760142267848,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test\u00a0Rust programs. Alas, the Rust ecosystem remains relatively young, meaning\u00a0that every one of these tools has had to re-implement difficult, time-consuming machinery to interface with the Rust compiler and its cargo build system,\u00a0to hook into the Rust compiler\u2019s internal representation, and to expose\u00a0an abstract syntax tree (AST) that is suitable for analysis rather than optimized for efficiency.<\/jats:p>\n          <jats:p>We address this missing building block of the Rust ecosystem, and propose Charon, an analysis framework for Rust. Charon acts as a swiss-army knife\u00a0for analyzing Rust programs, and deals with all of the tedium above, providing clients with an AST that can serve as the foundation of\u00a0many analyses. We demonstrate the usefulness of Charon through a series of\u00a0case studies, ranging from a Rust verification framework (Aeneas), a compiler from Rust to C (Eurydice), and a novel taint-checker for cryptographic code. To drive the point home, we also re-implement a popular existing analysis (Rudra), and show that it can be replicated\u00a0by leveraging the Charon framework.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_18","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:33:01Z","timestamp":1753155181000},"page":"377-391","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Charon: An Analysis Framework for\u00a0Rust"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3297-9156","authenticated-orcid":false,"given":"Son","family":"Ho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5244-893X","authenticated-orcid":false,"given":"Guillaume","family":"Boisseau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Franceschino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoann","family":"Prak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2642-543X","authenticated-orcid":false,"given":"Aymeric","family":"Fromherz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7347-3050","authenticated-orcid":false,"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"18_CR1","unstructured":"Github tracking issue for bugs fixed by the MIR borrow checker or NLL. https:\/\/github.com\/rust-lang\/rust\/issues\/47366"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification. In: Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) (2019)","DOI":"10.1145\/3360573"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Ayoun, S.\u00c9., Denis, X., Maksimovi\u0107, P., Gardner, P.: A hybrid approach to semi-automated rust verification. arXiv preprint arXiv:2403.15122 (2024)","DOI":"10.1145\/3729289"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Bae, Y., Kim, Y., Askar, A., Lim, J., Kim, T.: Rudra: finding memory safety bugs in rust at the ecosystem scale. In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, pp. 84\u201399 (2021)","DOI":"10.1145\/3477132.3483570"},{"key":"18_CR5","unstructured":"Bernstein, D.J., et al.: KyberSlash: exploiting secret-dependent division timings in Kyber implementations. Cryptology ePrint Archive, Paper 2024\/1049 (2024). https:\/\/eprint.iacr.org\/2024\/1049"},{"key":"18_CR6","unstructured":"Bhargavan, K., Franceschino, L., Hansen, L.L., Kiefer, F., Schneider-Bensch, J., Spitters, B.: Hax - enabling high assurance cryptographic software. RustVerify (2024). https:\/\/github.com\/hacspec\/hacspec.github.io\/blob\/master\/RustVerify24.pdf"},{"key":"18_CR7","unstructured":"Bhargavan, K., Kiefer, F., Tamvada, G.: Verified ML-KEM (Kyber) in rust. https:\/\/cryspen.com\/post\/ml-kem-implementation\/"},{"key":"18_CR8","unstructured":"Charon team: Charon github repository (2025). https:\/\/github.com\/AeneasVerif\/charon"},{"key":"18_CR9","unstructured":"Charon team: Charon zenodo artifact (2025). https:\/\/zenodo.org\/records\/15314373"},{"key":"18_CR10","unstructured":"Cook, K.: [GIT PULL] Rust introduction for v6.1-rc1. https:\/\/lore.kernel.org\/lkml\/202210010816.1317F2C@keescook\/"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Denis, X., Jourdan, J.H., March\u00e9, C.: CREUSOT: a foundry for the deductive verification of rust programs. In: Riesco, A., Zhang, M. (eds.) International Conference on Formal Engineering Methods, pp. 90\u2013105. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"G\u00e4her, L., Sammler, M., Jung, R., Krebbers, R., Dreyer, D.: RefinedRust: a type system for high-assurance verification of Rust programs. Proc. ACM Programm. Lang. 8(PLDI), 1115\u20131139 (2024)","DOI":"10.1145\/3656422"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Grech, N., Georgiou, K., Pallister, J., Kerrison, S., Morse, J., Eder, K.: Static analysis of energy consumption for LLVM IR programs. In: Proceedings of the 18th International Workshop on Software and Compilers for Embedded Systems, pp. 12\u201321 (2015)","DOI":"10.1145\/2764967.2764974"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Gritti, F., et al.: HEAPSTER: analyzing the security of dynamic allocators for monolithic firmware images. In: Proceedings of the IEEE Symposium on Security & Privacy (S &P) (2022)","DOI":"10.1109\/SP46214.2022.9833610"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Navas, J.A.: Abstract interpretation of LLVM with a region-based memory model. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) International Workshop on Numerical Software Verification, pp. 122\u2013144. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_8","DOI":"10.1007\/978-3-030-95561-8_8"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Ho, S., Fromherz, A., Protzenko, J.: Sound borrow-checking for rust via symbolic semantics. Proc. ACM Programm. Lang. 8(ICFP), 426\u2013454 (2024)","DOI":"10.1145\/3674640"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Ho, S., Protzenko, J.: Aeneas: rust verification by functional translation. Proc. ACM Programm. Lang. 6(ICFP), 711\u2013741 (2022). https:\/\/doi.org\/10.1145\/3547647","DOI":"10.1145\/3547647"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (2018)","DOI":"10.1145\/3158154"},{"key":"18_CR19","unstructured":"Kani contributors: the Kani rust verified. https:\/\/github.com\/model-checking\/kani"},{"key":"18_CR20","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization (CGO) (2004)"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Lattuada, A., et al.: Verus: verifying rust programs using linear ghost types. In: Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) (2023). https:\/\/doi.org\/10.1145\/3586037","DOI":"10.1145\/3586037"},{"key":"18_CR22","unstructured":"libcrux contributors: libcrux - the formally verified crypto library. https:\/\/github.com\/cryspen\/libcrux\/"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Marx, S., Erdweg, S.: Abstract interpretation of java bytecode in sturdy. In: Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs pp. 17\u201322 (2024)","DOI":"10.1145\/3678721.3686226"},{"key":"18_CR24","unstructured":"Matsakis, Niko: Introducing MIR. https:\/\/blog.rust-lang.org\/2016\/04\/19\/MIR.html"},{"key":"18_CR25","unstructured":"Merigoux, D., Kiefer, F., Bhargavan, K.: HACSPEC: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust. Technical report, Inria (2021). https:\/\/inria.hal.science\/hal-03176482"},{"key":"18_CR26","unstructured":"Miri Contributors: Miri, an undefined behavior detection tool for rust. https:\/\/github.com\/rust-lang\/miri"},{"key":"18_CR27","unstructured":"National security agency: software memory safety (2022). https:\/\/media.defense.gov\/2022\/Nov\/10\/2003112742\/-1\/-1\/0\/CSI_SOFTWARE_MEMORY_SAFETY.PDF"},{"key":"18_CR28","unstructured":"NIST: Module-lattice-based key-encapsulation mechanism standard (2024). https:\/\/csrc.nist.gov\/pubs\/fips\/203\/final"},{"key":"18_CR29","unstructured":"Nitin, V., Mulhern, A., Arora, S., Ray, B.: Yuga: automatically detecting lifetime annotation bugs in the rust language (2023). https:\/\/arxiv.org\/abs\/2310.08507"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Nitin, V., Mulhern, A., Arora, S., Ray, B.: Yuga: Automatically detecting lifetime annotation bugs in the rust language. IEEE Trans. Softw. Eng. 50, 2602\u20132613 (2024)","DOI":"10.1109\/TSE.2024.3447671"},{"issue":"8","key":"18_CR31","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1145\/355609.362337","volume":"16","author":"WW Peterson","year":"1973","unstructured":"Peterson, W.W., Kasami, T., Tokura, N.: On the capabilities of while, repeat, and exit statements. Commun. ACM 16(8), 503\u2013512 (1973)","journal-title":"Commun. ACM"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Polubelova, M., et al.: HACLxN: verified generic SIMD crypto (for all your favourite platforms). In: Proceedings of the ACM Conference on Computer and Communications Security (CCS) (2020)","DOI":"10.1145\/3372297.3423352"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Ramsey, N.: Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl). Proc. ACM Programm. Lang. 6(ICFP), 1\u201322 (2022)","DOI":"10.1145\/3547621"},{"key":"18_CR34","unstructured":"Rust compiler team: Implementors of MirPass (2024). https:\/\/doc.rust-lang.org\/nightly\/nightly-rustc\/rustc_mir_transform\/pass_manager\/trait.MirPass.html#implementors"},{"key":"18_CR35","unstructured":"Rust Crypto maintainers: rust crypto - cryptographic algorithms written in pure rust. https:\/\/github.com\/RustCrypto"},{"key":"18_CR36","unstructured":"Stable MIR contributors: stable MIR: define a compiler intermediate representation usable by external tools. https:\/\/github.com\/rust-lang\/project-stable-mir"},{"key":"18_CR37","unstructured":"StackOverflow: 2023 developer survey (2023). https:\/\/survey.stackoverflow.co\/2023\/#section-admired-and-desired-programming-scripting-and-markup-languages"},{"key":"18_CR38","unstructured":"Stateright Contributors: stateright, a model-checker for implementing distributed systems. https:\/\/github.com\/stateright\/stateright"},{"key":"18_CR39","unstructured":"The HACL* Team: a preliminary version of HACL* extracted to *safe* Rust. https:\/\/github.com\/hacl-star\/hacl-star\/pull\/918"},{"key":"18_CR40","unstructured":"The RaRust development team: Rarust (2025). https:\/\/github.com\/Mepy\/rarust-oopsla25"},{"key":"18_CR41","unstructured":"The register: in rust we trust: Microsoft azure CTO shuns C and C++ (2022). https:\/\/www.theregister.com\/2022\/09\/20\/rust_microsoft_c\/"},{"key":"18_CR42","unstructured":"The Register: Microsoft is busy rewriting core Windows code in memory-safe Rust (2023). https:\/\/www.theregister.com\/2023\/04\/27\/microsoft_windows_rust\/"},{"key":"18_CR43","unstructured":"The white house: back to the building blocks: a path toward secure and measurable software. https:\/\/www.whitehouse.gov\/wp-content\/uploads\/2024\/02\/Final-ONCD-Technical-Report.pdf"},{"key":"18_CR44","unstructured":"Verdi, S.: Why rust is the most admired language among developers (2023). https:\/\/github.blog\/2023-08-30-why-rust-is-the-most-admired-language-among-developers\/"},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"Zakai, A.: Emscripten: an LLVM-to-Javascript compiler. In: Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) (2011)","DOI":"10.1145\/2048147.2048224"},{"key":"18_CR46","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 427\u2013440 (2012)","DOI":"10.1145\/2103656.2103709"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:54:41Z","timestamp":1760086481000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}