Document Open Access Logo

IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL

Authors Matt Griffin , Brijesh Dongol , Azalea Raad

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.14.pdf
  • Filesize: 1.39 MB
  • 30 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
Keywords
  • Binary Analysis Platform
  • Isabelle/HOL
  • Hoare Logic
  • Incorrectness Logic

Metrics

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

Abstract

This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP’s intermediate language, called BIL and integrate it with Hoare logic (to enable proofs of correctness) as well as incorrectness logic (to enable proofs of incorrectness). IsaBIL inherits the full flexibility of BAP, allowing us to verify binaries for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), and can also be used when the source code for a binary is unavailable.
To make verification tractable, we develop a number of big-step rules that combine BIL’s existing small-step rules at different levels of abstraction to support reuse. We develop high-level reasoning rules for RISC-V instructions (our main target architecture) to further optimise verification. Additionally, we develop Isabelle proof tactics that exploit common patterns in C binaries for RISC-V to discharge large numbers of proof goals (often in the 100s) automatically. IsaBIL includes an Isabelle/ML based parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible proof environment for program binaries. As examples, we prove correctness of key examples from the Joint Strike Fighter coding standards and the MITRE database.

Cite As Get BibTex

Matt Griffin, Brijesh Dongol, and Azalea Raad. IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.14

Author Details

Matt Griffin
  • University of Surrey, Guildford, UK
  • Imperial College London, UK
Brijesh Dongol
  • University of Surrey, Guildford, UK
Azalea Raad
  • Imperial College London, UK

Funding

  • Dongol, Brijesh: Supported by VeTSS and EPSRC grants EP/X037142/1, EP/X015149/1, EP/V038915/1, and EP/R025134/2.
  • Raad, Azalea: Supported by the UKRI Future Leaders Fellowship MR/V024299/1, by the EPSRC grant EP/X037029/1 and by VeTSS.

Supplementary Materials

References

  1. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for armv8-a, risc-v, and CHERI-MIPS. Proc. ACM Program. Lang., 3(POPL):71:1-71:31, 2019. URL: https://doi.org/10.1145/3290384.
  2. Atmel. Avr instruction set manual, 2016. URL: https://ww1.microchip.com/downloads/en/devicedoc/atmel-0856-avr-instruction-set-manual.pdf.
  3. Clemens Ballarin. Locales and locale expressions in isabelle/isar. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 34-50. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_3.
  4. BAP. Bap toolkit examples, 2019. URL: https://github.com/BinaryAnalysisPlatform/bap-toolkit/blob/master/av-rule-21/descr.
  5. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. Cosmedis: A distributed social media platform with formally verified confidentiality guarantees. In SP, pages 729-748. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/SP.2017.24.
  6. A formal specification for BIL: BIL instruction language (v0.3), 2018. URL: https://github.com/BinaryAnalysisPlatform/bil/releases.
  7. Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM, volume 4085 of LNCS, pages 460-475. Springer, 2006. URL: https://doi.org/10.1007/11813040_31.
  8. David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J. Schwartz. BAP: A binary analysis platform. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, CAV, volume 6806 of LNCS, pages 463-469. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_37.
  9. Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. Constant-time foundations for the new spectre era. In Alastair F. Donaldson and Emina Torlak, editors, PLDI, pages 913-926. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385970.
  10. Kevin Cheang, Cameron Rasmussen, Sanjit A. Seshia, and Pramod Subramanyan. A formal approach to secure speculation. In CSF, pages 288-303. IEEE, 2019. URL: https://doi.org/10.1109/CSF.2019.00027.
  11. Adam Chlipala. The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In Greg Morrisett and Tarmo Uustalu, editors, ICFP, pages 391-402. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500592.
  12. M. R. Clarkson and F. B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  13. Karl Crary and Susmit Sarkar. Foundational certified code in a metalogical framework. In Franz Baader, editor, CADE, volume 2741 of Lecture Notes in Computer Science, pages 106-120. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45085-6_9.
  14. Brijesh Dongol, Matt Griffin, Andrei Popescu, and Jamie Wright. Relative security: Formally modeling and (dis)proving resilience against semantic optimization vulnerabilities. In CSF, pages 403-418. IEEE, 2024. URL: https://doi.org/10.1109/CSF61375.2024.00027.
  15. Chelsea Edmonds and Lawrence C. Paulson. Formal probabilistic methods for combinatorial structures using the lovász local lemma. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, CPP, pages 132-146. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636946.
  16. Anthony C. J. Fox. Formal specification and verification of ARM6. In David A. Basin and Burkhart Wolff, editors, TPHOLs, volume 2758 of Lecture Notes in Computer Science, pages 25-40. Springer, 2003. URL: https://doi.org/10.1007/10930755_2.
  17. Anthony C. J. Fox and Magnus O. Myreen. A trustworthy monadic formalization of the armv7 instruction set architecture. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 243-258. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_18.
  18. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying strong eventual consistency in distributed systems. CoRR, abs/1707.01747, 2017. URL: https://arxiv.org/abs/1707.01747.
  19. Matt Griffin and Brijesh Dongol. Verifying secure speculation in Isabelle/HOL. In Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan, editors, FM, volume 13047 of LNCS, pages 43-60. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-90870-6_3.
  20. Matt Griffin, Brijesh Dongol, and Azalea Raad. Isabelle/HOL files for "IsaBIL: A framework for verifying (in)correctness of binaries in Isabelle/HOL", 2025. URL: https://doi.org/10.5281/zenodo.15261359.
  21. Matt Griffin, Brijesh Dongol, and Azalea Raad. IsaBIL: A framework for verifying (in)correctness of binaries in Isabelle/HOL (Extended version), 2025. URL: https://arxiv.org/abs/2504.16775.
  22. Kevin W. Hamlen, Dakota Fisher, and Gilmore R. Lundquist. Source-free machine-checked validation of native code in coq. In FEAST, FEAST'19, pages 25-30, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3338502.3359759.
  23. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  24. Graham Hutton. Book review: Introduction to HOL: A theorem proving environment for higher order logic by mike gordon and tom melham (eds.), cambridge university press, 1993, ISBN 0-521-44189-7. J. Funct. Program., 4(4):557-559, 1994. URL: https://doi.org/10.1017/S0956796800001180.
  25. Jonas Braband Jensen, Nick Benton, and Andrew Kennedy. High-level separation logic for low-level code. In Roberto Giacobazzi and Radhia Cousot, editors, POPL, pages 301-314. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429105.
  26. Florian Kammüller and Manfred Kerber. Investigating airplane safety and security against insider threats using logical modeling. In SP, pages 304-313. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/SPW.2016.47.
  27. Florian Kammüller, Markus Wenzel, and Lawrence C Paulson. Locales a sectioning concept for isabelle. In TPHOLs, pages 149-165. Springer, 1999. URL: https://doi.org/10.1007/3-540-48256-3_11.
  28. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. Cakeml: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, POPL, pages 179-192. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  29. Kait Lam and Nicholas Coughlin. Lift-off: Trustworthy armv8 semantics from formal specifications. In Alexander Nadel and Kristin Yvonne Rozier, editors, FMCAD, pages 274-283. IEEE, 2023. URL: https://doi.org/10.34727/2023/ISBN.978-3-85448-060-0_36.
  30. Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, POPL, pages 42-54. ACM, 2006. URL: https://doi.org/10.1145/1111037.1111042.
  31. Xavier Leroy and Sandrine Blazy. Formal verification of a c-like memory model and its uses for verifying program transformations. J. Autom. Reason., 41(1):1-31, 2008. URL: https://doi.org/10.1007/s10817-008-9099-0.
  32. Lockheed Martin. Joint strike fighter, air vehicle, c++ coding standard, 2005. Google Scholar
  33. Daniel Matichuk, Toby C. Murray, and Makarius Wenzel. Eisbach: A proof method language for isabelle. J. Autom. Reason., 56(3):261-282, 2016. URL: https://doi.org/10.1007/s10817-015-9360-2.
  34. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. Exploring C semantics and pointer provenance. Proc. ACM Program. Lang., 3(POPL):67:1-67:32, 2019. URL: https://doi.org/10.1145/3290380.
  35. Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan. Rocksalt: better, faster, stronger SFI for the x86. In Jan Vitek, Haibo Lin, and Frank Tip, editors, PLDI, pages 395-404. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254111.
  36. Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In ASE, pages 1186-1189. IEEE, 2019. URL: https://doi.org/10.1109/ASE.2019.00133.
  37. Magnus O. Myreen, Anthony C. J. Fox, and Michael J. C. Gordon. Hoare logic for ARM machine code. In Farhad Arbab and Marjan Sirjani, editors, FSEN, volume 4767 of LNCS, pages 272-286. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75698-9_18.
  38. Magnus O. Myreen and Michael J. C. Gordon. Hoare logic for realistically modelled machine code. In Orna Grumberg and Michael Huth, editors, TACAS, volume 4424 of LNCS, pages 568-582. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71209-1_44.
  39. Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. Machine-code verification for multiple architectures - an application of decompilation into logic. In Alessandro Cimatti and Robert B. Jones, editors, FMCAD, pages 1-8. IEEE, 2008. URL: https://doi.org/10.1109/FMCAD.2008.ECP.24.
  40. Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. Decompilation into logic - improved. In Gianpiero Cabodi and Satnam Singh, editors, FMCAD, pages 78-81. IEEE, 2012. URL: https://ieeexplore.ieee.org/document/6462558/.
  41. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  42. Peter W. O'Hearn. Incorrectness logic. POPL, 4(POPL):1-32, 2019. URL: https://doi.org/10.1145/3371078.
  43. 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.
  44. Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. Islaris: verification of machine code against authoritative ISA semantics. In Ranjit Jhala and Isil Dillig, editors, PLDI, pages 825-840. ACM, 2022. URL: https://doi.org/10.1145/3519939.3523434.
  45. Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In Hans-Juergen Boehm and Cormac Flanagan, editors, PLDI, pages 471-482. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462183.
  46. Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In IEEE SP, 2016. Google Scholar
  47. Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, and Peter Sewell. Relaxed virtual memory in armv8-a. In Ilya Sergey, editor, ESOP, volume 13240 of LNCS, pages 143-173. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_6.
  48. Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. Armv8-a system semantics: Instruction fetch in relaxed architectures. In Peter Müller, editor, ESOP, volume 12075 of LNCS, pages 626-655. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_23.
  49. Romain Thomas. Lief - library to instrument executable formats. https://lief.quarkslab.com, April 2017.
  50. Christian Urban. The Isabelle cookbook: A gentle tutorial for programming Isabelle, 2019. Google Scholar
  51. Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, and Binoy Ravindran. Formally verified lifting of c-compiled x86-64 binaries. In Ranjit Jhala and Isil Dillig, editors, PLDI, pages 934-949. ACM, 2022. URL: https://doi.org/10.1145/3519939.3523702.
  52. Fish Wang and Yan Shoshitaishvili. Angr - the next generation of binary analysis. In IEEE SecDev, pages 8-9. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/SecDev.2017.14.
  53. Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. oo7: Low-overhead defense against spectre attacks via program analysis. IEEE Trans. Software Eng., 47(11):2504-2519, 2021. URL: https://doi.org/10.1109/TSE.2019.2953709.
  54. Mark Wassell, Alasdair Armstrong, Neel Krishnaswami, and Peter Sewell. Mechanised metatheory for the sail isa specification, 2018. Google Scholar
  55. Andrew Waterman, Yunsup Lee, David A. Patterson, and Krste Asanović. The RISC-V instruction set manual, volume i: User-level isa, version 2.0. Technical Report UCB/EECS-2014-54, University of California, Berkeley, 2014. URL: http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-54.html.
  56. Lu Zhao, Guodong Li, Bjorn De Sutter, and John Regehr. Armor: fully verified software fault isolation. In Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah, and Sebastian Fischmeister, editors, EMSOFT, pages 289-298. ACM, 2011. URL: https://doi.org/10.1145/2038642.2038687.
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