Document Open Access Logo

Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding

Authors Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, Philippa Gardner

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.19.pdf
  • Filesize: 0.87 MB
  • 27 pages

Document Identifiers

Author Details

Petar Maksimović
  • Imperial College London, UK
  • Runtime Verification Inc., Urbana, IL, USA
Caroline Cronjäger
  • Ruhr-Universität Bochum, Germany
Andreas Lööw
  • Imperial College London, UK
Julian Sutherland
  • Nethermind, London, UK
Philippa Gardner
  • Imperial College London, UK

Funding

Maksimović, Lööw and Gardner were partially supported by the EPSRC Fellowship "VetSpec: Verified Trustworthy Software Specification" (EP/R034567/1). Cronjäger was partially supported by the Erasmus Plus Student Mobility for Traineeships scheme.

Acknowledgements

We would like to thank Sacha-Élie Ayoun and Daniele Nantes Sobrinho for the many discussions that have improved the quality of the paper. We would also like to thank the anonymous reviewers for their comments.

Cite As Get BibTex

Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 19:1-19:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ECOOP.2023.19

Abstract

Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised.
We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Program reasoning
  • Theory of computation → Separation logic
  • Theory of computation → Hoare logic
  • Theory of computation → Abstraction
Keywords
  • Separation logic
  • program correctness
  • program incorrectness
  • abstraction

Metrics

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

Related Versions

References

  1. Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-driven compositional symbolic execution. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_28.
  2. Saswat Anand, Corina S. Pasareanu, and Willem Visser. Symbolic execution with abstraction. International Journal on Software Tools for Technology Transfer, 11(1), 2009. URL: https://doi.org/10.1007/s10009-008-0090-1.
  3. Andrew W. Appel. Coq’s vibrant ecosystem for verification engineering. In Conference on Certified Programs and Proofs (CPP), 2022. URL: https://doi.org/10.1145/3497775.3503951.
  4. Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. A logic for locally complete abstract interpretations. In Symposium on Logic in Computer Science (LICS), 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470608.
  5. Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. A correctness and incorrectness program logic. Journal of the ACM, 70(2), 2023. URL: https://doi.org/10.1145/3582267.
  6. Arthur Charguéraud. Separation logic for sequential programs (functional pearl). Proceedings of the ACM on Programming Languages, 4(ICFP), 2020. URL: https://doi.org/10.1145/3408998.
  7. Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. Modular termination verification for non-blocking concurrency. In European Symposium on Programming (ESOP), 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_8.
  8. Edsko de Vries and Vasileios Koutavas. Reverse Hoare logic. In Software Engineering and Formal Methods (SEFM), 2011. URL: https://doi.org/10.1007/978-3-642-24690-6_12.
  9. Robert W. Floyd. Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics, 19, 1967. Google Scholar
  10. José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, part I: A multi-language platform for symbolic execution. In Programming Language Design and Implementation (PLDI), 2020. URL: https://doi.org/10.1145/3385412.3386014.
  11. José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby, and Philippa Gardner. Symbolic execution for JavaScript. In Principles and Practice of Declarative Programming (PPDP), 2018. URL: https://doi.org/10.1145/3236950.3236956.
  12. José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner. JaVerT: JavaScript verification toolchain. Proceedings of the ACM on Programming Languages, 2(POPL), 2018. URL: https://doi.org/10.1145/3158138.
  13. 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), 2019. URL: https://doi.org/10.1145/3290379.
  14. Philippa Gardner, Sergio Maffeis, and Gareth David Smith. Towards a program logic for JavaScript. In Principles of Programming Languages (POPL), 2012. URL: https://doi.org/10.1145/2103656.2103663.
  15. Patrice Godefroid. Compositional dynamic test generation. In Principles of Programming Languages (POPL), 2007. URL: https://doi.org/10.1145/1190216.1190226.
  16. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and Sai Deep Tetali. Compositional may-must program analysis: Unleashing the power of alternation. In Principles of Programming Languages (POPL), 2010. URL: https://doi.org/10.1145/1706299.1706307.
  17. Benjamin Hillery, Eric Mercer, Neha Rungta, and Suzette Person. Exact heap summaries for symbolic execution. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016. URL: https://doi.org/10.1007/978-3-662-49122-5_10.
  18. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM (CACM), 12(10), 1969. URL: https://doi.org/10.1145/363235.363259.
  19. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods Symposium (NFM), 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_4.
  20. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Principles of Programming Languages (POPL), 2015. URL: https://doi.org/10.1145/2676726.2676980.
  21. 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. Proceedings of the ACM on Programming Languages, 6(OOPSLA1), 2022. URL: https://doi.org/10.1145/3527325.
  22. Yude Lin, Tim Miller, and Harald Sondergaard. Compositional symbolic execution using fine-grained summaries. In Australasian Software Engineering Conference, 2015. URL: https://doi.org/10.1109/ASWEC.2015.32.
  23. Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, and Philippa Gardner. Gillian, part II: Real-world verification for JavaScript and C. In Computer Aided Verification (CAV), 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_38.
  24. Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. Exact separation logic (extended version), 2023. URL: https://arxiv.org/abs/2208.07200.
  25. Toby Murray, Pengbo Yan, and Gidon Ernst. Incremental vulnerability detection with insecurity separation logic, 2021. URL: https://arxiv.org/abs/2107.05225.
  26. Peter W. O'Hearn. Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL), 2019. URL: https://doi.org/10.1145/3371078.
  27. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Computer Science Logic, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  28. 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 Computer Aided Verification (CAV), 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_14.
  29. Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn. Concurrent incorrectness separation logic. Proceedings of the ACM on Programming Languages, 6(POPL), 2022. URL: https://doi.org/10.1145/3498695.
  30. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS), 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  31. Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction, Chapter 10. MIT Press, 1993. Google Scholar
  32. Greta Yorsh, Eran Yahav, and Satish Chandra. Generating precise and concise procedure summaries. In Principles of Programming Languages (POPL), 2008. URL: https://doi.org/10.1145/1328438.1328467.
  33. Noam Zilberstein, Derek Dreyer, and Alexandra Silva. Outcome logic: A unifying foundation for correctness and incorrectness reasoning. Proceedings of the ACM on Programming Languages, 7(OOPSLA1), 2023. URL: https://doi.org/10.1145/3586045.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact