Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification

Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, Hamed Nemati

TL;DR

The paper tackles the difficulty of reasoning about unstructured control flow in binary code for trustworthy verification. It develops a general theory of forward symbolic execution built from sound inference rules and instantiates it to the BIR intermediate language, with machine-checked soundness proofs in HOL4. The authors implement the theory in HolBA-SE and demonstrate automated verification of functional properties for RISC-V binaries and execution-time bounds for Cortex-M0, achieving moderate overhead for medium-sized programs. By combining ISA-independent lifting, contract automation, and precise timing analysis, the work enables scalable, provably correct binary verification suitable for cryptographic and low-level system code. The practical impact includes a reusable theorem-prover framework, proof-producing executors, and a set of case studies illustrating translation validation and WCET analysis that complement industrial tools like aiT while offering stronger formal guarantees.

Abstract

Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory's foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification

TL;DR

The paper tackles the difficulty of reasoning about unstructured control flow in binary code for trustworthy verification. It develops a general theory of forward symbolic execution built from sound inference rules and instantiates it to the BIR intermediate language, with machine-checked soundness proofs in HOL4. The authors implement the theory in HolBA-SE and demonstrate automated verification of functional properties for RISC-V binaries and execution-time bounds for Cortex-M0, achieving moderate overhead for medium-sized programs. By combining ISA-independent lifting, contract automation, and precise timing analysis, the work enables scalable, provably correct binary verification suitable for cryptographic and low-level system code. The practical impact includes a reusable theorem-prover framework, proof-producing executors, and a set of case studies illustrating translation validation and WCET analysis that complement industrial tools like aiT while offering stronger formal guarantees.

Abstract

Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory's foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.
Paper Structure (23 sections, 2 theorems, 7 equations, 7 figures, 2 tables)

This paper contains 23 sections, 2 theorems, 7 equations, 7 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. The BIR language
  4. Running example
  5. Challenges and approach
  6. Symbolic Semantics
  7. Symbolic Execution
  8. Progress structures
  9. Inference rules
  10. Symbolic execution example
  11. Implementation
  12. Results formalized and proved in HOL4
  13. Symbolic executors and progress structures in HolBA-SE
  14. Practical evaluation of symbolic execution using HolBA-SE
  15. Application: Automated Verification of Functional Properties of RISC-V Binaries
  16. ...and 8 more sections

Key Result

theorem thmcountertheorem

If $\overline{s} \mathrel{\stackrel{\hbox{\normalfont\tiny H}}{\triangleright}} s$ and ${s} \rightarrow {s'}$, then exists $\overline{s}' \in \mathit{symsem}({\overline{s}})$ such that $\overline{s}' \mathrel{\stackrel{\hbox{\normalfont\tiny H}}{\triangleright}} s'$.

Figures (7)

  • Figure 1: ModExp pseudocode.
  • Figure 2: BIR CFG of ModExp.
  • Figure 3: Overview of the symbolic-execution core inference-rules, part 1.
  • Figure 4: Overview of the symbolic-execution core inference-rules, part 2.
  • Figure 5: Architecture of HolBA, a HOL4-based binary analysis library. Components and outputs relevant to HolBA-SE are highlighted.
  • ...and 2 more figures

Theorems & Definitions (6)

  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • theorem thmcountertheorem