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.

翻译：对于高置信度软件而言，源码级推理是不够的：我们需要二进制级保障。尽管约束Horn子句（CHC）求解是最流行的自动化验证形式之一，但此前研究尚未评估CHC求解在二进制分析中的可行性。为填补这一空白，我们构建了一个流程，将二进制分析问题编码为无量词位向量SMT逻辑中的CHC，并表明现成的CHC求解器在编译自983个C语言不变量推断基准测试的二进制程序上取得了合理成功：一个求解器组合分别解决了来自未优化和优化二进制程序的59.5%和66.1%的问题——这大致相当于领先C语言验证器在源码上的成功率（60.1%）。此外，我们表明二进制分析为位向量CHC基准测试（目前稀缺）提供了宝贵来源：二进制衍生问题在结构、求解器成功率和排名上与现有基准测试均存在差异。将二进制衍生基准测试纳入CHC求解竞赛将鼓励求解器开发者改进位向量推理，进而使CHC求解成为二进制分析中更有效的工具。