UCSan: Time and Space Efficient Under-Constrained Concolic Execution via Dynamic Data-Flow Analysis

UCSan (Under-Constrained Symbolic Sanitizer) is an efficient concolic execution engine based on SymSan (Symbolic Sanitizer) and the Data-Flow Sanitizer (DFSan) framework. By modeling forward symbolic execution as a dynamic data-flow analysis and leveraging the time- and space-efficient data-flow tracking infrastructure from DFSan, UCSan imposes much lower runtime overhead than previous symbolic execution engines.

Similar to other compilation-based symbolic executors like SymCC, UCSan uses compile-time instrumentation to insert symbolic execution logic into the target program, and a runtime support library to maintain symbolic state during execution.

Under-constrained symbolic execution enables the binary to start execution at any function, which eliminates the considerable cost of setting up a full environment or bypassing complex pre-conditions. The trade-off: the constraints collected are incomplete (under-constrained) and cannot capture all pre-conditions, which may produce false positives.

UCSan is being merged to SymSan, with support of llvm-14 and other features. This repo will be archived after the merge.

Full documentation: see docs/overview.md for architecture details, end-to-end walkthroughs, and the offline solver API.

---

Building

UCSan has two components that collaborate: the instrumentation + runtime library, and a Python companion server called Thoroupy.

Instrumentation component

UCSan leverages the shadow memory implementation from LLVM's sanitizers; only LLVM 12 is currently tested.

Build requirements

• Linux x86-64 (tested on Ubuntu 20.04)
• LLVM 12.0.1: clang, libc++, libc++abi

Compilation

mkdir build && cd build
CC=clang-12 CXX=clang-12 cmake \
    -DCMAKE_INSTALL_PREFIX=/path/to/install \
    -DCMAKE_BUILD_TYPE=Release \
    /path/to/ucsan/source
make -j && make install

Key build outputs (under the install prefix):

Output	Purpose
bin/ko-clang, bin/ko-clang++	Instrumented compiler wrappers
lib/symsan/libTaintPass.so	LLVM instrumentation pass
lib/symsan/dfsan_abilist.txt	DFSan ABI list
lib/libdfsan_rt-x86_64.a	Runtime library
libZ3Solver.a, libThoroupy.a, libFastgen.a	Solver variants

Companion server (Thoroupy)

cd thoroupy
pip install -r requirements.txt

Python 3.10+ required. The solver/lib/libThoroupyZ3.so library is built as part of the CMake build above and copied into this directory automatically.

Build in Docker

A pre-built Docker image is available:

docker load < ucsan.tar
docker run --cap-add=SYS_PTRACE --security-opt seccomp=unconfined \
           --ulimit core=0 --privileged -it \
           -v /path/to/ucsan:/workdir ucsan

LIBCXX

The repo contains instrumented libc++ and libc++abi to support C++ programs. To rebuild from source, run the rebuild.sh script in the libcxx/ directory.

Note: the in-process Z3 solver (solvers/z3.cpp) uses Z3's C++ API and STL containers, so it depends on the C++ libs. This causes linking errors when building C++ targets. Use KO_USE_THOROUPY=1 (out-of-process) for C++ targets instead.

---

Testing

The testsuite/ directory contains a Python test runner and ~35 test programs.

cd testsuite

# Run all tests (quiet output)
python test.py -q

# Run a single test by name
python test.py test linklist

# Verbose output
python test.py -v test linklist

# Debug with GDB
python test.py test linklist -g

# Re-run with a specific seed
python test.py run_seed linklist blocking/linklist.ucsan-xxx.seed

Expected clean result: 33 pass, 2 fail (struct and magma have pre-existing issues unrelated to UCSan correctness).

---

Instrumenting a Binary

Metadata YAML

Every instrumented binary requires a metadata YAML file that names the entry function and the instrumentation scope. Functions outside the scope receive external wrappers that return unconstrained symbolic values.

# note.yaml
entry: cal          # replaces main(); UCSan starts execution here
scope:
  - cal             # fully instrument these functions
  - helper
  - exit            # include exit() so termination is detected

For C++ targets, scope names must use demangled signatures:

entry: "cal(Node*)"
scope:
  - "cal(Node*)"
  - "Node::compute(int)"
  - "exit"

Build from source

