Abstract
As Rust’s popularity increases, the need for ensuring correctness properties of software written in Rust also increases. In recent years, much work has been done to develop tools to analyze Rust programs, including Property-Based Testing (PBT), model checking, and verification tools. However, developers still need to specify the properties that need to be analyzed and write test harnesses to perform the analysis. We observe that one kind of correctness properties that has been overlooked is correctness invariants of Rust trait implementations; for instance, implementations of the equality trait need to be reflexive, symmetric, and transitive. In this paper, we develop a fully automated tool that allows developers to analyze their implementations of a set of built-in Rust traits. We encoded the test harnesses for the correctness properties of these traits and use Kani to verify them. We evaluated our tool over six open-source Rust libraries and identified three issues in PROST!, a protocol buffer library with nearly 40 million downloads.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Rust verification tools (2021). https://rust-formal-methods.github.io/tools.html
crates.io: Rust Package Registry (2023). https://crates.io/
haybale (2023). https://github.com/PLSysSec/haybale
Introducing the kani vs code extension (2023). https://model-checking.github.io/kani-verifier-blog/2023/06/30/introducing-the-kani-vscode-extension.html
Loom (2023). https://github.com/tokio-rs/loom
Shuttle (2023). https://www.shuttle.rs/
Astrauskas, V., et al.: The Prusti project: formal verification for rust (invited). In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 88–108. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0_5
Denis, X., Jourdan, J.H., Marché, C.: Creusot: a Foundry for the Deductive verification of rust programs. In: Riesco, A., Zhang, M. (eds.) ICFEM 2022. LNCS, vol. 13478, pp. 90–105. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17244-1_6, https://hal.inria.fr/hal-03737878
Erdin, M.: Verification of Rust Generics, Typestates, and Traits. Master’s thesis, ETH Zürich (2019)
Filho, W.A.: Rust in the Linux kernel, April 2021. https://security.googleblog.com/2021/04/rust-in-linux-kernel.html
Ho, S., Protzenko, J.: Aeneas: rust verification by functional translation. Proc. ACM Program. Lang. 6(ICFP), 116:711–116:741 (2022). https://doi.org/10.1145/3547647
Howarth, J.: Why discord is switching from go to rust (2020). https://discord.com/blog/why-discord-is-switching-from-go-to-rust
Jayakar, S.: Rewriting the heart of our sync engine (2020). https://dropbox.tech/infrastructure/rewriting-the-heart-of-our-sync-engine
Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2(POPL), 66:1–66:34 (2017). https://doi.org/10.1145/3158154
Kroening, Daniel, Tautschnig, Michael: CBMC – C bounded model checker. In: Ábrahám, Erika, Havelund, Klaus (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26
Lehmann, N., Geller, A., Vazou, N., Jhala, R.: Flux: Liquid Types for Rust (November 2022). http://arxiv.org/abs/2207.04034
Matsakis, N.D., Klock, F.S.: The rust language. In: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology. pp. 103–104. HILT ’14. Association for Computing Machinery, New York, NY, USA, October 2014. https://doi.org/10.1145/2663171.2663188
Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43, 15:1–15:54 (2021). https://doi.org/10.1145/3462205
Miller, S., Lerche, C.: Sustainability with Rust | AWS Open Source Blog, February 2022. https://aws.amazon.com/blogs/opensource/sustainability-with-rust/, section: Developer Tools
Paraskevopoulou, Zoe, Hriţcu, C.ătălin, Dénès, Maxime, Lampropoulos, Leonidas, Pierce, Benjamin C..: Foundational property-based testing. In: Urban, Christian, Zhang, Xingyuan (eds.) ITP 2015. LNCS, vol. 9236, pp. 325–343. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_22
Schwartz-Narbonne, D.: Use Kani action in CI by danielsn \(\cdot \) Pull Request #1556 \(\cdot \) aws/s2n-quic, October 2022. https://github.com/aws/s2n-quic/pull/1556
Takashima, Y.: Propproof: Free model-checking harnesses from PBT. In: ESEC/FSE (2023)
The proptest developers: Proptest, May 2023. https://github.com/proptest-rs/proptest
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. ICSE-SEIP ’22, pp. 321–330. Association for Computing Machinery (2022). https://doi.org/10.1145/3510457.3513031
Vaughan-Nichols, S.J.: Linux kernel 6.1: Rusty release could be a game-changer (2023). https://www.theregister.com/2022/12/09/linux_kernel_61_column/
Acknowledgements
We would like to thank the anonymous reviewers for their feedback on our paper. This work was partially funded by the National Science Foundation via grants CNS2114148 and an Amazon Research Award, Fall 2022 CFP. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not reflect the views of Amazon.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Byrnes, T., Takashima, Y., Jia, L. (2024). Automatically Enforcing Rust Trait Properties. In: Dimitrova, R., Lahav, O., Wolff, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2024. Lecture Notes in Computer Science, vol 14500. Springer, Cham. https://doi.org/10.1007/978-3-031-50521-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-031-50521-8_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-50520-1
Online ISBN: 978-3-031-50521-8
eBook Packages: Computer ScienceComputer Science (R0)