2019/01/04 by Ian Roessle, Freek Verbeek, Binoy Ravindran · 1 voice
Computer Science · #Advanced Malware Detection Techniques #Distributed systems and fault tolerance #Security and Verification in Computing
paper · doi:10.1145/3293880.3294102
openalex publication_date 2019/01/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.