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

分析不可信的计算机程序以检测恶意行为对计算机安全至关重要。在计算机系统中运行的许多程序没有源代码，只能以可执行的形式提供，称为二进制程序。直接分析二进制程序对于防止恶意软件至关重要，恶意软件继续破坏现代社会的运作。该项目提出了横切研究、教育机会和扩展计划，以提高二进制程序分析的准确性、稳健性和可扩展性，并具有从根本上增强理解和预防恶意软件的能力的潜力。这个项目的二进制分析框架的核心有两种新技术：(1)一种新的指针分析技术，它基于一种叫做块内存模型的内存模型；(2)一种用一种叫做Datalog的声明性语言将核心分析作为规则实现，这种规则可以有效地求解。这个项目将有三个基于这些技术的任务。(1)在Task A中，项目将生成一个名为Blockbin的综合框架，该框架可以生成输入二进制程序的精确逆向工程信息。该框架将处理由针对不同体系结构的不同源语言生成的二进制程序，并且这些程序已被混淆。(2)任务B将侧重于通过一系列不同的应用程序来展示Blockbin的实用性，从程序强化到作者归属和恶意软件分析。(3)任务C将通过设计一个高度并行的Datalog求解器来提高Blockbin的可扩展性，并支持基于格的静态分析。结果将是一个为复杂二进制文件生成高精度逆向工程信息的工具，并演示了该工具在各种应用程序中的实用性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.