一句话：提出形式化证明正确的二进制级指针分析，并用通用抽象域证明义务支持不同精度实例化。
二进制级指针分析可用于符号执行、测试、验证与反编译等任务，但结果必须可信，即指针指向关系应是可形式化证明的过近似。本文提出一种形式化证明正确的二进制级指针分析方法。其核心贡献是先通用地刻画指针分析抽象域必须满足的证明义务，从而让不同精度的抽象域都能在保持分析正确性的前提下方便实例化。作者实现并比较了高、中、低三种精度的抽象域，在真实商用现货（COTS）二进制上评估，能够以上下文敏感的过程间方式可靠地推导内存写操作的指向关系；当指针计算因编译混淆而难以精确分析时，也可退化为较粗粒度分析，以折中可扩展性与精度。
Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the result is trustworthy, i.e., it can be formally established that the pointer designations are overapproximative. This paper presents an approach to formally proven correct binary-level pointer analysis. A salient property of our approach is that it first generically considers what proof obligations a generic abstract domain for pointer analysis must satisfy. This allows easy instantiation of different domains, varying in precision, while preserving the correctness of the analysis. In the trade-off between scalability and precision, such customization allows “meaningful” precision (sufficiently precise to ensure basic sanity properties, such as that relevant parts of the stack frame are not overwritten during function execution) while also allowing coarse analysis when pointer computations have become too obfuscated during compilation for sound and accurate bounds analysis. We experiment with three different abstract domains with high, medium, and low precision. Evaluation shows that our approach is able to derive designations for memory writes soundly in COTS binaries, in a context-sensitive interprocedural fashion.
DOI 原文 ·
@inproceedings{paperbot8883,
title = {Formally Verified Binary-Level Pointer Analysis},
author = {Freek Verbeek and Ali Shokri and Daniel Engel and Binoy Ravindran},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00231}
}