一句话：提出 filtered-simulation 刻画真实二进制提升中启发式假设的正确性，并形式化三种核心变换。
真实世界的二进制提升工具常依赖启发式假设，难以用严格的形式化方法保证正确性，而已有形式验证的提升器又对输入二进制限制过强。本文提出对真实二进制提升正确性的新解释：将提升过程分解为一系列变换，每个变换引入新的抽象特征，并用 filtered-simulation（双模拟的变体）定义变换前后程序间的正确性。作者形式化了控制流图重建、抽象栈重建和函数输入/输出识别三种核心变换，并实现面向 x86-64 Linux 二进制的 fible。实验表明，fible 能正确提升用 GCC 编译的 Coreutils 和 CGC 数据集。
Binary lifting is a key component in binary analysis tools. In order to guarantee the correctness of binary lifting, researchers have proposed various formally verified lifters. However, such formally verified lifters have too strict requirements on binary, which do not sufficiently reflect real-world lifters. In addition, real-world lifters use heuristic-based assumptions to lift binary code, which makes it difficult to guarantee the correctness of the lifted code using formal methods. In this paper, we propose a new interpretation of the correctness of real-world binary lifting. We formalize the process of binary lifting with heuristic-based assumptions used in real-world lifters by dividing it into a series of transformations, where each transformation represents a lift with new abstraction features. We define the correctness of each transformation as filtered-simulation , which is a variant of bi-simulation, between programs before and after transformation. We present three essential transformations in binary lifting and formalize them: (1) control flow graph reconstruction, (2) abstract stack reconstruction, and (3) function input/output identification. We implement our approach for x86-64 Linux binaries, named fible , and demonstrate that it can correctly lift Coreutils and CGC datasets compiled with GCC.
@article{paperbot3178,
title = {Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation},
author = {Jihee Park and Insu Yun and Sukyoung Ryu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720524}
}