Path-sensitive and alias-aware typestate analysis for detecting OS bugs

Finding bugs in an operating system by reasoning about code rather than running it normally fails in one of two ways — the analysis is too imprecise and buries you in false alarms, or it is precise and too slow to finish on 14 million lines; the usual precision tool, working out which pointers refer to the same memory, breaks down badly on operating systems because most kernel functions are reached through function-pointer tables and so have no visible caller, leaving their pointer parameters with EMPTY information and causing the analysis to silently conclude that two genuine aliases are unrelated; this paper (Tsinghua and UTS) derives aliases from assignments along each control-flow path instead, and then finds that knowing two variables are the same thing makes the analysis CHEAPER rather than more expensive — 49.8 percent fewer states to track and 87.3 percent fewer constraints to solve.

The argument in one glance

Problem

Kernel bugs matter enormously, and analysis either drowns you or never finishes

An operating system is what everything else stands on, so even an ordinary mistake — dereferencing a pointer that turned out to be null, reading memory nobody initialised, forgetting to release memory on an error path — can crash a machine or open it to attack. Finding these by reasoning about the code instead of running it is the standard approach, and it fails in one of two directions. An imprecise analysis produces so many false alarms that developers stop reading them. A precise analysis does not finish, because following a separate state for every variable along every path through 14 million lines is an enormous amount of work.
What people did

Buy precision with points-to analysis

The standard way to make such an analysis precise is POINTS-TO ANALYSIS: work out, for each pointer, which memory objects it could refer to. Two pointers whose sets of possible objects overlap might be ALIASES, meaning two names for the same memory, and knowing that is essential — a check on one name protects the other, and a mistake through one name is a mistake through both. Most serious bug-finding tools do this, including the Clang Static Analyzer, Infer, Saber and SVF, and it is a well-founded and successful technique on ordinary programs.
Why it fell short

Kernel functions have no callers, so the analysis concludes they alias nothing

Points-to analysis names memory objects by the place they were allocated. But an operating system is modular and driven by events: a driver registers its initialisation routine in a table of function pointers, and the kernel invokes it from somewhere else entirely, so there is no CALL to that function anywhere in the analysed code. Its pointer parameters therefore have EMPTY sets of possible objects. Since two empty sets do not overlap, the analysis concludes those parameters alias nothing — silently, and with confidence. A real null-pointer dereference in a Linux media driver is invisible for exactly this reason. Recording every alias pair explicitly instead would work, but costs too much memory to scale to a kernel.
This paper's idea

Derive aliases from assignments along each path, and let precision pay for itself

This paper (Tsinghua and University of Technology Sydney — Li, Bai, Sui, Hu) drops points-to information entirely. Along each control-flow path it maintains a graph in which each node is a set of variables naming one memory object and each edge is a field access or a dereference, updated by the assignments it walks past. No allocation sites are needed, so a function with no caller is not a problem — it is where the analysis STARTS. The result then inverts the usual trade. Knowing that several variables are the same thing means keeping ONE state for the whole group instead of one each, and creating ONE solver symbol instead of several plus the constraints tying them together. Precision makes the analysis cheaper: 49.8 percent fewer states and 87.3 percent fewer constraints. It found 574 real bugs across Linux and three embedded operating systems, 206 confirmed by their developers.

Why this problem is worth solving

The technique in question is old and well understood, which is what makes its failure on kernels interesting.

TYPESTATE ANALYSIS gives each variable a STATE and describes the legal sequences of operations on it as a small state machine. For null-pointer dereferences the states are roughly “unknown”, “known to be null” and “known not to be null”; assigning null or taking the branch where a check failed moves a variable into “known null”, and DEREFERENCING it while in that state is the bug. Memory leaks use the same shape: allocating moves an object to “not freed”, freeing moves it to “freed”, and returning from a function while still “not freed” is the bug. This is attractive because one framework covers many bug types — each new checker here is 100 to 200 lines. The cost is that a state must be carried for every variable along every path, and a kernel has an enormous number of both. Running this analysis over four operating systems tracked 45.8 billion states before the paper’s optimisation, and 23.0 billion after

