RustBelt: securing the foundations of the Rust programming language

Abstract

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.

References

1. David Abrahams. 1998. Exception-safety in generic components. In International Seminar on Generic Programming (LNCS).
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.
3. Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2005. A step-indexed model of substructural state. In ICFP.
4. Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L 3 : A linear language with locations. Fundamenta Informaticae 77, 4 (2007), 397–449.
5. Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Ph.D. Dissertation. Princeton University.
6. 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-assurance file system implementations. In ASPLOS.
7. Andrew W. Appel. 2001. Foundational proof-carrying code. In LICS.
8. Andrew W. Appel. 2007. Compiling with Continuations. Cambridge University Press.
9. Andrew W. Appel (Ed.). 2014. Program Logics for Certified Compilers. Cambridge University Press.
10. Andrew W. Appel and David McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS 5 (2001).
11. 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.
12. Thibaut Balabonski, François Pottier, and Jonathan Protzenko. 2016. The design and formalization of Mezzo, a permissionbased programming language. TOPLAS 38, 4 (2016).
13. Ariel Ben-Yehuda. 2015a. Can mutate in match-arm using a closure. Rust issue #27282. https://github.com/rust- lang/rust/ issues/27282 .
14. Ariel Ben-Yehuda. 2015b. dropck can be bypassed via a trait object method. Rust issue #26656. https://github.com/rust- lang/ rust/issues/26656 .
15. 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 .
16. 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 .
17. John Boyland. 2003. Checking interference with fractional permissions. In SAS (LNCS).
18. Arthur Charguéraud and François Pottier. 2017. Temporary read-only permissions for separation logic. In ESOP (LNCS).
19. David G. Clarke, John M. Potter, and James Noble. 1998. Ownership types for flexible alias protection. In OOPSLA.
20. The Coq team. 2017. The Coq proof assistant. https://coq.inria.fr/ .
21. Robert DeLine and Manuel Fähndrich. 2001. Enforcing high-level protocols in low-level software. In PLDI.
22. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: Compositional reasoning for concurrent programs. In POPL.
23. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP (LNCS).
24. Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. 2009. Deny-guarantee reasoning. In ESOP (LNCS).
25. Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical step-indexed logical relations. LMCS 7, 2:16 (2011).
26. Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In POPL.
27. Manuel Fähndrich and Robert DeLine. 2002. Adoption and Focus: Practical Linear Types for Imperative Programming. In PLDI.
28. Matthew Fluet, Greg Morrisett, and Amal J. Ahmed. 2006. Linear regions are all you need. In ESOP (LNCS).
29. Douglas Gregor and Sibylle Schupp. 2003. Making the usage of STL safe. In IFIP TC2 / WG2.1 Working Conference on Generic Programming.
30. Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, and James Cheney. 2002. Region-Based Memory Management in Cyclone. In PLDI.
31. ISO Working Group 21. 2011. Programming languages – C++.
32. Jonas Braband Jensen and Lars Birkedal. 2012. Fictional separation logic. In ESOP (LNCS).
33. 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.
34. Ralf Jung. 2017. MutexGuard〈Cell〈i32〉〉 must not be Sync. Rust issue #41622. https://github.com/rust- lang/rust/issues/ 41622 .
35. 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/ .
36. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP.
37. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš 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.
38. 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.
39. 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.
40. Robbert Krebbers. 2015. The C standard formalized in Coq. Ph.D. Dissertation. Radboud University.
41. 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).
42. Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b. Interactive proofs in higher-order concurrent separation logic. In POPL.
43. Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. 2012. Superficially substructural types. In ICFP.
44. Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. 2017. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL.
45. 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.
46. Xavier Leroy, Andrew Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert memory model, version 2. Technical Report RR-7987. Inria.
47. Nicholas D. Matsakis. 2016a. Introducing MIR. https://blog.rust- lang.org/2016/04/19/MIR.html .
48. Nicholas D. Matsakis. 2016b. Non-lexical lifetimes: Introduction. http://smallcultfollowing.com/babysteps/blog/2016/04/27/ non- lexical- lifetimes- introduction/ .
49. Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust language. In SIGAda Ada Letters, Vol. 34.
50. Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17, 3 (1978), 348–375.
51. 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).
52. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. 2008. Ynot: Dependent types for imperative programs. In ICFP.
53. 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.
54. Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical computer science 375, 1-3 (2007).
55. Gordon Plotkin. 1973. Lambda-definability and logical relations. Unpublished manuscript.
56. Eric Reed. 2015. Patina: A formalization of the Rust programming language. Master’s thesis. University of Washington.
57. John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS.
58. The Rust team. 2016. Drop Check. In The Rustonomicon. https://doc.rust- lang.org/nomicon/dropck.html .
59. The Rust team. 2017. The Rust programming language. http://rust- lang.org/ .
60. Simon Sapin. 2015. Add std::cell::Ref::map and friends. Rust PR #25747. https://github.com/rust- lang/rust/pull/25747# issuecomment- 105175235 .
61. Josh Stone and Nicholas D. Matsakis. 2017. The Rayon library. https://crates.io/crates/rayon .
62. Bjarne Stroustrup. 2012. Foundations of C++. In ESOP.
63. Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In ESOP (LNCS).
64. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016. Dependent types and multi-monadic effects in F*. In POPL.
65. David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. In OOPSLA (PACMPL).
66. W. W. Tait. 1967. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32, 2 (1967).
67. Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A higher-order logic for concurrent termination-preserving refinement. In ESOP (LNCS).
68. 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.
69. John Toman, Stuart Pernsteiner, and Emina Torlak. 2015. CRUST: A bounded verifier for Rust. In ASE.
70. Jesse A. Tov and Riccardo Pucella. 2011. Practical affine types. In POPL.
71. Aaron Turon. 2015a. Abstraction without overhead: Traits in Rust. https://blog.rust- lang.org/2015/05/11/traits.html .
72. Aaron Turon. 2015b. Implied bounds on nested references + variance = soundness hole. Rust issue #25860. https: //github.com/rust- lang/rust/issues/25860 .
73. Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP.
74. Philip Wadler. 1990. Linear types can change the world! In Programming Concepts and Methods.
75. Andrew K Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and computation 115, 1 (1994).

Index Terms

• Theory of computation

  • Logic

    • Programming logic

    • Separation logic

  • Semantics and reasoning

    • Program semantics

      • Operational semantics