Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation

Explore a 14-minute conference presentation from OOPSLA 2025 that introduces a novel approach to binary lifting correctness verification. Learn how researchers from KAIST address the fundamental challenge of bridging formally verified binary lifters with real-world implementations that rely on heuristic-based assumptions. Discover the concept of filtered-simulation, a variant of bi-simulation, used to define correctness between programs before and after transformation in binary lifting processes. Examine three essential transformations formalized in this research: control flow graph reconstruction, abstract stack reconstruction, and function input/output identification. Understand how the FIBLE implementation demonstrates successful lifting of Coreutils and CGC datasets compiled with GCC for x86-64 Linux binaries. Gain insights into how this work formalizes the binary lifting process by dividing it into a series of transformations, each representing a lift with new abstraction features, making it possible to guarantee correctness while accommodating the practical requirements of real-world binary analysis tools.