METADATA=note.yaml \
KO_CC=clang-12 \
KO_USE_THOROUPY=1 \
KO_TRACE_BB=1 \
KO_DONT_OPTIMIZE=1 \
  ko-clang -o example.ucsan -g example.c

For C++:

METADATA=note.yaml \
KO_CXX=clang++-12 \
KO_USE_THOROUPY=1 \
KO_USE_NATIVE_LIBCXX=1 \
KO_TRACE_BB=1 \
KO_DONT_OPTIMIZE=1 \
  ko-clang++ -o example.ucsan -g example.cpp

Environment variables

Variable	Purpose
METADATA	Path to metadata YAML (required)
KO_CC / KO_CXX	Clang compiler to use (default: clang-12 / clang++-12)
KO_USE_THOROUPY	Out-of-process Thoroupy solver (recommended)
KO_USE_Z3	In-process Z3 solver (C targets only — not compatible with C++)
KO_USE_FASTGEN	Fastgen solver (fast, no SMT)
KO_USE_NATIVE_LIBCXX	Use system libc++ (required for C++ targets)
KO_DONT_OPTIMIZE	Disable forced O3 optimization
KO_TRACE_BB	Trace basic blocks in execution path
KO_WRAP_INDIRECT_CALL	Wrap indirect calls with under-constrained wrappers

Build from LLVM bitcode

Script for building from pre-compiled bitcode

The JSON file below describes the desired instrumentation for the targeted binary. _path specifies the entry function's bitcode file. objs lists additional object files for linking. scope lists functions to instrument.

{
  "_path": "net/sctp/bind_addr.bc",
  "entry": "sctp_raw_to_bind_addrs",
  "objs": ["net/sctp/objcnt.bc"],
  "scope": ["sctp_add_bind_addr", "sctp_bind_addr_state"]
}

path_to_install = "/path/to/install"

import json, yaml, os, subprocess, uuid, sys

KO_FLAGS = [
    "KO_USE_THOROUPY=1", "KO_TRACE_BB=1", "KO_CC=clang-12",
    "KO_DONT_OPTIMIZE=1", "_KO_FORCE_EXTERN_PRIVATE=1", "KO_WRAP_INDIRECT_CALL=1"
]
ko_flags = ' '.join(KO_FLAGS)
cc = (f"opt-12 -load {path_to_install}/build/lib/symsan/libTaintPass.so "
      f"-taint-abilist={path_to_install}/build/lib/symsan/dfsan_abilist.txt "
      f"-taint-abilist={path_to_install}/build/lib/symsan/zlib_abilist.txt "
      f"-O0 -S -disable-verify")
ko_cc = f"{path_to_install}/build/bin/ko-clang"

