Bridging the Gap: Specification Inference for Automated Kernel Bug Detection

PhD Qualifying Examination


Title: "Bridging the Gap: Specification Inference for Automated Kernel Bug 
Detection"

by

Miss Wei CHEN


Abstract:

The monolithic operating system mediates interactions between user-space 
applications and hardware, playing a central role in system reliability and 
enforcing security guarantees. In recent years, the Linux kernel, which is 
widely deployed across cloud, mobile, and embedded platforms, has seen a 
growing number of vulnerability disclosures. Many of these vulnerabilities 
lead to serious consequences such as denial-of-service, information leaks, 
and remote code execution. This trend underscores the need for effective 
kernel bug detection techniques, among which static and dynamic analysis 
remain the dominant approaches in research and practice. Static analysis 
aims to reason about program properties through intermediate representations 
without executing the code, whereas dynamic analysis drives kernel execution 
via crafted inputs to uncover erroneous behaviors. However, the scale, 
complexity, and domain-specific semantics of kernel code pose significant 
obstacles for both approaches. In particular, their effectiveness is tightly 
coupled with the availability of precise and semantically meaningful 
specifications that guide the analysis. Consequently, the automated 
inference of high-quality specifications has become a central open problem 
in kernel vulnerability detection.

In this survey, we present a systematic overview of the problem, key 
challenges, and existing approaches for specification inference in the 
context of kernel bug detection. We categorize existing techniques based on 
the sources of knowledge and inference mechanisms they rely on, including 
manual engineering, mining from kernel codebases, learning from examples, 
and, more recently, leveraging large language models (LLMs). For each 
category, we analyze representative techniques in terms of their 
assumptions, inference strategies, and the types of generated 
specifications. We further discuss how prior work has evolved to improve 
specification expressiveness, increase the degree of automation, and enhance 
specification quality. This comprehensive survey aims to provide insights 
and inspire future research in this area.


Date:                   Wednesday, 10 December 2025

Time:                   10:00am - 12:00noon

Venue:                  Room 2129C
                        Lift 19

Committee Members:      Prof. Charles Zhang (Supervisor)
                        Dr. Shuai Wang (Chairperson)
                        Dr. Dongdong She
                        Dr. Wei Wang