USENIX OSDI 2026

UCSan

A Compilation-based Under-Constrained Execution Engine

Mingjun Yin · Zhaorui Li · Ju Chen · Haochen Zeng · Chengyu Song

University of California, Riverside

Motivation

Finding bugs in large systems is hard

Neither scales precise analysis to the individual components of a large system.

Software bugs remain the major threat to system correctness, and that is especially true for OS kernels. On the screen is the kernel, drawn as a map of components. We have two ways to hunt bugs in something this big. First, dynamic testing. Watch the fuzzer here. It is precise, but everything it reaches must flow through a hand written harness, plus a virtual machine, a disk image, or real hardware. Components like the network stack are harnessed today, but only after enormous manual effort. Driver heavy or deep code still needs specific setup that it simply does not have. Second, static analysis. It sweeps the entire map, but look at what it leaves behind. UBITect , a static analyzer that analyze the Use before Initialization in linux kernel, emits 147,643 warnings in total, and only 52 were ever confirmed or patched. Nobody can triage that. So neither approach scales precise analysis down to the individual components of a large system.

The gap & our idea

Test components in isolation — at native speed

The dream: extract any subset of code, make it self-contained, analyze it precisely

Under-constrained execution (UC-KLEE) automates this via lazy initialization — allocate & initialize memory objects on first dereference. (Manual extraction — TCP stack, LKL — is labor-intensive and unmaintainable.)

The gap: every existing UC engine is an interpreter — watch them race

Native

finished ✓

1×

KLEE

≈ 3,000× slower…

Angr

≈ 321,000× ☠

Same workload — interpreters re-decode every instruction. File systems, the TCP stack, and drivers are out of reach.

Our idea — UCSan: under-constrained execution as a compiler pass

An LLVM pass + runtime library: compiles any set of C/C++ functions into a self-contained executable → native speed
Decoupled from the dynamic analysis — combine with concolic execution, fuzzing, or model checking

The ideal would be to extract a code subset, make it self contained, and point precise dynamic analysis right at it. People have done this manually. Researchers have extracted TCP stacks, and there is the Linux Kernel Library. But manual extraction is labor intensive and unmaintainable. UC KLEE pioneered the automated version. It is called under constrained execution, with lazy initialization. When a pointer is dereferenced for the first time and points to nothing, you allocate the object on the fly. Here is the gap. Every existing under constrained engine is an interpreter. KLEE is roughly three thousand times slower than native. Angr is over three hundred twenty one thousand times slower. That is nowhere near enough for a file system, the TCP stack, or a driver. Our idea is simple to state. Do under constrained execution as a compiler pass. UCSan is an LLVM pass plus a runtime library, built on the sanitizer framework. It compiles an arbitrary set of functions into a self contained executable that runs at native speed. And it is decoupled from whatever analysis sits on top. To our knowledge, this is the first compilation based engine for under constrained execution. Let me show exactly what that means with a running example.

The running example

Running example: linked-list sum

Goal: analyze cal() in isolation — cover every path, including the assert(false) on line 12.

No tool can start here. Fuzzer input bounces off: there is no main(), and nobody built a list in memory.

head dangles into nothing. UCSan must answer on the fly: what does it point to · how big is it · what's inside?

Compile-time transformation

What UCSan compiles in

Generated entry point — main()

A shadow pointer per pointer argument, deserialize the seed into head, then call cal() → a self-contained binary.

Pointer translation — check_ptr()

Every memory access is translated before use. Aliased pointers (curr, curr->v, head->next) share one shadow pointer — like a segment register. Translated pointers are ephemeral: the object may be reallocated or resized later.

External functions

Map to a wrapper (kmalloc → malloc) · assume pure · or havoc pointer args. (None in this example.)

All on LLVM IR — zero source changes; any code that emits IR works.

This is what UCSan compiles in. It is shown at source level for readability, but the real transformation happens on LLVM IR. Green lines are inserted. Struck out lines are replaced. There are three parts. First, a generated main function. It creates a shadow pointer for each pointer argument, deserializes the seed into head, and calls cal. Second, pointer translation. Before every memory access, we insert a call to check pointer, which translates a potentially uninitialized pointer into a real address. The shadow pointer is the key data structure. All aliased pointers share one, and it works like a segment register. Translated pointers are deliberately ephemeral, because the underlying object may be reallocated or resized. Third, external functions. We can wrap them, for example mapping kmalloc to malloc. We can assume they are pure. Or we can havoc their pointer arguments. This example has none. Everything happens on LLVM IR. Zero source changes. Any code that emits IR works.

