Elamur Research⌕
☰
home / papers / 2018 / RustBelt: Securing the Foundations of the Rust Programming Language

RustBelt: Securing the Foundations of the Rust Programming Language

Paper · 2018 · Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers et al.

Summary

Rust promises the resource control of C together with the type and memory safety of high-level languages, but none of these guarantees had been formally proven. The main obstacle is that Rust's ownership-based type system is extended by libraries whose internals use unsafe code. The classic "progress and preservation" method assumes a fixed set of typing rules, so it cannot account for this open-world design.

The authors define λRust, a continuation-passing core language inspired by Rust's MIR. It captures borrowing, lifetimes and lifetime inclusion. They then give a semantic soundness proof using a step-indexed logical relation built in the Iris separation-logic framework and mechanized in Coq. Because the model defines what each type means semantically, every library containing unsafe code gets a precise verification condition. Meeting that condition shows the library safely extends the type system. The authors discharge these conditions for several central standard libraries, many of which rely on interior mutability.

This is the first machine-checked safety proof for a realistic Rust subset. The work also uncovered a real soundness bug in Rust's standard library.

Key points

  • λRust scope and simplifications:
    • Omits traits and trait objects, stack unwinding on panic, automatic destruction, proper type polymorphism and unsized types such as [i32].
    • Uses a simplified memory model with only non-atomic and sequentially consistent atomic accesses, so the relaxed atomics that libraries like Arc use for efficiency are not modeled.
  • Proof infrastructure: The proof relies on three Iris features:
    • custom logical resources ("fictional separation"), used to encode borrow propositions in a new lifetime logic;
    • impredicative invariants;
    • tactic-based proving in Coq.
  • Verified code: Libraries with unsafe implementations were proven safely encapsulated by their types, including their destructors. Examples include RefCell and its subtle Ref::map and RefMut::map functions.
  • Practical impact:
    • The verification found and fixed a previously unknown bug in Rust's standard library [Jung 2017].
    • λRust already supports non-lexical lifetimes, which Rust itself was still designing at the time.
  • Related work and publication:
    • Patina provides only partial syntactic proofs.
    • CRUST is a bounded model checker that examines one library at a time, so it misses bugs arising from interactions between libraries, such as Leakpocalypse.
    • The paper appeared at POPL 2018 (PACMPL 2, Article 66) and was funded by ERC grant 683,289.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🔬Max Planck Institute for Software SystemsSaarbrücken · Germany6 works · 39,162 citations🎓Delft University of TechnologyDelft · Netherlands9 works · 771 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Code & programming languages · 194 works

Cite