The specific reason precision fails here is structural rather than accidental.

Two variables ALIAS when they name the same memory. This matters enormously for bug finding: if p and q alias, then a null check on p tells you something about q, and a dereference of q is a dereference of p. The standard way to determine aliasing is POINTS-TO ANALYSIS, which computes for each pointer the set of memory objects it might refer to, naming those objects by their allocation sites. Two pointers whose sets overlap may alias. Kernel code breaks this in a specific way. Operating systems are modular and event-driven, so a driver does not call its own entry points — it stores them in a structure of function pointers and the kernel invokes them from another module entirely. From the analysis’s point of view those functions have NO CALLER, so their pointer parameters were never assigned anything and their sets of possible objects are EMPTY. Two empty sets do not overlap, so the analysis reports “not aliases” — which is not a warning, it is a wrong answer delivered confidently

What people did before, and where it broke

Path-sensitive analysis of scalar values. Some analyses track values precisely along individual paths, which is exactly the right idea, but they reason about numbers rather than pointers. Most interesting kernel bugs are about pointers.
Typestate plus flow-insensitive points-to. Others handle pointers by bolting on a cheap points-to analysis that ignores statement order. That combination is unstable: imprecise alias facts fed into a path-sensitive analysis produce large numbers of false alarms, particularly on big programs with complicated pointer use.
Flow-sensitive alias analysis that merges at join points. More careful analyses respect statement order but must combine results where two branches meet. Taking the INTERSECTION loses real aliases that hold on one branch; taking the UNION invents aliases that hold on neither. Either way, no individual path gets an accurate answer.
Value-flow graphs for one bug type at a time. Recent path-sensitive tools pre-compute a graph of how values flow and then check reachability from a source to a sink, which works well for memory leaks. But that graph is built with points-to analysis, so it inherits the kernel problem, and reachability alone carries no state, so it does not generalise across bug types.
General-purpose bug finders. Cppcheck, Coccinelle, Smatch, the Clang Static Analyzer, Infer, Saber and SVF all detect kernel bugs. Most are path-insensitive and either approximate aliasing crudely or ignore it. On the Linux kernel the Clang Static Analyzer produced 1,151 reports of which 196 were real — an 83 percent false alarm rate — while Saber and SVF ran out of memory and did not finish at all.
The gap. Everyone treated precision as something you pay for and therefore ration. Nobody had noticed that on this particular analysis, precision about aliasing is not a cost at all — it is the thing that makes the analysis affordable.

How aliases become the optimisation

Derive aliases from the path, merge what is the same, and validate only what looks wrong

Track a state per variable along every path

Classic typestate analysis gives each variable a state, follows the control-flow graph, and reports a bug when an illegal sequence occurs. It needs to know which variables alias, and gets that from points-to analysis, which fails on kernel functions that have no visible caller.
↓ →
Start where points-to analysis gives up new

Take every function that has no explicit caller in the code — precisely the module entry points registered through function-pointer tables — and begin analysing there. Walk the control flow depth-first, one path at a time, unrolling loops and recursive calls exactly once.
↓ →
Build the alias picture from assignments, not allocations new

Maintain a graph in which each node holds a set of variables naming one memory object, and each edge is labelled with a structure field or a dereference. Four instruction kinds update it. Because a field access gets its own edge, two different fields of the same structure stay distinct.
↓ →
Keep one graph per path rather than merging at joins new

Where branches meet, copy the graph into each branch instead of intersecting or unioning them. Every program point therefore has a separate alias picture for each path reaching it, so an alias that holds only on one branch is neither lost nor wrongly generalised.
↓ →
Give the whole alias set ONE state new

