Document Open Access Logo

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness

Authors Pedro Carrott , Sacha-Élie Ayoun , Azalea Raad

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.5.pdf
  • Filesize: 1.08 MB
  • 28 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Theory of computation → Separation logic
  • Theory of computation → Programming logic
  • Theory of computation → Automated reasoning
  • Theory of computation → Program specifications
  • Software and its engineering → General programming languages
Keywords
  • Rust
  • bug detection
  • static analysis
  • program logics
  • under-approximation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Rust is a modern programming language marrying the best of language design by offering fine-grained control over system resources (thus enabling efficient implementations), while simultaneously ensuring memory safety and data-race freedom. However, ensuring type safety in internally unsafe libraries remains an important and non-trivial challenge, where unsafe features enable low-level control but can introduce undefined behaviour (UB). Existing works on reasoning about unsafe code either use verification techniques to show correctness (i.e. safety, useful only when the unsafe code is indeed correct), or use bug detection techniques to show incorrectness (i.e. unsafety) but fail to do so automatically (to avoid developer burden), compositionally (to support libraries without a main function), soundly (without false positives) and generally (rather than applying to specific patterns). 
We close this gap by developing RUXt, a fully automatic, compositional bug detection technique for detecting UB in internally unsafe Rust libraries with a formal inadequacy theorem (formalised and proven in Rocq) providing a no-false-positives guarantee. RUXt leverages the Rust type system to under-approximate the set of safe values for user-defined types and detect safety violations without requiring manual annotations by the user. By encoding well-typed values in Rust as separation logic assertions, RUXt enables compositional reasoning about types to refute unsound type signatures and detect UB. The inadequacy theorem of RUXt ensures that each UB detected by RUXt in an internally unsafe library is a true safety violation that can be triggered by a safe program, i.e. one that solely interacts with the safe API of the library. To this end, when RUXt identifies a UB, it additionally produces a safe program witnessing the UB. In addition, we develop a prototype implementation in OCaml that can analyse programs written in a small model of Rust, and apply it to several case studies, showcasing its ability to detect true safety violations.

Cite As Get BibTex

Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad. Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.5

Author Details

Pedro Carrott
  • Imperial College London, UK
Sacha-Élie Ayoun
  • Imperial College London, UK
Azalea Raad
  • Imperial College London, UK

Funding

This project was sponsored by the Defense Advanced Research Projects Agency, (DARPA), Information Innovation Office (I2O), Program BAA HR001124S0003, under Cooperative Agreement No. HR00112420359. Disclaimer: The content of the information does not necessarily reflect the position or the policy of the U.S. Government, and no official endorsement should be inferred. Raad is further supported by the UKRI Future Leaders Fellowship MR/V024299/1, by the EPSRC grant EP/X037029/1 and by VeTSS.

Supplementary Materials

