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.

JNI programs are widely used thanks to the combined benefits of C and Java programs. However, because understanding the interaction behaviors between two different programming languages is challenging, JNI program development is difficult to get right and vulnerable to security attacks. Thus, researchers have proposed static analysis of JNI program source code to detect bugs and security vulnerabilities in JNI programs. Unfortunately, such source code analysis is not applicable to compiled JNI programs that are not open-sourced or open-source JNI programs containing third-party binary libraries. While JN-SAF, the state-of-the-art analyzer for compiled JNI programs, can analyze binary code, it has several limitations due to its symbolic execution and summary-based bottom-up analysis. In this paper, we propose a novel approach to statically analyze compiled JNI programs without their source code using binary decompilation. Unlike JN-SAF that analyzes binaries directly, our approach decompiles binaries and analyzes JNI programs with the decompiled binaries using an existing JNI program analyzer for source code. To decompile binaries to compilable C source code with precise JNI-interoperation-related types, we improve an existing decompilation tool by leveraging the characteristics of JNI programs. Our evaluation shows that the approach is precise as almost the same as the state-of-the-art JNI program analyzer for source code, and more precise than JN-SAF.

JavaScript was initially designed for client-side programming in web browsers, but its engine is now embedded in various kinds of host software. Despite the popularity, since the JavaScript semantics is complex especially due to its dynamic nature, understanding and reasoning about JavaScript programs are challenging tasks. Thus, researchers have proposed several attempts to define the formal semantics of JavaScript based on ECMAScript, the official JavaScript specification. However, the existing approaches are manual, labor-intensive, and error-prone and all of their formal semantics target ECMAScript 5.1 (ES5.1, 2011) or its former versions. Therefore, they are not suitable for understanding modern JavaScript language features introduced since ECMAScript 6 (ES6, 2015). Moreover, ECMAScript has been annually updated since ES6, which already made five releases after ES5.1.