Paper Notes: REDQUEEN—Fuzzing with Input-to-State Correspondence

00 - About

Authors: Cornelius Aschermann, Sergej Schumilo, Tim Blazytko, Robert Gawlik, and Thorsten Holz

Fuzz-based automated testing has resurged, especially feedback-driven fuzzing such as AFL. Two persistent obstacles are magic numbers and checksums. Taint tracking and symbolic execution can overcome them but are computationally expensive and often require source access, environmental knowledge, or exact platform semantics.

The paper therefore introduces a lightweight but highly effective alternative to taint tracking and symbolic execution for improving feedback-driven fuzzing. It scales readily to large binary applications and unknown environments.

02 – What

The paper proposes a tracing method based on the observation that input bytes are often copied directly into memory or registers for comparison, creating strong input-to-state correspondence. It traces comparison instructions, tests whether changes at an input offset change program state, and retains mutations that produce new coverage.

The prototype REDQUEEN outperforms KLEE, VUzzer, and AFLFast and found bugs missed by LAVA-M, plus bugs in two Linux filesystems and fifty-five user programs.

03 – How

The method relies on strong input-to-state correspondence: many programs use input values directly as runtime state. Observing these values suggests which offsets to replace—like lightweight taint tracking—and what replacements to use—like symbolic execution.

The authors use this relationship to handle magic numbers and checksums.

Magic bytes

For magic numbers, the authors give this example:

Feedback-driven fuzzers such as AFL struggle with these constructs because they are unlikely to guess the satisfying input—for example, the 64-bit magic value MAGICHDR. Existing magic-number and checksum techniques often add significant overhead.

REDQUEEN handles this simply: whenever a new path appears, it hooks comparison instructions for a trace run. When a comparison has differing operands, it creates a custom <pattern → repl> mutation from them.

Tracing For each new fuzzing input, run one trace, hook all comparisons—including some switch constructs and comparison functions—and extract their operands.

Example: set the input to TestSeedInput. A comparison checks whether its first eight bytes, interpreted as uint64, equal the uint64 interpretation of magichdr. Because integers are generally little-endian, the compared ASCII forms are deestest and rdhcigam.

Variation At runtime, REDQUEEN cannot know which flags are checked after a comparison and therefore cannot distinguish operations such as less-than and equality. It varies comparison values by adding or subtracting one, which also increases the chance of finding off-by-one bugs.

Example: adding and subtracting one from RDHCIGAM produces RDHCIGAL and RDHCIGAN.

Encodings Input may be transformed before reaching a comparison. To cover common transformations and generate more candidates, REDQUEEN applies encodings such as zero/sign extension, reverse, C string, memory, and ASCII.

Example: apply little-endian encoding to RDHCIGAM and RDHCIGAL/RDHCIGAN to obtain MAGICHDR, LAGICHDR, and NAGICHDR.

Application REDQUEEN represents a mutation as <pattern → repl>, identifying the input substring to replace. This works for atomic comparisons without further target modification or hooking and sharply reduces candidate replacement locations.

Example: the TestSeed substring of TestSeedInput is compared with MAGICHDR. Replace only that substring, producing MAGICHDRInput, LAGICHDRInput, NAGICHDRInput, and similar cases.

Colorization Randomize more bytes in the initial input to increase entropy, making it resemble asdmohaoianxb rather than zzzzzzzzzzz.
Strings and Memory Special handling is implemented for memcmp.
Input-Specific Dictionary Add values containing long runs of bytes that are neither zero nor 0xff to an input-specific dictionary. Part of the transformation is shown below:

Checksum

Another challenge for fuzzers is checksums. The paper gives an example.

Existing methods such as FLAYER, TAINTSCOPE, and T-FUZZ share the idea of removing hard checks and repairing them later.

TAINTSCOPE and T-FUZZ also detect hard checks automatically, then use symbolic execution to repair them after interesting behavior appears.

The proposed method proceeds as follows:

Detailed steps:

Identification The following rules identify checksum-related comparisons.
- Find every pattern on the left side of mutation rules while bypassing magic bytes.
- Neither comparison operand is immediate. During colorization, pattern changes with the input and its corresponding replacement changes as well; the value depends on input bytes.

The rule is imperfect: a removed instruction may be a relevant bounds check and produce false positives. REDQUEEN removes all associated patches whenever it adds a new input to the queue, avoiding persistent false positives.

Patch After identifying likely checksum checks, replace their instructions with patches that have the same side effects as a successful comparison.
Verification Run every new fuzzing input on the real target after correcting it with the magic-byte rules above. Retain it if it triggers new coverage; otherwise remove the corresponding patch.

04 – Implementation details

kAFL Fuzzer

kAFL is an OS-independent, AFL-inspired, feedback-driven kernel fuzzer. REDQUEEN was implemented on kAFL with roughly 10,000 changed or added lines. Much of this work supports ring-3 fuzzing, VMI features, bug fixes, evaluation, and debugging rather than the paper's core technique.

Comparison hook

The implementation uses hardware-assisted VM breakpoints to extract input-to-state correspondence. Disassembly records addresses of interesting comparisons. During REDQUEEN analysis, breakpoints are placed there; when hit, operands are saved for later fuzzing. Interesting instructions include calls as well as cmp.

Colorization

REDQUEEN replaces as many bytes as possible with random values without changing the execution path. This increases entropy and reduces the number of locations matching an observed pattern. A binary-search method usually converges within a few hundred executions:

Instruction Patching

REDQUEEN uses KVM and QEMU to replace comparison instructions with cmp al, al, while Intel Processor Tracing filters unexpected cases such as compiler-generated jumps into the middle of instructions.

Input Validation and Fixing

The following algorithm verifies and corrects preliminary comparison candidates in the input:

The algorithm repeatedly applies a single mutation, observes input-to-state correspondence, and iteratively attempts to repair every comparison.

Linux User Space Application Loader for KAFL

The paper extends kAFL with a Linux ring-3 loader to compare it with user-space fuzzers, demonstrating generality and robustness. Major extensions include:

Reimplemented the AFL fork server
Injected fork-server functionality into target startup through LD_PRELOAD
Set the user bit in the model-specific IA32_RTIT_CTL MSR.
Added 32-bit mode disassembly to qemu-pt for decoding 32-bit Intel PT traces

05 – Result

The paper poses three research questions:

Is input-to-state correspondence general enough to work across targets and environments?
How does input-to-state correspondence compare with more complex taint-tracking or symbolic-execution techniques?
What improvements does input-to-state correspondence bring to inputs in real-world fuzzing?

The authors evaluated REDQUEEN across multiple environments and the LAVA-M and CGC suites, then found real-world bugs and compared performance with other kAFL-based tools.

Experiments show substantial advantages over existing methods. REDQUEEN found new bugs in well-tested software: ten bugs across two Linux filesystem drivers and fifty-five across sixteen user-space programs and libraries.

At publication time, the work had received sixteen CVEs, with four pending.

Overall, the paper proposes a simple efficiency improvement based on a common fact: program input is often used directly in logic checks and can be recovered through tracing. The assumption does not cover every case but is broadly useful and efficient.