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

SaTC：核心：小：MOSE：模块特定语义错误的自动检测

• 批准号: 1815621
• 负责人: Kangjie Lu
• 金额: $ 49.53万
• 依托单位: University of Minnesota-Twin Cities
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-09-01 至 2021-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1815621&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; MOSE; Automated

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.

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

项目成果

Detecting Missed Security Operations Through Differential Checking of Object-based Similar Paths

• DOI: 10.1145/3460120.3485373
• 发表时间: 2021-11
• 期刊: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
• 作者: Dinghao Liu;Qiushi Wu;S. Ji;Kangjie Lu;Zhenguang Liu;Jianhai Chen;Qinming He

Detecting Kernel Memory Leaks in Specialized Modules with Ownership Reasoning

• DOI: 10.14722/ndss.2021.24416
• 发表时间: 2021
• 期刊: Proceedings 2021 Network and Distributed System Security Symposium
• 作者: Navid Emamdoost

Detecting missing-check bugs via semantic- and context-aware criticalness and constraints inferences

通过语义和上下文感知的关键性和约束推断来检测遗漏检查错误

• DOI: 10.5555/3361338.3361461
• 发表时间: 2019
• 期刊: Proceedings of the 28th USENIX Conference on Security Symposium
• 作者: Lu, Kangjie Lu;Pakki, Aditya;Wu, Qiushi
• 通讯作者: Wu, Qiushi

Automatically Identifying Security Checks for Detecting Kernel Semantic Bugs

• DOI: 10.1007/978-3-030-29962-0_1
• 发表时间: 2019-09
• 作者: Kangjie Lu;Aditya Pakki;Qiushi Wu

On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic Execution

论PHP符号执行的自动内置函数建模的可行性

• DOI: 10.1145/3442381.3450002
• 发表时间: 2021
• 期刊: the 30th International World Wide Web Conference (WWW'21
• 作者: Li, Penghui;Meng, Wei;Lu, Kangjie;Luo, Changhua
• 通讯作者: Luo, Changhua