Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving

TL;DR

This paper demonstrates that encoding binary analysis as bit-vector CHCs and solving them with existing tools is feasible and yields comparable success rates to source-level verification, while also providing valuable new benchmarks.

Contribution

It introduces a pipeline for encoding binary analysis problems as bit-vector CHCs and evaluates their solvability with existing solvers, highlighting the potential for improved binary verification.

Findings

CHC solvers solve 59.5% and 66.1% of binary problems from benchmarks.

Binary-derived CHC problems differ structurally from existing benchmarks.

Binary analysis can generate valuable new benchmarks for CHC solver development.

Abstract

For high-assurance software, source-level reasoning is insufficient: we need binary-level guarantees. Despite constrained Horn clause (CHC) solving being one of the most popular forms of automated verification, prior work has not evaluated the viability of CHC solving for binary analysis. To fill this gap, we assemble a pipeline that encodes binary analysis problems as CHCs in the SMT logic of quantifier-free bit vectors, and show that off-the-shelf CHC solvers achieve reasonable success on binaries compiled from 983 C invariant inference benchmarks: a portfolio solves 59.5% and 66.1% of the problems derived from the unoptimized and optimized binaries, respectively -- roughly equal to the success rate of a leading C verifier on the source code (60.1%). Moreover, we show that binary analysis provides a valuable source of bit-vector CHC benchmarks (which are in short supply): binary-derived problems differ from existing benchmarks both structurally and in solver success rates and rankings. Augmenting CHC solving competitions with binary-derived benchmarks will encourage solver developers to improve bit-vector reasoning, in turn making CHC solving a more effective tool for binary analysis.