Document Open Access Logo

A General Approach to Under-Approximate Reasoning About Concurrent Programs

Authors Azalea Raad , Julien Vanegue, Josh Berdine, Peter O'Hearn

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.25.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Author Details

Azalea Raad
  • Imperial College London, UK
Julien Vanegue
  • Bloomberg, New York, NY, USA
Josh Berdine
  • Skiplabs, London, UK
Peter O'Hearn
  • University College London, UK
  • Lacework, London, UK

Funding

  • Raad, Azalea: UKRI Future Leaders Fellowship under grant number MR/V024299/1

Cite AsGet BibTex

Azalea Raad, Julien Vanegue, Josh Berdine, and Peter O'Hearn. A General Approach to Under-Approximate Reasoning About Concurrent Programs. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 25:1-25:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.25

Abstract

There is a large body of work on concurrent reasoning including Rely-Guarantee (RG) and Concurrent Separation Logics. These theories are over-approximate: a proof identifies a superset of program behaviours and thus implies the absence of certain bugs. However, failure to find a proof does not imply their presence (leading to false positives in over-approximate tools). We describe a general theory of under-approximate reasoning for concurrency. Our theory incorporates ideas from Concurrent Incorrectness Separation Logic and RG based on a subset rather than a superset of interleavings. A strong motivation of our work is detecting software exploits; we do this by developing concurrent adversarial separation logic (CASL), and use CASL to detect information disclosure attacks that uncover sensitive data (e.g. passwords) and out-of-bounds attacks that corrupt data. We also illustrate our approach with classic concurrency idioms that go beyond prior under-approximate theories which we believe can inform the design of future concurrent bug detection tools.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Theory of computation → Programming logic
  • Theory of computation → Program analysis
  • Security and privacy → Logic and verification
Keywords
  • Under-approximate reasoning
  • incorrectness logic
  • bug detection
  • software exploits
  • separation logic

Metrics

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

Related Versions

References

  1. Abeer Alhuzali, Birhanu Eshete, Rigel Gjomemo, and VN Venkatakrishnan. Chainsaw: Chained automated workflow-based exploit generation. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pages 641-652, 2016. Google Scholar
  2. Thanassis Avgerinos, Sang Kil Cha, Alexandre Rebert, Edward J Schwartz, Maverick Woo, and David Brumley. Automatic exploit generation. Communications of the ACM, 57(2):74-84, 2014. Google Scholar
  3. Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. Racerd: Compositional static race detection. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276514.
  4. James Brotherston, Paul Brunet, Nikos Gorogiannis, and Max Kanovich. A compositional deadlock detector for android java. In Proceedings of ASE-36. ACM, 2021. URL: http://www0.cs.ucl.ac.uk/staff/J.Brotherston/ASE21/deadlocks.pdf.
  5. Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. Unleashing mayhem on binary code. In 2012 IEEE Symposium on Security and Privacy, pages 380-394. IEEE, 2012. Google Scholar
  6. Weiteng Chen, Xiaochen Zou, Guoren Li, and Zhiyun Qian. KOOBE: Towards facilitating exploit generation of kernel Out-Of-Bounds write vulnerabilities. In 29th USENIX Security Symposium (USENIX Security 20), pages 1093-1110, 2020. Google Scholar
  7. Facebook, 2021. URL: https://fbinfer.com/.
  8. Heartbleed. The heartbleed bug, 2014. URL: https://heartbleed.com/.
  9. Sean Heelan, Tom Melham, and Daniel Kroening. Automatic heap layout manipulation for exploitation. In 27th USENIX Security Symposium (USENIX Security 18), pages 763-779, 2018. Google Scholar
  10. Sean Heelan, Tom Melham, and Daniel Kroening. Gollum: Modular and greybox exploit generation for heap overflows in interpreters. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pages 1689-1706, 2019. Google Scholar
  11. C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596-619, October 1983. URL: https://doi.org/10.1145/69575.69577.
  12. 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 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pages 637-650, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676980.
  13. 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.
  14. Lars Müller. KPTI: A mitigation method against meltdown, 2018. URL: https://www.cs.hs-rm.de/~kaiser/events/wamos2018/Slides/mueller.pdf.
  15. Peter W. O'Hearn. Resources, concurrency and local reasoning. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, pages 49-67, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  16. 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.
  17. 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. Google Scholar
  18. Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn. Concurrent incorrectness separation logic. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498695.
  19. Azalea Raad, Julien Vanegue, Josh Berdine, and Peter O'Hearn. Technical appendix, 2023. URL: https://www.soundandcomplete.org/papers/CONCUR2023/CASL/appendix.pdf.
  20. Viktor Vafeiadis and Matthew Parkinson. A marriage of rely/guarantee and separation logic. In Luís Caires and Vasco T. Vasconcelos, editors, CONCUR 2007 - Concurrency Theory, pages 256-271, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  21. Julien Vanegue. Zero-sized heap allocations vulnerability analysis. In Proceedings of the 4th USENIX Conference on Offensive Technologies, WOOT'10, pages 1-8, USA, 2010. USENIX Association. Google Scholar
  22. Julien Vanegue. Adversarial logic. Proc. ACM Program. Lang., (SAS), December 2022. Google Scholar
  23. Wei Wu, Yueqi Chen, Jun Xu, Xinyu Xing, Xiaorui Gong, and Wei Zou. FUZE: Towards facilitating exploit generation for kernel Use-After-Free vulnerabilities. In 27th USENIX Security Symposium (USENIX Security 18), pages 781-797, 2018. Google Scholar
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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact