Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
Aaron Bembenek (1), Toby Murray (1) ((1) The University of Melbourne)

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):…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