def execute(command):
    p = subprocess.Popen(command, shell=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
    return *p.communicate(), p.returncode

def compile(tp: dict, fn: str = "tmp.ll"):
    path = tp['_path']
    yaml.dump({"entry": tp['entry'], "scope": tp.get('scope', [])}, open(f"ko-{fn}.yaml", "w"))
    execute(f"{ko_flags} METADATA={os.curdir}/ko-{fn}.yaml {cc} {path} -o {fn}")
    execute(f"llc-12 -filetype=obj --relocation-model=pic -o {fn}.o {fn}")
    execute(f"{ko_flags} METADATA={os.curdir}/ko-{fn}.yaml {ko_cc} {fn}.o -o output.ucsan")

tp = {"_path": "net/sctp/bind_addr.bc", "entry": "sctp_raw_to_bind_addrs",
      "objs": ["net/sctp/objcnt.bc"], "scope": ["sctp_add_bind_addr", "sctp_bind_addr_state"]}
compile(tp)

---

Running the Engine

from manager import UcsanManager

m = UcsanManager("path/to/target.ucsan")
m.run()

When a bug-triggering path is found, the seed is written to testsuite/blocking/<name>-<pid>-block-<timestamp>.seed.

---

Seeds and the Object Model

A seed is a snapshot of symbolic inputs for one execution, stored as a pickled Python Seed object containing a list of UObjects.

Object 0: the argument buffer

Object 0 is a flat byte buffer — not a typed C object. Its bytes feed two sources:

1. Entry function arguments — packed sequentially in declaration order, sizeof(param) bytes each. Pointer args are dereferenced lazily: the first read through a pointer allocates a new child object.

2. External/under-constrained return values — functions outside the scope call __dfsan_wrap_retval, which appends unconstrained bytes to Object 0. Call-site source locations are recorded in objects[0].metadata.citations.

Object 0 byte layout:
 offset  0           8           16           ...
         ┌──────────┬───────────┬──────────────────────┐
         │  param0  │  param1   │  ext. returns ...    │
         └──────────┴───────────┴──────────────────────┘

Objects 1+ are lazily allocated when pointers are dereferenced and carry DWARF-inferred type information via metadata.from_object / metadata.from_offset.

---

Analysis Tools

seed_report — human/LLM-readable seed analysis

python thoroupy/tools/seed_report.py \
    testsuite/blocking/linklist.ucsan-xxx.seed \
    testsuite/binary/linklist.ucsan \
    --entry cal [--format text|json]

Output includes:

• Entry function signature with source location
• Type definitions (struct layouts with per-field byte offsets and source locations)
• Per-object analysis: parameter values, decoded fields, pointer annotations
• Reference graph of object relationships

offline_solver — offline Z3 constraint editing

Allows adding constraints on specific struct fields of a seed and solving for a new concrete seed — without running the instrumented binary. Designed for LLM-driven root-cause analysis and PoC generation.

from tools.offline_solver import SeedConstraintSolver
import z3

s = SeedConstraintSolver(
    "testsuite/blocking/linklist.ucsan-xxx.seed",
    "testsuite/binary/linklist.ucsan",
    entry="cal"
)

print(s.describe())             # inspect structure

v = s.field(1, "v")            # struct node.v → BitVec(32)
s.reset()                       # clear byte-pin defaults
s.add(v == 42)                  # force v = 42
new_seed = s.solve()            # returns updated Seed or None if UNSAT
s.save("patched.seed")          # solve + write pickle

# Nested struct fields use dot notation
ox = s.field(1, "origin.x")    # struct Rect.origin.x → BitVec(32)

Method	Description
param(name)	Z3 BitVec for an entry parameter
field(obj_id, path)	Z3 BitVec for a struct field (dot-notation for nested)
external_return(n)	Z3 BitVec for the n-th external return value
add(*constraints)	Add hard Z3 constraints
reset()	Clear user constraints
solve()	Return updated Seed, or None if UNSAT
save(path)	Solve and write pickle
describe()	Human-readable structure summary
available_fields(obj_id)	List all settable dot-paths for an object

---

Writing a New Test

1. Create the C/C++ file in testsuite/tests/:

// METADATA: mytest.yaml
// FLAG: 200
#include <stdlib.h>

typedef struct { int x; int y; } Point;

int cal(Point *p) {
    if (p->x > 100 && p->y > 100)
        exit(200);
    return 0;
}

2. Create the metadata YAML in testsuite/metadata/:

entry: "cal"
scope:
  - "cal"
  - "exit"

3. Run: python test.py test mytest

Test annotations

Annotation	Meaning
// METADATA: foo.yaml	Which metadata YAML to use
// FLAG: 200	Expected exit code (any count)
// FLAG: 200,3	Expected exit code, exactly 3 seeds
// DISCARD: 1	Exit code to ignore
// ENV: KO_USE_NATIVE_LIBCXX	Extra env vars to set

---

Known Limitations

Issue	Details
struct test (pre-existing)	Struct-return external wrapper loses taint — field shadows zeroed by caller when unpacking
magma test (pre-existing)	Missing __dfsw_magma_log linker symbol
C++ virtual destructors	TaintPass LLVM 12 crash on EH cleanup blocks — omit virtual destructors
In-process Z3 + C++	STL symbol conflicts — use KO_USE_THOROUPY for C++ targets

---

Documentation

See docs/overview.md for a full architecture guide, IPC design, DWARF type system details, and an end-to-end walkthrough.

---

Reference

To cite UCSan in scientific work, please use the following BibTeX:

@inproceedings{yin2026compilation,
  title={A Compilation-based Under-Constrained Execution Engine},
  author={Yin, Mingjun and Li, Zhaorui and Chen, Ju and Zeng, Haochen and Song, Chengyu},
  booktitle={20th USENIX Symposium on Operating Systems Design and Implementation (OSDI 26)},
  address={Seattle, WA},
  year={2026},
  publisher={USENIX Association}
}