{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:36:13Z","timestamp":1781238973641,"version":"3.54.1"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031866944","type":"print"},{"value":"9783031866951","type":"electronic"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-86695-1_7","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:44Z","timestamp":1746151604000},"page":"96-119","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["hax: Verifying Security-Critical Rust Software Using Multiple Provers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3152-8997","authenticated-orcid":false,"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maxime","family":"Buyse","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucas","family":"Franceschino","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3593","authenticated-orcid":false,"given":"Lasse Letager","family":"Hansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Franziskus","family":"Kiefer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonas","family":"Schneider-Bensch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0973","authenticated-orcid":false,"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"key":"7_CR1","unstructured":"Back to the building blocks: a path towards secure and measurable software (2024). https:\/\/www.whitehouse.gov\/wp-content\/uploads\/2024\/02\/Final-ONCD-Technical-Report.pdf"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Module-Lattice-based key-encapsulation mechanism standard (2024). https:\/\/doi.org\/10.6028\/NIST.FIPS.203","DOI":"10.6028\/NIST.FIPS.203"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: CCS, pp. 1807\u20131823. ACM (2017)","DOI":"10.1145\/3133956.3134078"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Annenkov, D., Nielsen, J.B., Spitters, B.: Concert: a smart contract certification framework in COQ. In: CPP, pp. 215\u2013228. ACM (2020)","DOI":"10.1145\/3372885.3373829"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Verified software toolchain. In: Goodloe, A., Person, S. (eds.) NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. LNCS, vol.\u00a07226, p.\u00a02. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_2","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), vol.\u00a03, pp. 147:1\u2013147:30 (2019)","DOI":"10.1145\/3360573"},{"issue":"2","key":"7_CR7","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/3665453.3665461","volume":"11","author":"D Baelde","year":"2024","unstructured":"Baelde, D., Delaune, S., Jacomme, C., Koutsos, A., Lallemand, J.: The squirrel prover and its logic. ACM SIGLOG News 11(2), 62\u201383 (2024)","journal-title":"ACM SIGLOG News"},{"key":"7_CR8","unstructured":"Barbosa, M., Bhargavan, K., Kiefer, F., Schwabe, P., Strub, P., Westerbaan, B.: Formal specifications for certifiable cryptography (2024)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Barbosa, M., et al.: Sok: computer-aided cryptography. In: SP, pp. 777\u2013795. IEEE (2021)","DOI":"10.1109\/SP40001.2021.00008"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.: Easycrypt: a tutorial. In: FOSAD. LNCS, vol.\u00a08604, pp. 146\u2013166. Springer (2013)","DOI":"10.1007\/978-3-319-10082-1_6"},{"issue":"3","key":"7_CR11","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MSEC.2022.3154689","volume":"20","author":"DA Basin","year":"2022","unstructured":"Basin, D.A., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real-world, cryptographic protocols. IEEE Secur. Priv. 20(3), 24\u201332 (2022)","journal-title":"IEEE Secur. Priv."},{"key":"7_CR12","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":"7_CR13","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pp. 483\u2013502. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/SP.2017.26","DOI":"10.1109\/SP.2017.26"},{"key":"7_CR14","unstructured":"Blanchet, B.: Cryptoverif: computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl Seminar Formal Protocol Verification Applied, vol.\u00a0117, p.\u00a0156 (2007)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic verification of security protocols in the symbolic model: the verifier proverif. In: FOSAD. LNCS, vol.\u00a08604, pp. 54\u201387. Springer (2013)","DOI":"10.1007\/978-3-319-10082-1_3"},{"key":"7_CR16","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: Kirda, E., Ristenpart, T. (eds.) 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017, pp. 917\u2013934. USENIX Association (2017). https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-030-03332-3_9","volume-title":"Advances in Cryptology \u2013 ASIACRYPT 2018","author":"C Brzuska","year":"2018","unstructured":"Brzuska, C., Delignat-Lavaud, A., Fournet, C., Kohbrok, K., Kohlweiss, M.: State separation for code-based game-playing proofs. In: Peyrin, T., Galbraith, S. (eds.) ASIACRYPT 2018. LNCS, vol. 11274, pp. 222\u2013249. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03332-3_9"},{"key":"7_CR18","unstructured":"Cheval, V., Jacomme, C., Kremer, S., K\u00fcnnemann, R.: SAPIC+: protocol verifiers of the world, unite! In: USENIX Security Symposium, pp. 3935\u20133952. USENIX Association (2022)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. In: ICFP, pp. 268\u2013279. ACM (2000)","DOI":"10.1145\/357766.351266"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Delignat-Lavaud, A., et al.: Implementing and proving the TLS 1.3 record layer. In: 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pp. 463\u2013482. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/SP.2017.58","DOI":"10.1109\/SP.2017.58"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Denis, X., Jourdan, J.H., March\u00e9, C.: Creusot: a foundry for the deductive verification of rust programs. In: International Conference on Formal Engineering Methods, pp. 90\u2013105. Springer (2022)","DOI":"10.1007\/978-3-031-17244-1_6"},{"issue":"2","key":"7_CR22","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013207 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: IEEE Symposium on Security and Privacy, pp. 1202\u20131219. IEEE (2019)","DOI":"10.1109\/SP.2019.00005"},{"key":"7_CR24","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 Program. Lang. 8(PLDI), 1115\u20131139 (2024)","DOI":"10.1145\/3656422"},{"key":"7_CR25","unstructured":"Hansen, L.L., Spitters, B.: Specifying smart contract with Hax and concert. In: CoqPL (2024). https:\/\/popl24.sigplan.org\/details\/CoqPL-2024-papers\/9\/Specifying-Smart-Contract-with-Hax-and-ConCert"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Haselwarter, P.G., Hvass, B.S., Hansen, L.L., Winterhalter, T., Hritcu, C., Spitters, B.: The last yard: foundational end-to-end verification of high-speed cryptography. In: CPP, pp. 30\u201344. ACM (2024)","DOI":"10.1145\/3636501.3636961"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Haselwarter, P.G., et al.: SSProve: a foundational framework for modular cryptographic proofs in COQ. ACM Trans. Program. Lang. Syst. 45(3), 15:1\u201315:61 (2023)","DOI":"10.1145\/3594735"},{"key":"7_CR28","unstructured":"Ho, S., Boisseau, G., Franceschino, L., Prak, Y., Fromherz, A., Protzenko, J.: Charon: an analysis framework for rust. arXiv preprint arXiv:2410.18042 (2024)"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Ho, S., Protzenko, J.: Aeneas: rust verification by functional translation. PACM PL 6(ICFP) (2022). https:\/\/doi.org\/10.1145\/3547647","DOI":"10.1145\/3547647"},{"key":"7_CR30","unstructured":"Holdsbjerg-Larsen, R., Spitters, B., Milo, M.: A verified pipeline from a specification language to optimized, safe rust. In: CoqPL\u201922 (2022). https:\/\/popl22.sigplan.org\/details\/CoqPL-2022-papers\/5\/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust"},{"key":"7_CR31","unstructured":"Kiefer, F., et al.: HACSPEC: a gateway to high-assurance cryptography. RealWorldCrypto (2023)"},{"key":"7_CR32","unstructured":"Kroening, D., Schrammel, P., Tautschnig, M.: CBMC: the C bounded model checker. arXiv preprint arXiv:2302.02384 (2023)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Lehmann, N., Geller, A.T., Vazou, N., Jhala, R.: Flux: liquid types for rust. Proc. ACM Program. Lang. 7(PLDI), 1533\u20131557 (2023)","DOI":"10.1145\/3591283"},{"key":"7_CR34","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":"7_CR35","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"NIST: Module-lattice-based key-encapsulation mechanism standard, Technical report, Federal Information Processing Standards Publications (FIPS PUBS) 203, U.S. Department of Commerce, Washington, D.C. (2024). https:\/\/doi.org\/10.6028\/NIST.FIPS.203","DOI":"10.6028\/NIST.FIPS.203"},{"key":"7_CR37","unstructured":"Pernsteiner, S., et al.: Crux, a precise verifier for rust and other languages. arXiv preprint arXiv:2410.18280 (2024)"},{"key":"7_CR38","unstructured":"Polyakov, A., Tsai, M., Wang, B., Yang, B.: Verifying arithmetic assembly programs in cryptographic primitives (invited talk). In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol.\u00a0118, pp. 4:1\u20134:16 (2018)"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Protzenko, J., Beurdouche, B., Merigoux, D., Bhargavan, K.: Formally verified cryptographic web applications in webassembly. In: 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19-23, 2019, pp. 1256\u20131274. IEEE (2019). https:\/\/doi.org\/10.1109\/SP.2019.00064","DOI":"10.1109\/SP.2019.00064"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1(ICFP), 17:1\u201317:29 (2017). https:\/\/doi.org\/10.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"7_CR41","unstructured":"Ramananandro, T., et al.: Everparse: verified secure zero-copy parsers for authenticated message formats. In: 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019, pp. 1465\u20131482. USENIX Association (2019)"},{"key":"7_CR42","doi-asserted-by":"publisher","unstructured":"Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446 (2018). https:\/\/doi.org\/10.17487\/RFC8446","DOI":"10.17487\/RFC8446"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pp. 256\u2013270. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"7_CR44","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The Coq proof assistant (2024). https:\/\/doi.org\/10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"VanHattum, A., Schwartz-Narbonne, D., Chong, N., Sampson, A.: Verifying dynamic trait objects in rust. In: Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice, pp. 321\u2013330 (2022)","DOI":"10.1109\/ICSE-SEIP55303.2022.9794041"},{"key":"7_CR46","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: Hacl*: a verified modern cryptographic library. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pp. 1789\u20131806. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-86695-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:16:16Z","timestamp":1746155776000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-86695-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031866944","9783031866951"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-86695-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"3 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.soundandcomplete.org\/vstte2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}