Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Matt Griffin, Brijesh Dongol, Azalea Raad

TL;DR

IsaBIL presents a deep embedding of BIL into Isabelle/HOL to enable formal verification of binaries lifted by BAP, leveraging Hoare and Incorrectness logic. The framework uses a locale-based mechanisation to achieve modular, reusable proofs across architectures (notably RISC-V) and toolchains, with an automated parser that translates BIL outputs into Isabelle locales. It delivers large-scale verification capabilities, including a compositional analysis of a real-world double-free vulnerability in cURL (CVE-2016-8619) and coverage of JSF coding standard examples, while exposing and fixing inconsistencies in the BIL specification. The combination of big-step reasoning, automated tactic support, and compositional proof reuse yields scalable, verified analyses of binaries even when sources are unavailable, offering a practical approach to binary verification and security analysis. The work advances the state of low-level verification by integrating formal semantics, automated proof techniques, and real-world case studies within a unified Isabelle/HOL framework.

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.

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

TL;DR

IsaBIL presents a deep embedding of BIL into Isabelle/HOL to enable formal verification of binaries lifted by BAP, leveraging Hoare and Incorrectness logic. The framework uses a locale-based mechanisation to achieve modular, reusable proofs across architectures (notably RISC-V) and toolchains, with an automated parser that translates BIL outputs into Isabelle locales. It delivers large-scale verification capabilities, including a compositional analysis of a real-world double-free vulnerability in cURL (CVE-2016-8619) and coverage of JSF coding standard examples, while exposing and fixing inconsistencies in the BIL specification. The combination of big-step reasoning, automated tactic support, and compositional proof reuse yields scalable, verified analyses of binaries even when sources are unavailable, offering a practical approach to binary verification and security analysis. The work advances the state of low-level verification by integrating formal semantics, automated proof techniques, and real-world case studies within a unified Isabelle/HOL framework.

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.

Paper Structure

This paper contains 71 sections, 4 theorems, 35 equations, 16 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Scalability
  3. Contributions
  4. Supplementary material
  5. Motivation and Workflow
  6. Two C programs and their BIL representations
  7. Workflow and Mechanisation
  8. BIL Syntax and Semantics
  9. Syntax
  10. Statements
  11. Expressions
  12. Types and Values
  13. Typing Rules and Typing Context
  14. Expression Semantics
  15. IsaBIL Extensions
  16. ...and 56 more sections

Key Result

theorem 1

Let $\mathcal{C}_{bad}$ and $\mathcal{C}_{good}$ be the programs corresponding to double_free_bad and double_free_good, respectively. Both of the following hold

Figures (16)

  • Figure 1: Translation of C source programs to an Isabelle/HOL proof
  • Figure 2: Structure of IsaBIL locales: theories indicated by ${}^*$ are auto-generated from a given *.bil file following the translation in \ref{['fig:translation-c-isabelle']}.
  • Figure 3: BIL syntax and types
  • Figure 4: Reduction rules for Load
  • Figure 5: PLT stubs for free and malloc
  • ...and 11 more figures

Theorems & Definitions (10)

  • Example 3.1
  • Example 3.2
  • Example 3.3
  • Example 3.4
  • Example 4.1
  • theorem 1
  • theorem 2
  • theorem 3
  • theorem 4
  • Example G.1