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

University Of Minnesota-Twin Cities, Minneapolis MN

Investigators

Abstract

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.