Two ideas — thirty seconds

Just-In-Time Initialization (JITI) & pseudo- vs. real pointers

Watch for these in the next three runs: every pointer the program touches is a pseudo-pointer · check_ptr turns it into a real pointer just in time · JITI materializes memory the first time it's needed.

⌗ hover — peek at the instrumented code

Before we run it, two pieces of vocabulary. This takes thirty seconds. After the transformation, the pointer values the program manipulates, like head equals hex one, are pseudo pointers. They are logical addresses that do not address real memory. Only the shadow pointer knows the actual backing object. It works exactly like a segment register, and all aliased pointers share one. Now watch the translation arithmetic, in execution order. First, container of. That is pure pointer arithmetic, and arithmetic on pseudo pointers needs no translation at all. So curr simply becomes hex one, minus the size of the int in front of the list field. That is minus three. The cast also reveals the real underlying type, node t, and that tells UCSan the right allocation size. Second, the first actual dereference is the address of curr arrow v, whose pseudo value is minus three. That triggers just in time initialization. UCSan mallocs object one as a zero filled phantom, and the shadow pointer records the pseudo value at that moment, minus three, as the segment's base offset. So minus three maps to object one's v field, at segment offset zero. From then on, every real pointer is computed as the object base, plus the current offset, minus the base offset. For example, head arrow next has pseudo value hex one. Object one, plus hex one, minus minus three, equals object one plus four. That is exactly the next field. Real pointers are deliberately ephemeral. They are used for one access and then thrown away, because the backing object may later be reallocated or resized. In fact, container of can even grow it. Keep these in mind. You will see all of them across the next three seeds.

Plug in an analysis

Exploring paths needs a solver — so plug one in

The binary runs — but exploring paths needs new seeds. UCSan is decoupled, so that’s just composition.

= UCSan^† — a complete under-constrained concolic engine; this loop drives the exploration you’re about to watch.

Concolic exploration ① ② ③

Seed 0 — start with an empty seed

①get_concrete(head): not in seed → phantom object, zero-filled → head = 0x0

②while(head): 0 → loop skipped, sum = 0 → assert NOT triggered

③Solver negates head ≠ null → assign head = 0x1 (a pseudo-pointer — any non-null value works) ⟹ Seed 1

Concolic exploration ④ ⑤ ⑥ ⑦

Seed 1 — JIT-initialize on first access

⑤check_ptr → JITI allocates obj1 (phantom): size from container_of → node_t, not list_t · pointed-by SO@0 recorded

⑥pseudo-pointer head->next (0x1) → real obj1.list.next; shadow ptr stores logical base −3 (1−4), so any pointer arithmetic keeps working

⑦obj1.next = 0 → loop exits · sum = 0+obj1.v is symbolic → solve sum>100 ∧ obj1.next≠0 ⟹ Seed 2

With seed one, head is hex one. We enter the loop, and the first dereference triggers just in time initialization. check pointer allocates object one as a phantom. There are three challenges right here. Challenge one is size. Trusting head's declared type, list t, would under allocate. UCSan instruments pointer arithmetic and casts, so container of reveals the real type, node t. Challenge two is offset. The pointer lands on the embedded next field, and the shadow pointer records the logical base, minus three, because container of subtracted four from hex one. The v field is recovered through that negative offset. Challenge three is future seeds. UCSan records that object one is pointed by slot zero of the super object. Object one is zero filled, so next is null and the loop exits. But sum is now symbolic. It is zero plus object one's v. The solver asks for sum greater than one hundred, and object one's next not null. That gives seed two. Note that object one's next can also be hex one, the same value as head. The same logical address in different segments never conflicts.

Concolic exploration ⑧ ⑨ ⑩

Seed 2 — replay objects & trigger the bug

⑨obj1 loaded from seed (via pointed-by recorded at ⑤) → obj1.next = 0x1 → re-enter loop

⑩check_ptr → JITI obj2 (phantom); record point-to (obj1 off 4 → obj2); obj2.next = 0 ends the loop

sum = 101 → assert(false) FIRES ✓ all paths covered — no harness, no manual setup

Generalize

Everything you saw is automatic — and analysis-agnostic

LLVM IRany front end — e.g. kernel LTO build ; cal.bcdefine i32 @cal(ptr %head)

YAML configentry · scope · external fns entry: calscope: [foo, bar]kmalloc: → malloc

➜

UCSan pass instrument memory accesses · handle external calls · drop out-of-scope code *p ⇒ *check_ptr(p, p_s)kmalloc() ⇒ malloc()✂ out-of-scope functions

➜

analysis pass (optional)pipelined on the same IR SymSan: sum>100 ⇒ SMTor fuzzer · model checker

➜

self-contained executableUCSan + PUT + analysis runtimes; a normal user-space program $ ./cal_uc seed2assert(false) hit!

Config is the harness-killer: name any function as entry, any set of functions as scope. Write it by hand — or generate it with static analysis or an LLM.

Output runs anywhere: no VM, no disk image, no device. Kernel code becomes a normal user-space process.

Stepping back. Everything in that walkthrough is produced by this fully automatic pipeline. There are two inputs. The first is the program as LLVM IR. Any front end that emits IR works, and for the kernel, enabling LTO gets you the IR. The second is a small YAML config that names the entry function, the analysis scope, and how to handle out of scope functions. The config can be written by hand, or generated by static analysis or an LLM. UCSan instruments every memory access for address translation, stubs or wraps external calls, and drops out of scope code. Any analysis pass slots into the pipeline the same way SymSan did. Fuzzing or model checking work too. The output links into a normal user space executable. No virtual machine, no disk image, no device. The snippets under each stage show our linked list example flowing through. Cal's IR plus a three line config goes in. Check pointer instrumentation happens in the middle. And at the end, you get a binary that you just run with a seed, and it hits the assertion. That generality is what we now evaluate.

Performance

RQ1: Native-speed execution

Linked-list micro-benchmark (20 nodes)

UCSan

9s

KLEE

20s

Angr

79s

Takeaways

UCSan beats KLEE by orders of magnitude on every nbench test
Angr: no single iteration in 18h — crashed (OOM)
UCSan^†'s extra cost is just SymSan's symbolic tracing

nbench — slowdown vs native execution (log scale, lower is better)

UCSan (≈ 2–33×) UCSan^† (≈ 2–56×) KLEE (≈ 1,700–50,600×)

We evaluated three questions. Is it fast? Does it compile real world code? And does that translate into finding more bugs? First, performance. On the linked list micro benchmark with 20 nodes, end to end and without path exploration, UCSan takes 9 seconds, KLEE takes 20, and Angr takes 79. On the nbench suite, the gap is dramatic. This chart shows slowdown versus native execution, on a log scale. UCSan and UCSan dagger sit around one order of magnitude. KLEE sits three to four orders of magnitude above native, on every single test. Angr could not finish one iteration in 18 hours and crashed out of memory, so it is excluded. Since nbench does no constraint solving, the gap between UCSan and UCSan dagger isolates SymSan's tracing overhead. Under constrained execution itself adds very little.

Compatibility

RQ2: Compiles real kernel code

Compiled three Linux kernel versions: 4.14 · 5.10 (Android LTS) · 6.16 (latest stable)

Analysis scopes generated automatically: function pointers in static initializers as entries + call-graph analysis.

kernel modules

>80%

compile successfully

v5.10 · 15k scopes

96.2%

analysis scopes compiled

v6.16 · 157k scopes

88.9%

analysis scopes compiled

Remaining failures: unhandled inline assembly — the same limitation KLEE has. Unlike KLEE, UCSan offers a path forward: complex blocks can be modeled with a custom wrapper function (the same mechanism as external functions; LLMs can help generate them).

Next, compatibility. We compiled three kernel versions. Version 4.14, version 5.10, which is the Android long term branch, and version 6.16, the latest stable at evaluation time. Scopes were generated automatically, using function pointers from static initializers as entries, plus a simple call graph analysis. Overall, more than 80 percent of kernel modules compile. On 5.10, that is 96.2 percent of about fifteen thousand scopes. On 6.16, it is 88.9 percent of roughly 157 thousand. Almost all the remaining failures come from unhandled inline assembly, which is the same limitation KLEE has. But unlike KLEE, which is stuck there, UCSan offers a path forward. Any complex assembly block can be modeled with a custom wrapper function, using the same wrapper mechanism you saw for external functions. And we observed that LLMs can help generate these wrappers, removing most of the manual effort.

Impact · UBITect

RQ3: Filtering static-analysis warnings

Task

Confirm/refute UBITect's use-before-init warnings — 2-minute, 2 GB budget per warning. UCSan^† vs the KLEE-based engine built for this exact task (IncreLux).

Warnings finished within the 2-min budget

UCSan^†

95.46% (63,957)

KLEE

41.29%

6.36× faster average time-to-finish · 15.06× faster per warning (median 4.62s vs timeout)

Time-to-finish (2-min timeout)

	25th%	Median	75th%	Mean
UCSan^†	3.98s	4.62s	6.21s	14.37s
KLEE	92.13s	T.O.	T.O.	105.71s

That speed buys results

111 more warnings confirmed than the KLEE-based engine
≥ 15 real UBI bugs, later patched upstream — could have been caught years earlier

Our first bug finding case study is confirming or refuting UBITect's static analysis warnings, with a two minute and two gigabyte budget per warning. We compare against IncreLux, the KLEE based engine built for this exact task. UCSan dagger finishes over 95 percent of all warnings. The KLEE based engine manages 41 percent. Average time to finish is 6.36 times faster. Per warning throughput is 15 times faster. The median case finishes in under five seconds, while KLEE's median hits the timeout. That speed buys results. 111 more warnings confirmed, and at least 15 of them correspond to real use before initialization bugs that were later patched upstream. With this tool, they could have been caught years earlier.

Impact · CVEs

RQ3: Reproducing real vulnerabilities — no harness

Reproduce known bugs with only a scope + entry function (most configs generated automatically, incl. by a coding agent).

NVD CVEs

30 / 30

OSS + kernel — all reproduced

AFGen CVEs

69 / 94

re-discovered

SyzSpec kernel bugs

26 / 38

no fuzzer · no syscall specs

All without hand-crafted test harnesses; most misses are path explosion or incomplete scope, with a few from unsupported features (e.g. concurrency).

Conclusion

▸ UCSan: the first compilation-based under-constrained execution engine — native speed, general, decoupled from the analysis.

▸ Enables under-constrained concolic execution at scale — finishing far more analysis tasks and finding real bugs without harnesses.

▸ Validated on the Linux kernel and 150+ real CVEs & kernel bugs across three datasets.

Open source (Apache 2.0): github.com/R-Fuzz/UCSan

Thank you!

Questions? · [email protected] · github.com/R-Fuzz/UCSan

ACKNOWLEDGMENTS

We thank the anonymous reviewers for their insightful comments, and our shepherd for the valuable suggestions. This work is supported, in part, by the National Science Foundation (Grant No. 2046026), the Google ASPIRE Fund (2023 Award), and the United States Air Force and DARPA (Agreement No. FA8750-24-2-0002). Any opinions, findings, conclusions, or recommendations expressed are those of the authors and do not necessarily reflect the views of the funding agencies.

UCSan

Finding bugs in large systems is hard

Test components in isolation — at native speed

The dream: extract any subset of code, make it self-contained, analyze it precisely

The gap: every existing UC engine is an interpreter — watch them race

Our idea — UCSan: under-constrained execution as a compiler pass

Running example: linked-list sum

What UCSan compiles in

Generated entry point — main()

Pointer translation — check_ptr()

External functions

Just-In-Time Initialization (JITI) & pseudo- vs. real pointers

Exploring paths needs a solver — so plug one in

The binary runs — but exploring paths needs new seeds. UCSan is decoupled, so that’s just composition.

Seed 0 — start with an empty seed

Seed 1 — JIT-initialize on first access

Seed 2 — replay objects & trigger the bug

Everything you saw is automatic — and analysis-agnostic

RQ1: Native-speed execution

Linked-list micro-benchmark (20 nodes)

Takeaways

RQ2: Compiles real kernel code

Compiled three Linux kernel versions: 4.14 · 5.10 (Android LTS) · 6.16 (latest stable)

RQ3: Filtering static-analysis warnings

Task

Warnings finished within the 2-min budget

Time-to-finish (2-min timeout)

That speed buys results

RQ3: Reproducing real vulnerabilities — no harness

Conclusion

Thank you!

Outline — UCSan · OSDI 2026

Speaker notes