SaTC: CORE: Small: Reasoning about dependencies and information flow in dynamic code

该项目旨在调查代码在执行过程中可能发生变化的软件。这样的代码在现代系统中随处可见。例如，所有现代Web浏览器都包含一个称为JIT编译器的组件，它可以在执行期间创建或修改代码。对执行运行时修改的代码和作为结果创建或修改的代码之间的关系进行推理对于许多软件安全应用程序来说是重要的。例如，JIT编译器中的错误可能会导致可被黑客利用的漏洞。目前，这种推理是人工进行的。由于使用在执行期间创建或修改的代码的软件的规模和复杂性，这种手动推理是困难的、缓慢的、乏味的，并且容易出错。该项目旨在开发概念、技术和工具来自动化这一过程，并使其更快、更容易地推理和理解这类软件的行为。该项目的潜在好处包括提高软件安全性和培训本科生和研究生，包括未被充分代表的少数民族的成员。该项目将专注于开发概念、技术和算法，用于推理可以在运行时创建或修改的代码(动态代码)，这些代码不是基于特定技术或实现构件的，并将清楚地阐述任何潜在的假设。它的研究活动将集中在以下主题上：(1)识别动态代码的计算结构的合适表示，以便能够推理端到端信息流，即执行动态代码修改的代码和结果被修改的代码之间的信息流；(2)识别适当的依赖概念，以充分捕获动态代码中的端到端信息流；扩展为静态代码开发的分析，以自然的方式处理动态代码。(3)对这些想法进行评估，以确定它们在实际应用中的效果如何，例如JIT编译器中的错误本地化。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

This project aims to investigate software whose code can change during its execution. Such code is ubiquitous in modern systems. For example, all modern web browsers contain a component, known as a JIT compiler, that creates or modifies code during execution. Reasoning about relationships between the code that carries out the runtime modifications, and the code that is created or modified as a result, is important for a number of software security applications. For example, bugs in a JIT compiler can result in vulnerabilities that can be exploited by hackers. Currently, such reasoning is performed manually. Because of the size and complexity of software that uses code that is created or modified during execution, such manual reasoning is difficult, slow, tedious, and error-prone. This project aims to develop concepts, techniques, and tools to automate this process and make it faster and easier to reason about and understand the behavior of such software. Potential benefits of the project include improved software security and training undergraduate and graduate students, including members of underrepresented minorities, in advanced research techniques.The project will focus on developing concepts, techniques, and algorithms for reasoning about code that can be created or modified at runtime ("dynamic code") that are not predicated on specific technologies or implementation artifacts, and will articulate clearly any underlying assumptions. Its research activities will focus on the following topics: (1) identification of suitable representations for the computational structure of dynamic code so as to make it possible to reason about end-to-end information flow, i.e.,information flow between the code that performs dynamic code modification and the code that is modified as a result; (2) identification of appropriate notions of dependency that can adequately capture end-to-end information flow in dynamic code; extension of analyses developed for static code to work on dynamic code in a natural way. (3) the evaluation of these ideas to determine how well they work in practice in the context of real-world applications such as bug localization in JIT compilers.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.