Rather than a state per variable plus synchronisation between aliases, keep one state for each group of variables naming the same object. Any instruction touching any member moves the group. This is where the saving comes from, and it cut states tracked by 49.8 percent.
↓ →
Solve constraints only for candidate bugs, one symbol per group new

Skip feasibility checking entirely while searching, since paths containing suspected bugs are a small fraction of all paths. Then, for each candidate, translate its path into constraints for a solver — using one symbol per alias group, which removes both the equalities linking aliases and the implications between their fields.

Run on Linux 5.6 with all kernel code enabled, plus Zephyr, RIOT and TencentOS-tiny — 10.3 million lines analysed — on an ordinary desktop with eight processors and 16GB of memory, in 35 hours and 29 minutes total.

The idea

The obstacle is also the entry point. The reason points-to analysis fails here is that kernel functions are registered in tables and invoked from elsewhere, so they have no visible caller and their parameters carry no information. That is usually described as a limitation to be worked around. This paper turns it around: those callerless functions are exactly where the analysis BEGINS, one at a time, treating each as the root of its own exploration. Aliases are then derived from the assignments actually encountered — a store makes two names refer to one object, a field access adds a labelled edge — which requires no knowledge of where memory was allocated and therefore does not care that the caller is invisible. The information points-to analysis was missing was never needed. Recognising that the property blocking one approach is the natural starting point for another is the same reframe covered elsewhere on this site where a structural feature that defeats the conventional method turns out to define exactly where the alternative should begin.

Precision that pays for itself. Static analysis is normally taught as a trade: more precision, more cost, choose a point on the curve. This paper found a place where the curve bends the other way. Once you know that several variables name the same memory, you do not need a state for each of them plus machinery to keep those states synchronised — you need ONE state for the group, which any member can advance. The same applies at the solver: existing tools create a symbol per variable and then add equality constraints tying aliases together, plus implications saying their corresponding fields are equal too. Map the whole group to one symbol and all of that disappears, because the equalities become tautologies. The measured effect is large — 49.8 percent fewer states, 87.3 percent fewer constraints, 1.92 billion down to 244 million. Discovering that two things are the same is normally filed under accuracy; here it is directly a compression. Treating provably-identical things as a single object, so that work shrinks rather than merely becoming more correct, is the same equivalence-class reasoning covered elsewhere on this site where collapsing indistinguishable states turns an intractable enumeration into a feasible one.

Search cheaply, then validate the few survivors. The third move is a division of labour. Checking whether a path can actually execute requires a constraint solver and is expensive, so doing it during the search would be ruinous. But the observation is that paths containing a suspected bug are a small fraction of all paths. So the first stage ignores feasibility entirely and over-reports, and the second stage runs the solver only on the candidates it produced — discarding 54.7 thousand false reports. The two stages share the alias information, which is what makes the second one affordable. Separating a cheap over-approximate search from an expensive precise check, and paying the expensive one only where the cheap one already pointed, is the same filter-then-verify structure covered elsewhere on this site where a fast pass narrows an enormous space so a slow pass can afford to be exact.

A three-year-old null dereference in Zephyr

A real bug in the Zephyr Bluetooth mesh code, found and fixed from this tool's report

The bug had existed since Zephyr 1.8.0 in June 2017 — nearly three years. Simplified from the paper.

Step 1 of 5

One function checks the pointer and takes the failure branch

In friend_set, a local pointer cfg is assigned from a structure field, model->user_data. A few lines later the code tests whether cfg is null, and on that branch logs a warning and jumps to a shared exit label. Taking that branch is itself the information that matters: on this path, cfg is null.

the assignment makes cfg and model->user_data two names for the same memory, so the branch also establishes that model->user_data is null
the analysis records this as a graph edge labelled with the field user_data, which is why the two are linked rather than merely both present

Why it works

Aliases are derived from assignments rather than allocation sites → a function whose caller is invisible is analysable → so the module entry points that defeat points-to analysis become the natural starting points instead.
Each control-flow path keeps its own alias graph rather than merging at joins → an alias holding on one branch is neither discarded by intersection nor wrongly generalised by union → giving accurate alias facts for every individual path.
Variables naming one object share one state instead of one each plus synchronisation → the number of states falls with the amount of aliasing found → cutting states tracked from 45.8 billion to 23.0 billion, a 49.8 percent reduction.
One solver symbol per alias group makes equalities between aliases, and implications between their fields, into tautologies → those constraints need never be written or solved → reducing constraints from 1.92 billion to 244 million, an 87.3 percent reduction.
Feasibility checking is skipped during the search and applied only to candidates → the solver runs on a tiny fraction of paths → discarding 54.7 thousand false reports and bringing the false alarm rate from 69 percent down to 28.

What it costs (trade-offs and scope)

Loops and recursion are unrolled exactly once. This bounds the work and is deliberately unsound in both directions: aliases established on a second iteration are missed, and reports that depend on a loop running more than once can be wrong.
Indirect calls are not followed. Function-pointer calls are unhandled, so bugs whose trigger path passes through one cannot be found — a pointed limitation, given that function-pointer tables are what create the callerless entry points the design relies on.
Array indexing is not modelled. With a non-constant index, two accesses get different access paths and are treated as distinct even when they are provably equal, which produces false reports.
Concurrency is invisible. If one thread initialises a variable and another reads it under proper synchronisation, the analysis sees a read with no preceding initialisation and reports a bug that is not there.
The false alarm rate is 28 percent, not zero. Of 797 reports, 223 were wrong, and a PhD student spent 12 hours reading them. The analysis also took 33 hours on Linux against 8 for a version without alias reasoning, so the alias analysis itself is not free — it buys accuracy, and pays for part of itself downstream.

The evaluation

The tool was run on Linux 5.6 with every kernel option enabled and on three embedded operating systems — Zephyr, RIOT and TencentOS-tiny — covering 10.3 million of their 16.8 million lines, with the remainder excluded by build configuration rather than by choice. The hardware was an ordinary desktop with eight processors and 16GB of memory, and the whole run took 35 hours and 29 minutes. Every report was checked by hand. To avoid overwhelming maintainers, only 200 randomly chosen Linux bugs plus all 120 embedded-system bugs were submitted upstream.

Finding null dereferences, uninitialised reads and leaks in an operating system

Property	General-purpose checkers	Points-to based analysis	Path-derived alias sets
Handles callerless entry points
Alias facts at a branch join
Effect of finding more aliases
False alarm rate on these systems
Completed on the Linux kernel

574 real bugs were found — 463 null-pointer dereferences, 90 uninitialised-variable accesses and 21 memory leaks — of which 206 were confirmed by the developers of the four systems, with 13 submitted patches fixing 46 bugs merged and the rest fixed by maintainers from the reports. 328 of the real bugs were missed by all seven tools compared against. Three additional checkers, each 100 to 200 lines, found 43 more real bugs of three further types. Removing the alias reasoning entirely raised the false alarm rate from 28 to 69 percent and lost 260 of the real bugs.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This analysis is deliberately unsound in several places, and the authors are direct about all of them. Loops and recursive calls are unrolled exactly once, which both misses aliases established on later iterations and produces wrong reports that depend on a loop running more than once. Indirect calls through function pointers are not followed at all, which is a sharp limitation given that function-pointer tables are precisely what create the callerless entry points the whole design depends on. Array indexing with a non-constant index is not modelled, so two accesses that are provably the same element are treated as different. Concurrency is invisible, so a variable initialised by one thread and read by another under proper synchronisation is reported as an uninitialised read. The headline accuracy is real but not magic: 223 of 797 reports were wrong, a 28 percent false alarm rate, and one PhD student spent 12 hours reading them — better than the 69 percent the same tool produces without alias reasoning and far better than the 83 percent from the Clang Static Analyzer, but still a human cost per run. The alias analysis is not free either; it roughly quadrupled the Linux analysis time against a version without it, buying accuracy and recovering only part of that cost through the state and constraint reductions. Coverage was also partial, at 10.3 million of 16.8 million lines, with the rest excluded by build configuration — and two bugs that competing tools found were missed for exactly that reason, since those tools read source without compiling it.

Background

When precision compresses instead of costing, and the obstacle marks the starting point

This paper sits in the site’s correctness and program analysis cluster and rhymes with several ideas covered elsewhere on this site. Its central result belongs to the equivalence-class lineage this site keeps returning to: recognising that several names refer to one object lets the analysis carry one state and one solver symbol instead of many, so discovering that things are identical COMPRESSES the work rather than merely improving its accuracy — the same move the compiler super-optimisation and concurrency-testing pages make when collapsing provably indistinguishable states turns an intractable enumeration into a feasible one, and the same move the quantum optimisation page makes when a symmetry lets half the search be inferred rather than run. Its two-stage structure, where a cheap over-approximate search runs first and an expensive solver touches only the candidates that search produced, is the filter-then-verify division the recommendation-inference and graph-mining pages also use when they do heavy analysis offline against stable structure and keep only a cheap step on the hot path. And its opening reframe — that the property defeating the conventional method, kernel functions having no visible caller, is exactly where the alternative should begin — is the same look-again-at-the-obstacle reasoning the dynamic-shape compilation page uses when it notices that the part of the problem needing tuning does not depend on the unknown at all.

If you remember only three things

1. Bug-finding by static analysis fails on operating systems in one of two directions: too imprecise and it buries developers in false alarms, too precise and it never finishes across 14 million lines. The usual precision tool, points-to analysis, breaks structurally here — a driver registers its entry points in a table of function pointers and the kernel invokes them from another module, so those functions have NO visible caller, their pointer parameters have empty sets of possible memory objects, and since two empty sets do not overlap the analysis concludes confidently and wrongly that two genuine aliases are unrelated.
2. The fix is to derive aliases from the assignments actually walked past rather than from allocation sites, keeping a graph per control-flow path whose nodes are groups of variables naming one object and whose edges are field accesses and dereferences. No allocation information is needed, so callerless functions become the natural place to START. Keeping a separate graph per path rather than merging at branch joins also avoids the choice between intersection, which loses real aliases, and union, which invents false ones.
3. The surprising part is that precision here is a compression rather than a cost. Variables in one alias group share ONE state instead of one each plus synchronisation, and map to ONE solver symbol, which turns the equalities between aliases and the implications between their fields into tautologies that never need writing — 49.8 percent fewer states and 87.3 percent fewer constraints. Feasibility is then checked only on candidate paths, discarding 54.7 thousand false reports. The result was 574 real bugs across four operating systems at a 28 percent false alarm rate, against 69 percent for the same tool without alias reasoning, with 206 confirmed by maintainers and one three-year-old Zephyr bug fixed from its report.

Check yourself

Check your understanding

1. Points-to analysis is a mature, well-founded technique, yet it misses a real null-pointer dereference in a Linux driver entirely. Predict what goes wrong.
2. In static analysis, precision normally costs time. Here, being more precise about aliasing makes the analysis 87.3 percent CHEAPER at the solver. Predict why.
3. Existing flow-sensitive alias analyses combine their results where two branches meet, either by intersection or by union. Predict why this analysis instead keeps a separate graph for every path.
4. The search stage deliberately ignores whether a path can actually execute, and only afterwards runs a constraint solver on the candidates. Predict why not check feasibility while searching.

Sources

Path-Sensitive and Alias-Aware Typestate Analysis for Detecting OS Bugs (author PDF) — ASPLOS 2022; the full 24-page paper, read in full for this explainer.
ACM Digital Library (DOI 10.1145/3503222.3507770) — published version.