SaTC: CORE: Small: MOSE: Automated Detection of Module-Specific Semantic Errors

操作系统内核、库和应用程序框架等系统软件为计算设备（从个人计算机和服务器到移动设备和嵌入式设备）的所有功能提供了基础。系统软件中的安全漏洞尤其严重，因为它们可以破坏设备上运行的任何软件。系统软件中最常见的漏洞是语义错误，例如缺少安全检查。如果成功利用语义错误，可能导致严重的系统攻击，如特权升级、远程代码执行和信息泄漏。例如，易受攻击的设备可能处于攻击者的完全控制之下，并泄露用户的私人信息。尽管这一点很重要，但是检测语义错误是一项挑战，因为语义错误没有统一的模式，而且经常涉及复杂的代码逻辑。以往的语义错误检测研究主要采用统计分析或手工规范的方法来建立语义检查规则，往往忽略了模块特定的语义错误，这些语义错误涉及到各种功能和变量，每个功能和变量都只有很少的用途。本项目旨在通过开发识别模块特定函数和变量的自动化技术，并生成具体的检查规则，自动检测系统软件中特定模块的语义错误。该项目还将开发一种新的检测系统，以精确检测模块特定的语义错误。通过自动检测广泛使用的系统软件中常见的语义错误类别，本项目显著提高了普适计算机设备的安全性。该项目的更广泛的教育活动包括将研究与外展相结合，在明尼苏达州的大学和行业之间组织“夺旗”比赛，以及开发新的跨学科课程。本研究项目旨在检测特定于模块的语义错误，这是一种新的、广泛的语义错误类别，以前的检测采用统计分析或人工规范生成规则进行语义检查，否则无法检测。首先，它开发了新的技术来自动识别与安全相关的函数和变量，而不需要多次使用它们。这些技术包括错误代码分析、使用分析和行为分析。其次，对已识别的函数和变量进行实证分析，并根据其安全属性和上下文对其进行分类。对于每个类别，研究进一步开发了元规则，指定如何正确使用每个类别。例如，如果将变量用作内存分配的大小参数，则应该强制执行范围检查。元规则是通用的，可以组装和实例化，为每个模块特定的函数或变量生成具体的检查规则。第三，该项目开发了一种分阶段的方法和一套静态分析和符号执行技术，以精确地检测系统软件中以前未知的特定模块的语义错误。这些技术可以在广泛使用的系统软件（如Linux内核）上进行评估。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

System software such as operating system kernels, libraries, and application frameworks provide the foundation for all of the functionality of computing devices, from personal computers and servers to mobile and embedded devices. Security vulnerabilities in system software are particularly serious because they can undermine any of the software running on a device. The most common vulnerabilities in system software are semantic errors such as missing security checks. Semantic errors, if exploited successfully, can result in critical system attacks such as privilege escalation, remote code execution, and information leaks. For instance, vulnerable devices might come under the complete control of an adversary and reveal users' private information. Despite this importance, detecting semantic errors is challenging because semantic errors do not have uniform patterns and often involve complicated code logic. Previous research on detecting semantic errors mainly employs statistical analysis or manual specification to create rules for semantic checking, and often misses module-specific semantic errors involving the diverse functions and variables that each has only a few uses. This project aims to automatically detect such module-specific semantic errors in system software by developing automated techniques for identifying module-specific functions and variables, and generating concrete checking rules. This project will also develop a novel detection system to precisely detect module-specific semantic errors. By automatically detecting classes of common semantic errors in widely used system software, this project significantly improves the security of ubiquitous computer devices. The broader educational activities of this project include integrating research with outreach, organizing Capture The Flag competitions among universities and industries in Minnesota, and developing new interdisciplinary courses.This research project aims to detect module-specific semantic errors, a new and wide class of semantic error, which have been otherwise missed by previous detection that employs statistical analysis or manual specification to generate rules for semantic checking. First, it develops novel techniques to automatically identify security-related functions and variables, without requiring multiple uses of them. These techniques include error-code analysis, usage analysis, and behavior analysis. Second, it empirically analyzes identified functions and variables, and categorizes them based on their security properties and contexts. For each category, the research further develops meta-rules specifying how each category should be correctly used. For example, a range check should be enforced if a variable is used as a size parameter of memory allocation. Meta-rules are general, and can be assembled and instantiated to generate concrete checking rules for each module-specific function or variable. Third, the project develops a staged approach and a set of static analysis and symbolic execution techniques to precisely detect previously unknown module-specific semantic errors at scale for system software. These techniques can be evaluated on widely used system software such as the Linux kernel.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.