Cite as Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers and Derek Dreyer. 2018. RustBelt: Securing the Foundations of the Rust Programming Language. POPL 2018.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{jung2018rustbelt,
  title = {{RustBelt: Securing the Foundations of the Rust Programming Language}},
  author = {Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers and Derek Dreyer},
  booktitle = {POPL 2018},
  year = {2018},
  doi = {10.1145/3158154},
  url = {https://doi.org/10.1145/3158154}
}

References

60 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. David Abrahams. 1998. Exception-safety in generic components. In International Seminar on Generic Programming (LNCS). https://doi.org/10.1007/3-540-39953-4_6 — [doi:10.1007/3-540-39953-4_6](https://doi.org/10.1007/3-540-39953-4_6) ↗
  2. Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, and Daniel C. Wang. 2010. Semantic foundations for typed assembly languages. TOPLAS 32, 3 (2010), 1ś67. find
  3. Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2005. A step-indexed model of substructural state. In ICFP. https://doi.org/10.1145/1086365.1086376 Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L 3 : A linear language with locations. Fundamenta Informaticae 77, 4 (2007), 397ś449. — [doi:10.1145/1086365.1086376](https://doi.org/10.1145/1086365.1086376) ↗
  4. Amal Jamil Ahmed. 2004. Semantics of types for mutable state. find
  5. Ph.D. Dissertation. Princeton University. Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. 2016. Cogent: Verifying high-assura… — [doi:10.1145/2872362.2872404](https://doi.org/10.1145/2872362.2872404) find
  6. Andrew W. Appel. 2001. Foundational proof-carrying code. In LICS. find
  7. Andrew W. Appel. 2007. Compiling with Continuations. Cambridge University Press. Andrew W. Appel (Ed.). 2014. Program Logics for Certified Compilers. find
  8. Cambridge University Press. Andrew W. Appel and David McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS 5 (2001). https://doi.org/10.1145/504709.504712 — [doi:10.1145/504709.504712](https://doi.org/10.1145/504709.504712) ↗
  9. Andrew W. Appel, Paul-André Melliès, Christopher Richards, and Jérôme Vouillon. 2007. A very modal model of a modern, major, general type system. In POPL. https://doi.org/10.1145/1190216.1190235 — [doi:10.1145/1190216.1190235](https://doi.org/10.1145/1190216.1190235) ↗
  10. Thibaut Balabonski, François Pottier, and Jonathan Protzenko. 2016. The design and formalization of Mezzo, a permission-based programming language. TOPLAS 38, 4 (2016). https://doi.org/10.1145/2837022 — [doi:10.1145/2837022](https://doi.org/10.1145/2837022) ↗
  11. Ariel Ben-Yehuda. 2015a. Can mutate in match-arm using a closure. Rust issue \#27282. https://github.com/rust-lang/rust/ issues/27282. ↗
  12. Ariel Ben-Yehuda. 2015b. dropck can be bypassed via a trait object method. Rust issue \#26656. https://github.com/rust-lang/ rust/issues/26656. ↗
  13. 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. ↗
  14. 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. ↗
  15. John Boyland. 2003. Checking interference with fractional permissions. In SAS (LNCS). https://doi.org/10.1007/ 3-540-44898-5_4 Arthur Charguéraud and François Pottier. 2017. Temporary read-only permissions for separation logic. In ESOP (LNCS). https://doi.org/10.1007/978-3-662-54434-1_10 — [doi:10.1007/978-3-662-54434-1_10](https://doi.org/10.1007/978-3-662-54434-1_10) find
  16. David G. Clarke, John M. Potter, and James Noble. 1998. Ownership types for flexible alias protection. In OOPSLA. https://doi.org/10.1145/286936.286947 The Coq team. 2017. The Coq proof assistant. https://coq.inria.fr/. — [doi:10.1145/286936.286947](https://doi.org/10.1145/286936.286947) ↗
  17. Robert DeLine and Manuel Fähndrich. 2001. Enforcing high-level protocols in low-level software. In PLDI. https://doi.org/ 10.1145/381694.378811 — [doi:10.1145/381694.378811](https://doi.org/10.1145/381694.378811) find
  18. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: Compositional reasoning for concurrent programs. In POPL. https://doi.org/10.1145/2429069.2429104 — [doi:10.1145/2429069.2429104](https://doi.org/10.1145/2429069.2429104) ↗
  19. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP (LNCS). https://doi.org/10.1007/978-3-642-14107-2_24 — [doi:10.1007/978-3-642-14107-2_24](https://doi.org/10.1007/978-3-642-14107-2_24) ↗
  20. Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. 2009. Deny-guarantee reasoning. In ESOP (LNCS). https://doi.org/10.1007/978-3-642-00590-9_26 — [doi:10.1007/978-3-642-00590-9_26](https://doi.org/10.1007/978-3-642-00590-9_26) ↗
  21. Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical step-indexed logical relations. LMCS 7, 2:16 (2011). https://doi.org/10.2168/LMCS-7(2:16)2011 Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In POPL. https://doi… — [doi:10.2168/lmcs-7(2:16)2011](https://doi.org/10.2168/lmcs-7%282:16%292011) ↗
  22. Manuel Fähndrich and Robert DeLine. 2002. Adoption and Focus: Practical Linear Types for Imperative Programming. In PLDI. https://doi.org/10.1145/512529.512532 — [doi:10.1145/512529.512532](https://doi.org/10.1145/512529.512532) ↗
  23. Matthew Fluet, Greg Morrisett, and Amal J. Ahmed. 2006. Linear regions are all you need. In ESOP (LNCS). https://doi.org/10.1007/11693024_2 Douglas Gregor and Sibylle Schupp. 2003. Making the usage of STL safe. In IFIP TC2 / WG2.1 Working Conference on Generic Programming. https://doi.org/10.1007/9… — [doi:10.1007/11693024_2](https://doi.org/10.1007/11693024_2) ↗
  24. Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, and James Cheney. 2002. Region-Based Memory Management in Cyclone. In PLDI. https://doi.org/10.1145/512529.512563 — [doi:10.1145/512529.512563](https://doi.org/10.1145/512529.512563) ↗
  25. ISO Working Group 21. 2011. Programming languages ś C++. find
  26. Jonas Braband Jensen and Lars Birkedal. 2012. Fictional separation logic. In ESOP (LNCS). https://doi.org/10.1007/ 978-3-642-28869-2_19 Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A safe dialect of C. In USENIX ATC. find
  27. Ralf Jung. 2017. MutexGuard\<Cell\<i32\>\> must not be Sync. Rust issue \#41622. https://github.com/rust-lang/rust/issues/ 41622. ↗
  28. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017a. RustBelt: Securing the foundations of the Rust programming language ś Technical appendix and Coq development. https://plv.mpi-sws.org/rustbelt/popl18/. ↗
  29. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. https://doi.org/10. 1145/2951913.2951943 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2017b. Iris from the ground up: A modular foundation for h… find
  30. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. https://doi.org/10.1145/2676726.2676980 — [doi:10.1145/2676726.2676980](https://doi.org/10.1145/2676726.2676980) ↗
  31. 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. find
  32. Robbert Krebbers. 2015. The C standard formalized in Coq. find
  33. Ph.D. Dissertation. Radboud University. Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017a. The essence of higher-order concurrent separation logic. In ESOP (LNCS). https://doi.org/10.1007/978-3-662-54434-1_26 — [doi:10.1007/978-3-662-54434-1_26](https://doi.org/10.1007/978-3-662-54434-1_26) ↗
  34. Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b. Interactive proofs in higher-order concurrent separation logic. In POPL. https://doi.org/10.1145/3009837.3009855 — [doi:10.1145/3009837.3009855](https://doi.org/10.1145/3009837.3009855) ↗
  35. Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. 2012. Superficially substructural types. In ICFP. https://doi.org/10.1145/2364527.2364536 — [doi:10.1145/2364527.2364536](https://doi.org/10.1145/2364527.2364536) ↗
  36. Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. 2017. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL. https://doi.org/10.1145/3009837.3009877 — [doi:10.1145/3009837.3009877](https://doi.org/10.1145/3009837.3009877) ↗
  37. Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, and Nuno P. Lopes. 2017. Taming undefined behavior in LLVM. In PLDI. https://doi.org/10.1145/3062341.3062343 — [doi:10.1145/3062341.3062343](https://doi.org/10.1145/3062341.3062343) ↗
  38. Xavier Leroy, Andrew Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert memory model, version 2. Technical Report RR-7987. find
  39. Inria. Nicholas D. Matsakis. 2016a. Introducing MIR. https://blog.rust-lang.org/2016/04/19/MIR.html. ↗
  40. Nicholas D. Matsakis. 2016b. Non-lexical lifetimes: Introduction. http://smallcultfollowing.com/babysteps/blog/2016/04/27/ non-lexical-lifetimes-introduction/. ↗
  41. Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust language. In SIGAda Ada Letters, Vol. 34. https://doi.org/10.1145/ 2663171.2663188 Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17, 3 (1978), 348ś375. https://doi.org/10.1016/0022-0000(78)90014-4 find
  42. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating state transition systems for fine-grained concurrent resources. In ESOP (LNCS). https://doi.org/10.1007/978-3-642-54833-8_16 — [doi:10.1007/978-3-642-54833-8_16](https://doi.org/10.1007/978-3-642-54833-8_16) ↗
  43. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. 2008. Ynot: Dependent types for imperative programs. In ICFP. https://doi.org/10.1145/1411204.1411237 — [doi:10.1145/1411204.1411237](https://doi.org/10.1145/1411204.1411237) ↗
  44. Liam O’Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, and Gerwin Klein. 2016. Refinement through restraint: Bringing down the cost of verification. In ICFP. https://doi.org/10.1145/2951913.2951940 Peter W. O’Hearn. 2007. Resources,… — [doi:10.1145/2951913.2951940](https://doi.org/10.1145/2951913.2951940) ↗
  45. Gordon Plotkin. 1973. Lambda-definability and logical relations. Unpublished manuscript. find
  46. Eric Reed. 2015. Patina: A formalization of the Rust programming language. Master’s thesis. University of Washington. find
  47. John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. https://doi.org/10.1109/LICS. 2002.1029817 The Rust team. 2016. Drop Check. In The Rustonomicon. https://doc.rust-lang.org/nomicon/dropck.html. The Rust team. 2017. The Rust programming language. http://ru… — [doi:10.1109/lics](https://doi.org/10.1109/lics) ↗
  48. Simon Sapin. 2015. Add std::cell::Ref::map and friends. Rust PR \#25747. https://github.com/rust-lang/rust/pull/25747\# issuecomment-105175235. ↗
  49. Josh Stone and Nicholas D. Matsakis. 2017. The Rayon library. https://crates.io/crates/rayon. ↗
  50. Bjarne Stroustrup. 2012. Foundations of C++. In ESOP. https://doi.org/10.1007/978-3-642-28869-2_1 — [doi:10.1007/978-3-642-28869-2_1](https://doi.org/10.1007/978-3-642-28869-2_1) ↗
  51. Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In ESOP (LNCS). https://doi.org/10. 1007/978-3-642-54833-8_9 Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves S… — [doi:10.1145/2837614.2837655](https://doi.org/10.1145/2837614.2837655) find
  52. David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. In OOPSLA (PACMPL). https://doi.org/10.1145/3133913 — [doi:10.1145/3133913](https://doi.org/10.1145/3133913) ↗
  53. W. W. Tait. 1967. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32, 2 (1967). https://doi.org/10.2307/2271658 Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A higher-order logic for concurrent termination-preserving refinement. In ESOP (LNCS). https:… — [doi:10.2307/2271658](https://doi.org/10.2307/2271658) ↗
  54. Amin Timany, Léo 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. find
  55. John Toman, Stuart Pernsteiner, and Emina Torlak. 2015. CRUST: A bounded verifier for Rust. In ASE. https://doi.org/10. 1109/ASE.2015.77 Jesse A. Tov and Riccardo Pucella. 2011. Practical affine types. In POPL. https://doi.org/10.1145/1926385.1926436 — [doi:10.1145/1926385.1926436](https://doi.org/10.1145/1926385.1926436) find
  56. Aaron Turon. 2015a. Abstraction without overhead: Traits in Rust. https://blog.rust-lang.org/2015/05/11/traits.html. ↗
  57. Aaron Turon. 2015b. Implied bounds on nested references + variance = soundness hole. Rust issue \#25860. https://github.com/rust-lang/rust/issues/25860. ↗
  58. Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. https://doi.org/10.1145/2500365.2500600 — [doi:10.1145/2500365.2500600](https://doi.org/10.1145/2500365.2500600) ↗
  59. Philip Wadler. 1990. Linear types can change the world! In Programming Concepts and Methods. find
  60. Andrew K Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and computation 115, 1 (1994). https://doi.org/10.1006/inco.1994.1093 ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/jung-2018-rustbelt-securing-foundations-rust-programming/