EAGER: Finding Semantic Security Bugs with Pseudo-Oracle Testing

语义安全漏洞会在广泛的软件中造成严重的漏洞。例如，在最近的一次事件中，攻击者利用Apache Struts中的语义安全漏洞从Equifax服务器上窃取了多达1.43亿客户的敏感个人数据。事实上，这种脆弱性在实践中相当普遍。仅今年一年，分配给不同类型语义安全错误的常见漏洞和暴露标识符（CVE）总数就超过了2,000个。该项目的目标是通过自动检测关键软件中的语义漏洞来提高安全性和可靠性。自动检测这些bug很难，因为与崩溃bug不同，它们可能不会显示任何明显的副作用。相反，语义安全漏洞（例如，绕过安全检查、获得对敏感信息的访问、提升特权）通常是由于违反高级安全/安保规范而导致的，而这些规范在实践中很少被正式编写。这个项目将研究学习特定领域的变形关系是否有助于检测语义错误。 在软件工程中，将程序的多次执行的输出与不同的输入相关联的变形关系已被证明在发现简单的功能错误方面是有效的。虽然变形关系有希望检测语义安全漏洞，但它们无法检测其当前形式的语义安全漏洞，因为安全属性不能表示为简单的基于输入-输出的属性。该方法使用伪预言机测试技术，如差分测试和变形测试。该项目将使用有针对性的路径探索技术，以及自动学习算法来发现变形测试规则。该项目将学习如何增强变形关系的语义以检测语义安全漏洞。该研究设想了一个基于伪随机预言机的统一框架，它可以自动检测语义安全漏洞，而不需要手动创建形式化规范来比较相关执行的程序行为。作为第一步，EAGER项目的目标是以经验为基础，衡量是否有一个全面的语义表达的伪预言关系，可以检测语义安全漏洞。这个奖项反映了NSF的法定使命，并已被认为是值得支持的，通过评估使用基金会的智力价值和更广泛的影响审查标准。

Semantic security bugs cause serious vulnerabilities across a wide range of software. For example, in a recent incident, attackers exploited a semantic security bug in Apache Struts to steal sensitive personal data of up to 143 million customers from Equifax servers. In fact, such vulnerabilities are quite common in practice. The total number of Common Vulnerabilities and Exposure Identifiers (CVEs) assigned to different types of semantic security bugs exceeds 2,000 just this year alone. The goal of this project is to improve security and reliability by automatically detecting such semantic vulnerabilities in critical software. Automatically detecting these bugs is hard because unlike crash bugs they may not show any obvious side effects. In contrast, semantic security bugs (e.g., bypassing security checks, gaining access to sensitive information, escalating privileges) usually result from violation of high-level safety/security specifications which, in practice, are rarely written formally. This project will investigate whether learning domain-specific metamorphic relations can help in detecting semantic bugs. In Software Engineering, metamorphic relations, which correlate outputs from multiple executions of a program with different inputs, have been shown to be effective at finding simple functional bugs. While metamorphic relations have promise to detect semantic security vulnerabilities, they are not able to detect semantic security vulnerabilities in their current form, as security properties cannot be expressed as simple input-output based properties. The approach uses pseudo-oracle testing techniques like differential testing and metamorphic testing. The project will use targeted path exploration techniques, with automata-learning algorithms to discover metamorphic testing rules. The project will learn how the semantics of metamorphic relations can be augmented to detect semantic security bugs. The research envisions a unified framework based on pseudo-random Oracles, which can automatically detect semantic security bugs without the need for manually creating formal specifications to compare program behaviors of related executions. As a first step, the objective of this EAGER project is to empirically measure whether there is a comprehensive range of semantically expressive pseudo-oracle relations that can detect semantic security vulnerabilities.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.