StateLens — path-exhaustive fuzzing

Overview

StateLens targets programs and firmware, including RTOS and embedded targets, with the goal of exercising substantially every execution path. I worked on the software and analysis infrastructure: an LLVM pass rewriting program IR into a canonical deterministic form, extraction of control-flow structure so paths can be enumerated, a path-solver service, a customized AFL++ fork, and the reproducible build system.

Bound by NDA — I do not own the code, so details stay at the architecture level.

Design decisions 04

• A “namify” LLVM pass deterministically renames functions, basic blocks, allocas, and globals to a stable scheme — with an aggressive mode that also rewrites already-named globals — so downstream analysis reads one canonical IR regardless of how Clang originally named things.
• Path enumeration was explored two complementary ways rather than committing to one hand-coded traversal: a declarative Answer Set Programming formulation (facts and rules derived from the control-flow graph, visualized through a custom Graphviz fork) and a hand-written C++ constraint-graph engine.
• The C++ engine models the program as a constraint graph whose edges carry guards and state transformers, uses precomputed per-node reachability bitsets and dominator data for a fast path solver, and prunes repeatedly-infeasible dead edges — served over a Unix domain socket so the solver runs as a service.
• The toolchain is packaged as a Guix channel pinning a specific AFL++ fork and dependency forks, so the whole team builds bit-identical toolchains and the customized fuzzer is a reproducible, versioned dependency instead of a manually-installed binary.

LLVM / C++ · Clang · AFL++ · Guix · Answer Set Programming

listed under experience →