Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On the Termination of Borrow Checking in Featherweight Rust

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13260))

Included in the following conference series:

Abstract

A distinguished feature of the Rust programming language is its ability to deallocate dynamically-allocated data structures as soon as they go out of scope, without relying on a garbage collector. At the same time, Rust lets programmers create references, called borrows, to data structures. A static borrow checker enforces that borrows can only be used in a controlled way, so that automatic deallocation does not introduce dangling references. Featherweight Rust provides a formalisation for a subset of Rust where borrow checking is encoded using flow typing [40]. However, we have identified a source of non-termination within the calculus which arises when typing environments contain cycles between variables. In fact, it turns out that well-typed programs cannot lead to such environments—but this was not immediately obvious from the presentation. This paper defines a simplification of Featherweight Rust, more amenable to formal proofs. Then it develops a sufficient condition that forbids cycles and, hence, guarantees termination. Furthermore, it proves that this condition is, in fact, maintained by Featherweight Rust for well-typed programs.

Work supported by the SafePKT subproject of the LEDGER MVP Building Programme of the European Commission. Goal of the project is the analysis of Rust code used in the PKT blockchain (https://pkt.cash).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 109.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 139.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    This is a simplification of the \(\mathsf {dangling}(T)\) type in [40], that embeds the shadow type T of a value that has been moved away.

  2. 2.

    This definition is given as a type system in [40] and as a recursive function here.

References

  1. Anderson, B., et al.: Engineering the servo web browser engine using Rust. In: Proceedings of the ICSE, pp. 81–89 (2016)

    Google Scholar 

  2. Ashouri, M.: Etherolic: a practical security analyzer for smart contracts. In: Proceedings of the SAC, pp. 353–356. ACM Press (2020)

    Google Scholar 

  3. Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification. In: Proceedings of the OOPSLA, page Article 147 (2019)

    Google Scholar 

  4. Astrauskas, V., Matheja, C., Poli, F., Müller, P., Summers, A.J.: How do programmers use unsafe Rust? In: Proceedings of the OOPSLA, pp. 136:1–136:27 (2020)

    Google Scholar 

  5. 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 SOSP (2021, to appear)

    Google Scholar 

  6. Balasubramanian, A., Baranowski, M.S., Burtsev, A., Panda, A., Rakamari, Z., Ryzhyk, L.: System programming in Rust: beyond safety. OS Rev. 51(1), 94–99 (2017)

    Google Scholar 

  7. Baranowski, M., He, S., Rakamarić, Z.: Verifying Rust programs with SMACK. In: Proceedings of the ATVA, pp. 528–535 (2018)

    Google Scholar 

  8. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17

    Chapter  Google Scholar 

  9. Bornholt, J., et al.: Using lightweight formal methods to validate a key-value storage node in Amazon S3. In: Proceedings of the SOSP, pp. 836–850. ACM Press (2021)

    Google Scholar 

  10. Dang, H.-H., Jourdan, J.-H., Kaiser, J.-O., Dreyer, D.: RustBelt meets relaxed memory. In: Proceedings of the POPL, page Article 34 (2020)

    Google Scholar 

  11. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  12. Dewey, K., Roesch, J., Hardekopf, B.: Fuzzing the Rust typechecker using CLP (t). In: Proceedings of the ASE, pp. 482–493. IEEE (2015)

    Google Scholar 

  13. Emre, M., Schroeder, R., Dewey, K., Hardekopf, B.: Translating C to safer Rust, pp. 1–29 (2021)

    Google Scholar 

  14. Evans, A.N., Campbell, B., Soffa, M.L.: Is Rust used safely by software developers? In: Proceedings of the ICSE, pp. 246–257. ACM Press (2020)

    Google Scholar 

  15. Hjálmarsson, F.Þ., Hreiðarsson, G.K., Hamdaqa, M., Hjálmtýsson, G.: Blockchain-based e-voting system. In: Proceedings of the CLOUD, pp. 983–986 (2018)

    Google Scholar 

  16. Hua, B., Ouyang, W., Jiang, C., Fan, Q., Pan, Z.: Rupair: towards automatic buffer overflow detection and rectification for Rust. In: Proceedings of the ACSAC, pp. 812–823. ACM Press (2021)

    Google Scholar 

  17. Jespersen, T.B.L., Munksgaard, P., Larsen, K.F.: Session types for Rust. In: Proceedings of the Workshop on Generic Programming (WGP), pp. 13–22 (2015)

    Google Scholar 

  18. Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. In: Proceedings of the POPL, pp. 1–34 (2018)

    Google Scholar 

  19. Jung, R., Dang, H.-H., Kang, J., Dreyer, D.: Stacked borrows: an aliasing model for Rust. In: Proceedings of the POPL, page Article 41 (2020)

    Google Scholar 

  20. Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: Proceedings of the ICFP, pp. 256–269. ACM Press (2016)

    Google Scholar 

  21. Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. JFP 28, e20 (2018)

    Google Scholar 

  22. Kaiser, J.-O., Dang, H.-H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in iris. In: Proceedings of the ECOOP, vol. 74, pp. 17:1–17:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  23. Kokke, W.: Rusty variation: deadlock-free sessions with failure in Rust. In: Proceedings of the ICE, pp. 48–60 (2019)

    Google Scholar 

  24. Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26

  25. Rustan, K., Leino, M.: Developing verified programs with Dafny. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, p. 82. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27705-4_7

  26. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

  27. Levy, A., Campbell, B., Ghena, B., Pannuto, P., Dutta, P., Levis, P.: The case for writing a kernel in Rust. In: Proceedings of the APSYS, pp. 1:1–1:7 (2017)

    Google Scholar 

  28. Levy, A., et al.: Multiprogramming a 64kb computer safely and efficiently. In: Proceedings of the SOSP, pp. 234–251. ACM Press (2017)

    Google Scholar 

  29. Levy, A.A., et al.: Ownership is theft: experiences building an embedded OS in Rust. In: Proceedings of the Workshop on Programming Languages and Operating Systems, pp. 21–26 (2015)

    Google Scholar 

  30. Li, Z., Wang, J., Sun, M., Lui, J.C.S.: MirChecker: detecting bugs in Rust programs via static analysis. In: Proceedings of the CCS, pp. 2183–2196. ACM Press (2021)

    Google Scholar 

  31. Lindner, M., Aparicius, J., Lindgren, P.: No panic! Verification of Rust programs by symbolic execution. In: Proceedings of the INDIN, pp. 108–114 (2018)

    Google Scholar 

  32. Lindner, M., Fitinghoff, N., Eriksson, J., Lindgren, P.: Verification of safety functions implemented in Rust - a symbolic execution based approach. In: Proceedings of the INDIN, pp. 432–439 (2019)

    Google Scholar 

  33. Liu, P., Zhao, G., Huang, J.: Securing unsafe Rust programs with XRust. In: Proceedings of the ICSE, pp. 234–245. ACM Press (2020)

    Google Scholar 

  34. Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. In: ESOP 2020. LNCS, vol. 12075, pp. 484–514. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44914-8_18

  35. Memarian, K., et al.: Exploring C semantics and pointer provenance. In: Proceedings of the POPL, pp. 67:1–67:32 (2019)

    Google Scholar 

  36. Ning, P., Qin, B.: Stuck-me-not: a deadlock detector on blockchain software in Rust. Procedia Comput. Sci. 177, 599–604 (2020)

    Google Scholar 

  37. Olson, S.: Miri: an interpreter for Rust’s mid-level intermediate representation. Technical report (2016)

    Google Scholar 

  38. Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for Java. In: Proceedings of the OOPSLA (Companion), pp. 815–816 (2007)

    Google Scholar 

  39. Pearce, D.J.: Sound and complete flow typing with unions, intersections and negations. In: Proceedings of the VMCAI, pp. 335–354 (2013)

    Google Scholar 

  40. Pearce, D.J.: A lightweight formalism for reference lifetimes and borrowing in Rust. ACM TOPLAS 43(1), Article 3 (2021)

    Google Scholar 

  41. Pearce, D.J., Groves, L.: Designing a verifying compiler: lessons learned from developing Whiley. In: SCP, pp. 191–220 (2015)

    Google Scholar 

  42. Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2018. LNCS, vol. 11430, pp. 1–37. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17601-3_1

  43. Reed, E.: Patina: a formalization of the Rust programming language. Technical report (2015)

    Google Scholar 

  44. Rivera, E., Mergendahl, S., Shrobe, H.E., Okhravi, H., Burow, N.: Keeping safe Rust safe with Galeed. In: Proceedings of the ACSAC, pp. 824–836. ACM Press (2021)

    Google Scholar 

  45. Rosu, G., Serbanuta, T.: An overview of the K semantic framework. JLAP 79(6), 397–434 (2010)

    MathSciNet  MATH  Google Scholar 

  46. Rust Team: The Rust programming language. doc.rust-lang.org/book/. Accessed 05 Jan 2016

  47. Rust Team: The rustonomicon - the dark arts of advanced and unsafe Rust programming. doc.rust-lang.org/nomicon/. Accessed 31 Mar 2020

  48. Toman, J., Pernsteiner, S., Torlak, E.: Crust: a bounded verifier for Rust. In: Proceedings of the ASE, pp. 75–80 (2015)

    Google Scholar 

  49. Utting, M., Pearce, D.J., Groves, L.: Making Whiley Boogie! In: Proceedings of the IFM, pp. 69–84 (2017)

    Google Scholar 

  50. VanHattum, A., Schwartz-Narbonne, D., Chong, N., Sampson, A.: Verifying dynamic trait objects in Rust. In: Proceedings of the ICSE-SEIP (2022, to appear)

    Google Scholar 

  51. Wang, F., Song, F., Zhang, M., Zhu, X., Zhang, J.: KRust: a formal executable semantics of Rust. In: Proceedings of the TASE, pp. 44–51 (2018)

    Google Scholar 

  52. Wang, H., et al.: Towards memory safe enclave programming with Rust-SGX. In: Proceedings of the CCS, pp. 2333–2350. ACM Press (2019)

    Google Scholar 

  53. Wang, P., et al.: Building and maintaining a third-party library supply chain for productive and secure SGX enclave development. In: Proceedings of the ICSE-SEIP, pp. 100–109. ACM Press (2020)

    Google Scholar 

  54. Weiss, A., Patterson, D., Matsakis, N.D., Ahmed, A.: Oxide: The essence of Rust (2019)

    Google Scholar 

  55. Wolff, F., Bílý, A., Matheja, C., Müller, P., Summers, A.J.: Modular specification and verification of closures in Rust. In: Proceedings of the OOPSLA, pp. 1–29 (2021)

    Google Scholar 

  56. Xu, H., Chen, Z., Sun, M., Zhou, Y.: Memory-safety challenge considered solved? An empirical study with all Rust CVEs. CoRR, abs/2003.03296 (2020)

    Google Scholar 

  57. Zhang, F., et al.: The Ekiden platform for confidentiality-preserving, trustworthy, and performant smart contracts. IEEE S&P 18(3), 17–27 (2020)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIM, Université de La Réunion, Saint Denis, France

    Étienne Payet

  2. Victoria University of Wellington, Wellington, New Zealand

    David J. Pearce

  3. Dipartimento di Informatica, Università di Verona, Verona, Italy

    Fausto Spoto

Authors
  1. Étienne Payet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David J. Pearce
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fausto Spoto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David J. Pearce .

Editor information

Editors and Affiliations

  1. University of Southern California, Los Angeles, CA, USA

    Jyotirmoy V. Deshmukh

  2. Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, USA

    Klaus Havelund

  3. National Institute of Aerospace, Hampton, VA, USA

    Ivan Perez

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Payet, É., Pearce, D.J., Spoto, F. (2022). On the Termination of Borrow Checking in Featherweight Rust. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds) NASA Formal Methods. NFM 2022. Lecture Notes in Computer Science, vol 13260. Springer, Cham. https://doi.org/10.1007/978-3-031-06773-0_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-06773-0_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-06772-3

  • Online ISBN: 978-3-031-06773-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation