EAGER: Finding Semantic Security Bugs with Pseudo-Oracle Testing

语义安全漏洞会在各种软件中造成严重的漏洞。例如，在最近的一起事件中，攻击者利用Apache Struts中的语义安全漏洞从Equifax服务器窃取了多达1.43亿客户的敏感个人数据。事实上，这种漏洞在实践中相当常见。仅今年一年，分配给不同类型语义安全漏洞的常见漏洞和暴露标识符(CVE)总数就超过了2000个。该项目的目标是通过自动检测关键软件中的此类语义漏洞来提高安全性和可靠性。自动检测这些错误是很困难的，因为与崩溃错误不同，它们可能不会显示任何明显的副作用。相比之下，语义安全错误(例如，绕过安全检查、访问敏感信息、提升权限)通常是由于违反高级安全/安全规范造成的，而在实践中，这些规范很少是正式编写的。这个项目将调查学习特定于领域的变形关系是否有助于检测语义错误。在软件工程中，变形关系已经被证明在寻找简单的功能错误方面是有效的，它将来自具有不同输入的程序的多次执行的输出关联起来。虽然变形关系有望检测语义安全漏洞，但它们不能检测当前形式的语义安全漏洞，因为安全属性不能表示为简单的基于输入-输出的属性。该方法使用了差异测试和变形测试等伪先知测试技术。该项目将使用有针对性的路径探索技术，并使用自动机学习算法来发现变形测试规则。该项目将学习如何增强变形关系的语义以检测语义安全错误。该研究设想了一个基于伪随机预言的统一框架，它可以自动检测语义安全漏洞，而不需要手动创建形式化规范来比较相关执行的程序行为。作为第一步，这个渴望项目的目标是经验性地衡量是否存在一系列全面的语义表达的伪先知关系，可以检测到语义安全漏洞。这一奖项反映了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.