{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:09:26Z","timestamp":1781258966667,"version":"3.54.1"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["683289"],"award-info":[{"award-number":["683289"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.<\/jats:p>","DOI":"10.1145\/3158154","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":256,"title":["RustBelt: securing the foundations of the Rust programming language"],"prefix":"10.1145","volume":"2","author":[{"given":"Ralf","family":"Jung","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39953-4_6"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086376"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1365997.1366003"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_2_2_8_1","volume-title":"Compiling with Continuations","author":"Appel Andrew W."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_2_2_13_1","unstructured":"Ariel Ben-Yehuda. 2015a. Can mutate in match-arm using a closure. Rust issue #27282. https:\/\/github.com\/rust- lang\/rust\/ issues\/27282 .  Ariel Ben-Yehuda. 2015a. Can mutate in match-arm using a closure. Rust issue #27282. https:\/\/github.com\/rust- lang\/rust\/ issues\/27282 ."},{"key":"e_1_2_2_14_1","unstructured":"Ariel Ben-Yehuda. 2015b. dropck can be bypassed via a trait object method. Rust issue #26656. https:\/\/github.com\/rust- lang\/ rust\/issues\/26656 .  Ariel Ben-Yehuda. 2015b. dropck can be bypassed via a trait object method. Rust issue #26656. https:\/\/github.com\/rust- lang\/ rust\/issues\/26656 ."},{"key":"e_1_2_2_15_1","unstructured":"Ariel Ben-Yehuda. 2015c. std::thread::JoinGuard (and scoped) are unsound because of reference cycles. Rust issue #24292. https:\/\/github.com\/rust- lang\/rust\/issues\/24292 .  Ariel Ben-Yehuda. 2015c. std::thread::JoinGuard (and scoped) are unsound because of reference cycles. Rust issue #24292. https:\/\/github.com\/rust- lang\/rust\/issues\/24292 ."},{"key":"e_1_2_2_16_1","unstructured":"Christophe Biocca. 2017. std::vec::IntoIter::as_mut_slice borrows &self returns &mut of contents. Rust issue #39465. https:\/\/github.com\/rust- lang\/rust\/issues\/39465 .  Christophe Biocca. 2017. std::vec::IntoIter::as_mut_slice borrows &self returns &mut of contents. Rust issue #39465. https:\/\/github.com\/rust- lang\/rust\/issues\/39465 ."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_2_20_1","unstructured":"The Coq team. 2017. The Coq proof assistant. https:\/\/coq.inria.fr\/ .  The Coq team. 2017. The Coq proof assistant. https:\/\/coq.inria.fr\/ ."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_2"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35672-3_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_31_1","unstructured":"ISO Working Group 21. 2011. Programming languages \u2013 C++.  ISO Working Group 21. 2011. Programming languages \u2013 C++."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_2_33_1","volume-title":"Cyclone: A safe dialect of C. In USENIX ATC.","author":"Jim Trevor","year":"2002"},{"key":"e_1_2_2_34_1","unstructured":"Ralf Jung. 2017. MutexGuard\u3008Cell\u3008i32\u3009\u3009 must not be Sync. Rust issue #41622. https:\/\/github.com\/rust- lang\/rust\/issues\/ 41622 .  Ralf Jung. 2017. MutexGuard\u3008Cell\u3008i32\u3009\u3009 must not be Sync. Rust issue #41622. https:\/\/github.com\/rust- lang\/rust\/issues\/ 41622 ."},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2017a. RustBelt: Securing the foundations of the Rust programming language \u2013 Technical appendix and Coq development. https:\/\/plv.mpi- sws.org\/rustbelt\/popl18\/ .  Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2017a. RustBelt: Securing the foundations of the Rust programming language \u2013 Technical appendix and Coq development. https:\/\/plv.mpi- sws.org\/rustbelt\/popl18\/ .","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2017b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. (2017). Conditionally accepted to Journal of Functional Programming.  Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2017b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. (2017). Conditionally accepted to Journal of Functional Programming.","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_39_1","unstructured":"Jan-Oliver Kaiser Hoang-Hai Dang Derek Dreyer Ori Lahav and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP.  Jan-Oliver Kaiser Hoang-Hai Dang Derek Dreyer Ori Lahav and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364536"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009877"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_2_2_47_1","unstructured":"Nicholas D. Matsakis. 2016a. Introducing MIR. https:\/\/blog.rust- lang.org\/2016\/04\/19\/MIR.html .  Nicholas D. Matsakis. 2016a. Introducing MIR. https:\/\/blog.rust- lang.org\/2016\/04\/19\/MIR.html ."},{"key":"e_1_2_2_48_1","unstructured":"Nicholas D. Matsakis. 2016b. Non-lexical lifetimes: Introduction. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2016\/04\/27\/ non- lexical- lifetimes- introduction\/ .  Nicholas D. Matsakis. 2016b. Non-lexical lifetimes: Introduction. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2016\/04\/27\/ non- lexical- lifetimes- introduction\/ ."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_55_1","unstructured":"Gordon Plotkin. 1973. Lambda-definability and logical relations. Unpublished manuscript.  Gordon Plotkin. 1973. Lambda-definability and logical relations. Unpublished manuscript."},{"key":"e_1_2_2_56_1","volume-title":"Patina: A formalization of the Rust programming language. Master\u2019s thesis","author":"Reed Eric","year":"2015"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_58_1","unstructured":"The Rust team. 2016. Drop Check. In The Rustonomicon. https:\/\/doc.rust- lang.org\/nomicon\/dropck.html .  The Rust team. 2016. Drop Check. In The Rustonomicon. https:\/\/doc.rust- lang.org\/nomicon\/dropck.html ."},{"key":"e_1_2_2_59_1","unstructured":"The Rust team. 2017. The Rust programming language. http:\/\/rust- lang.org\/ .  The Rust team. 2017. The Rust programming language. http:\/\/rust- lang.org\/ ."},{"key":"e_1_2_2_60_1","unstructured":"Simon Sapin. 2015. Add std::cell::Ref::map and friends. Rust PR #25747. https:\/\/github.com\/rust- lang\/rust\/pull\/25747# issuecomment- 105175235 .  Simon Sapin. 2015. Add std::cell::Ref::map and friends. Rust PR #25747. https:\/\/github.com\/rust- lang\/rust\/pull\/25747# issuecomment- 105175235 ."},{"key":"e_1_2_2_61_1","volume-title":"Matsakis","author":"Stone Josh","year":"2017"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_1"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_68_1","doi-asserted-by":"crossref","unstructured":"Amin Timany L\u00e9o Stefanesco Morten Krogh-Jespersen and Lars Birkedal. 2018. A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST. Accepted to POPL.  Amin Timany L\u00e9o Stefanesco Morten Krogh-Jespersen and Lars Birkedal. 2018. A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST. Accepted to POPL.","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_69_1","volume-title":"CRUST: A bounded verifier for Rust. In ASE.","author":"Toman John","year":"2015"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926436"},{"key":"e_1_2_2_71_1","unstructured":"Aaron Turon. 2015a. Abstraction without overhead: Traits in Rust. https:\/\/blog.rust- lang.org\/2015\/05\/11\/traits.html .  Aaron Turon. 2015a. Abstraction without overhead: Traits in Rust. https:\/\/blog.rust- lang.org\/2015\/05\/11\/traits.html ."},{"key":"e_1_2_2_72_1","unstructured":"Aaron Turon. 2015b. Implied bounds on nested references + variance = soundness hole. Rust issue #25860. https: \/\/github.com\/rust- lang\/rust\/issues\/25860 .  Aaron Turon. 2015b. Implied bounds on nested references + variance = soundness hole. Rust issue #25860. https: \/\/github.com\/rust- lang\/rust\/issues\/25860 ."},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_74_1","unstructured":"Philip Wadler. 1990. Linear types can change the world! In Programming Concepts and Methods.  Philip Wadler. 1990. Linear types can change the world! In Programming Concepts and Methods."},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158154","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158154","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158154"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":72,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158154"],"URL":"https:\/\/doi.org\/10.1145\/3158154","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}