References

  1. Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, and Philippa Gardner. A Hybrid Approach to Semi-Automated Rust Verification. Proc. ACM Program. Lang., 9(PLDI), June 2025. URL: https://doi.org/10.1145/3729289.
  2. Yechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim, and Taesoo Kim. Rudra: Finding memory safety bugs in rust at the ecosystem scale. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, SOSP '21, pages 84-99, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3477132.3483570.
  3. Ariel Ben-Yehuda. std::thread::joinguard (and scoped) are unsound because of reference cycles. rust issue #24292, 2015. URL: https://github.com/rust-lang/rust/issues/24292.
  4. Christophe Biocca. std::vec::intoiter::as_mut_slice borrows &self, returns &mut of contents. rust issue #39465, 2017. URL: https://github.com/rust-lang/rust/issues/39465.
  5. Twain Byrnes, Yoshiki Takashima, and Limin Jia. Automatically enforcing rust trait properties. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, Verification, Model Checking, and Abstract Interpretation, pages 210-223, Cham, 2024. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-50521-8_10.
  6. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08, pages 209-224, USA, December 2008. USENIX Association. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  7. Nima Rahimi Foroushaani and Bart Jacobs. Modular Formal Verification of Rust Programs with Unsafe Blocks, December 2022. URL: https://doi.org/10.48550/arXiv.2212.12976.
  8. José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, part i: A multi-language platform for symbolic execution. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, pages 927-942, New York, NY, USA, June 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3385412.3386014.
  9. José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner. JaVerT 2.0: Compositional symbolic execution for JavaScript. Proceedings of the ACM on Programming Languages, 3(POPL):66:1-66:31, January 2019. URL: https://doi.org/10.1145/3290379.
  10. Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. Refinedrust: A type system for high-assurance verification of rust programs. Proc. ACM Program. Lang., 8(PLDI), June 2024. URL: https://doi.org/10.1145/3656422.
  11. Patrice Godefroid. Compositional dynamic test generation. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '07, pages 47-54, New York, NY, USA, January 2007. Association for Computing Machinery. URL: https://doi.org/10.1145/1190216.1190226.
  12. Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: Directed automated random testing. SIGPLAN Not., 40(6):213-223, June 2005. URL: https://doi.org/10.1145/1064978.1065036.
  13. Patrice Godefroid, Aditya Nori, and Sriram Rajamani. Compositional May-Must Program Analysis: Unleashing The Power of Alternation, January 2009. Google Scholar
  14. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pages 14-26, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/360204.375719.
  15. Bart Jacobs, Jan Smans, and Frank Piessens. A Quick Tour of the VeriFast Program Verifier. In Kazunori Ueda, editor, Programming Languages and Systems, Lecture Notes in Computer Science, pages 304-311, Berlin, Heidelberg, 2010. Springer. URL: https://doi.org/10.1007/978-3-642-17164-2_21.
  16. Ralf Jung. The Scope of Unsafe. https://www.ralfj.de/blog/2016/01/09/the-scope-of-unsafe.html, January 2016. Google Scholar
  17. Ralf Jung. Mutexguard> must not be sync. rust issue #41622, 2017. URL: https://github.com/rust-lang/rust/issues/41622.
  18. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. Stacked borrows: An aliasing model for Rust. Proceedings of the ACM on Programming Languages, 4(POPL):41:1-41:32, December 2019. URL: https://doi.org/10.1145/3371109.
  19. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158154.
  20. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, November 2018. URL: https://doi.org/10.1017/S0956796818000151.
  21. Yunho Kim, Shin Hong, and Moonzoo Kim. Target-driven compositional concolic testing with function summary refinement for effective bug detection. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2019, pages 16-26, New York, NY, USA, August 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3338906.3338934.
  22. Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages, 2(ICFP), July 2018. URL: https://doi.org/10.1145/3236772.
  23. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust Programs using Linear Ghost Types. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):85:286-85:315, April 2023. URL: https://doi.org/10.1145/3586037.
  24. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn. Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang., 6(OOPSLA1), April 2022. URL: https://doi.org/10.1145/3527325.
  25. Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In Jonathan Aldrich and Guido Salvaneschi, editors, 38th European Conference on Object-Oriented Programming (ECOOP 2024), volume 313 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:28, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2024.25.
  26. Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, and Philippa Gardner. Gillian, Part II: Real-World Verification for JavaScript and C. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 827-850, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-81688-9_38.
  27. Nicholas D. Matsakis and Felix S. Klock. The rust language. In Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT '14, pages 103-104, New York, NY, USA, October 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2663171.2663188.
  28. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, pages 41-62, Berlin, Heidelberg, 2016. Springer. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  29. Peter W. O'Hearn. Incorrectness logic. Proc. ACM Program. Lang., 4(POPL):10:1-10:32, December 2019. URL: https://doi.org/10.1145/3371078.
  30. Kelvin Qian, Scott Smith, Brandon Stride, Shiwei Weng, and Ke Wu. Semantic-Type-Guided Bug Finding. Software Artifact for Semantic-Type-Guided Bug Finding, 8(OOPSLA2):348:2183-348:2210, October 2024. URL: https://doi.org/10.1145/3689788.
  31. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, and Jules Villard. Local reasoning about the presence of bugs: Incorrectness separation logic. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification, pages 225-252, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-53291-8_14.
  32. Steven Ramsay and Charlie Walpole. Ill-Typed Programs Don't Evaluate. Proceedings of the ACM on Programming Languages, 8(POPL):2010-2040, January 2024. URL: https://doi.org/10.1145/3632909.
  33. Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. RefinedC: Automating the foundational verification of C code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 158-174, New York, NY, USA, June 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454036.
  34. Yoshiki Takashima, Chanhee Cho, Ruben Martins, Limin Jia, and Corina S. Păsăreanu. Crabtree: Rust API Test Synthesis Guided by Coverage and Type. Artifact Package for Paper "Crabtree: Rust API Test Synthesis Guided by Coverage and Type", 8(OOPSLA2):293:618-293:647, October 2024. URL: https://doi.org/10.1145/3689733.
  35. The Kani Team. How Open Source Projects are Using Kani to Write Better Software in Rust - AWS Open Source Blog. https://aws.amazon.com/blogs/opensource/how-open-source-projects-are-using-kani-to-write-better-software-in-rust/, November 2023. Google Scholar
  36. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 269-282, New York, NY, USA, August 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2628136.2628161.
  37. Neven Villani, Johannes Hostert, Derek Dreyer, and Ralf Jung. Tree Borrows, November 2024. URL: https://jhostert.de/assets/pdf/papers/villani2024trees.pdf.
  38. Robin Webbers, Klaus Von Gleissenthall, and Ranjit Jhala. Refinement Type Refutations. Proceedings of the ACM on Programming Languages, 8(OOPSLA2):962-987, October 2024. URL: https://doi.org/10.1145/3689745.
  39. Yizhuo Zhai, Yu Hao, Hang Zhang, Daimeng Wang, Chengyu Song, Zhiyun Qian, Mohsen Lesani, Srikanth V. Krishnamurthy, and Paul Yu. UBITect: A precise and scalable method to detect use-before-initialization bugs in Linux kernel. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, pages 221-232, New York, NY, USA, November 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3368089.3409686.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact