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.
- IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL
- Matt Griffin (Author) - University of Surrey, School of Computer Science & Electronic EngineeringBrijesh Dongol (Corresponding Author) - University of Surrey, School of Computer Science & Electronic EngineeringAzalea Raad (Corresponding Author) - Imperial College London
- 39th European Conference on Object-Oriented Programming, ECOOP 2025, Vol.333, pp.14:1-14:30
- 39th European Conference on Object-Oriented Programming (ECOOP 2025) (Bergen, Norway, 30/06/2025–04/07/2025)
- Leibniz International Proceedings in Informatics
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- 30
- 25/06/2025
- University of Surrey (United Kingdom, Guildford)Verifiably Correct Swarm Attestation, EP/V038915/1, Engineering and Physical Sciences Research Council (United Kingdom, Swindon) - EPSRCEP/R025134/2, Engineering and Physical Sciences Research Council (United Kingdom, Swindon) - EPSRCSafe and secure COncurrent programming for adVancEd aRchiTectures (COVERT), EP/X015149/1, Engineering and Physical Sciences Research Council (United Kingdom, Swindon) - EPSRCSACRED-MA: Safe And seCure REmote Direct Memory Access, EP/X037142/1, Engineering and Physical Sciences Research Council (United Kingdom, Swindon) - EPSRCEP/X037029/1, Engineering and Physical Sciences Research Council (United Kingdom, Swindon) - EPSRCMR/V024299/1, UK Research and Innovation (United Kingdom, Swindon) - UKRIResearch Institute on Verified Trustworthy Software Systems (VeTSS)
- Brijesh Dongol: Supported by VeTSS and EPSRC grants EP/X037142/1, EP/X015149/1, EP/V038915/1, and EP/R025134/2. Azalea Raad: Supported by the UKRI Future Leaders Fellowship MR/V024299/1, by the EPSRC grant EP/X037029/1 and by VeTSS.
- 991148696202346; WOS:001592262200014
- © Matt Griffin, Brijesh Dongol, and Azalea Raad; licensed under Creative Commons License CC-BY 4.0
- School of Computer Science & Electronic Engineering
- English
- Conference proceeding