Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA

TL;DR

This paper tackles the challenge of trustworthy verification for RISC-V binaries by bridging the gap between high-level formal proofs and runtime machine-code behavior. It introduces a HOL4/HolBA-based toolchain that lifts RV64G binaries to the BIR intermediate language, performs proof-producing forward symbolic execution, and backloops results to obtain RISC-V contracts. The approach is validated with two case studies: ChaCha20 and a hand-written kernel routine from the S3K separation kernel, demonstrating applicability to cryptography and operating-system components. The authors also evaluate scalability of symbolic execution on large binaries and release an open-source framework, outlining future work to automate contract translations and broaden interface accessibility.

Abstract

Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be narrowed by techniques such as refinement, a verified program's trusted computing base may still include compilers and inlined assembly. In contrast, verification of binaries following an Instruction Set Architecture (ISA) such as RISC-V can ensure that machine code behaves as expected on real hardware. While binary analysis is useful and sometimes even necessary for ensuring trustworthiness of software systems, existing tools do not have a formal foundation or lack automation for verification. We present a workflow and toolchain based on the HOL4 theorem prover and the HolBA binary analysis library for trustworthy formal verification of RISC-V binaries. The toolchain automates proofs of binary contracts by forward symbolic execution of programs in HolBA's intermediate language, BIR. We validated our toolchain by verifying correctness of RISC-V binaries with (1) an implementation of the ChaCha20 stream cipher and (2) hand-written assembly for context switching in an operating system kernel.

Figures (7)

• Figure 1: Binary analysis tool architecture centering on an intermediate language (IL).
• Figure 2: Binary analysis workflow using HOL4 and HolBA.
• Figure 3: Example program that increments a 64-bit unsigned integer represented in C (top), corresponding RISC-V disassembly (middle) and BIR abstract syntax (bottom).
• Figure 4: Pre- and postconditions and theorems for program in Figure \ref{['fig:ex-prog']}.
• Figure 5: Architecture of HolBA, a theorem-prover-based binary analysis platform. The figure illustrates HolBA's modular design, highlighting key components.