SaTC: CORE: Small: Precise and Robust Binary Reverse Engineering and its Applications

Analyzing untrusted computer programs to detect malicious behavior is of paramount importance to computer security. Many programs running in computer systems do not come with their source code and are only available in an executable form, called binary programs . Analyzing binary programs directly is critical to preventing malware, which continues to disrupt the functioning of modern societies. This project presents crosscutting research, educational opportunities, and an outreach plan to improve the accuracy, robustness, and scalability of binary program analysis and has the potential of fundamentally enhancing the ability of understanding and preventing malware.The core of this project's binary-analysis framework has two novel techniques: (1) a new pointer analysis technique based on a memory model called the block memory model and (2) an implementation of the core analysis as rules in a declarative language called Datalog that can be efficiently solved. This project will have three tasks based on these techniques. (1) In Task A the project will produce a comprehensive framework called Blockbin, which can produce precise reverse-engineering information of an input binary program. The framework will handle binary programs that are produced from different source languages that are for different architectures, and that have been obfuscated. (2) Task B will focus on demonstrating the utility of Blockbin through a diverse set of applications from program hardening to authorship attribution and to malware analysis. (3) Task C will focus on improving the scalability of Blockbin by designing a highly parallel Datalog solver with support for lattice-based static analysis. The result will be a tool that generates high-precision reverse-engineering information for sophisticated binaries and a demonstration of the tool's utility in a diverse set of applications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.