Static Program Analysis for Security in Systems Software: From OS Source to Stripped Binaries

PhD Thesis Proposal Defence


Title: "Static Program Analysis for Security in Systems Software: From OS 
Source to Stripped Binaries"

by

Mr. Chengfeng YE


Abstract:

Systems software is vital in modern computing infrastructure, and its 
security is critical, as a single defect in systems software could compromise 
the whole system. Among various program analysis techniques, static program 
analysis examines large code bases before deployment and exposes bugs that 
are hard to trigger dynamically, making it a valuable approach for uncovering 
bugs in large code bases before deployment. However, applying static analysis 
to systems software still faces two severe problems. First, the complex 
concurrency interleaving in operating systems results in a large program 
analysis reasoning space and heterogeneous security issues that were not 
modeled. Second, many security-critical systems programs, like firmware, are 
available only as stripped binaries, leading to ineffective static analysis 
due to the loss of source-level information in binaries.

To address the problems, the thesis proposal is built upon two key 
contributions. First, we propose Archerfish, the first static analysis 
approach for detecting interrupt-based deadlocks, a special kind of deadlock 
that exists in the Linux kernel and is introduced by the asymmetric 
preemption property of interrupt preemption. At its core, Archerfish 
introduces the Interrupt-Aware Lock Graph (ILG) to model both traditional and 
interrupt-based deadlocks uniformly. Furthermore, Archerfish addresses three 
core challenges to achieve both high efficiency and precision, including the 
extensive interrupt-involving concurrency space, identifying potential 
interrupt handlers, and validating the feasibility of deadlock cycles. On 
Linux kernel v6.4, Archerfish analyzes 19.8 MLoC in about one hour and 
uncovers 76 previously unknown interrupt-based deadlocks with a high 
precision of 50.3%. We wrote 37 patches to fix these bugs and sent them to 
the corresponding Linux kernel subsystem developers, resulting in 46 bugs 
being fixed and 2 CVE IDs assigned.

Second, we propose Manta, a hybrid-sensitive type inference method to address 
the problem that a single-sensitivity analysis either produces overly 
over-approximated inference results or loses the hint to recover some 
variable types. At its core, Manta proposes a staged hybrid approach that 
starts with low-sensitivity inference to infer more variable types and 
combines it with context- and flow-sensitive refinement to refine type 
information. The inferred type info is then used to effectively improve 
indirect-call pruning and data-dependency-based vulnerability detection in 
static analysis.

Our experiments indicate that Manta outperforms prior work by inferring types 
with 78.7% precision and 97.2% recall. Based on the inferred types, we can 
prune away 63.9% more infeasible indirect-call targets compared to existing 
type-based analysis and perform program slicing on binaries with 61.1% 
similarity to that on source code. Moreover, Manta has led to 86 new 
developer-confirmed vulnerabilities in many popular IoT firmware, with 64 
CVE/PSV IDs assigned.


Date:                   Thursday, 27 August 2026

Time:                   2:00pm - 4:00pm

Venue:                  Room 5506
                        Lift 25/26

Committee Members:      Prof. Charles Zhang (Supervisor)
                        Prof. Shing-Chi Cheung (Chairperson)
                        Dr. Shuai Wang