git clone https://github.com/UNIST-LOFT/binradar.git
cd binradar
git submodule update --init --recursive
docker build -t fuzzolic:2204 -f docker/fuzzolic-runner/Dockerfile.Ubuntu2204v2 .

First, install guix and add the necessary channels. (Check guix installation guide for more details.) Necessary channels are provided in utils/channels.scm. You can copy it to ~/.config/guix/channels.scm or specify it with --channels-file option when you run guix pull.

Then, install just.

Now you can run just taosc in the target benchmark directory to generate patches with TAOSC.

More instructions to run TAOSC

cd benchmarks/loftix/binutils/CVE-2017-14940
# Run `just --list` for available commands
just build
# guix build binutils@2.29
just taosc
# guix shell taosc -- taosc-fix 1 workdir poc "$(guix build binutils@2.29)/bin/nm" -l @@
just setup
# python3 /path/to/binradar/benchmarks/scripts/binradar_setup.py -w workdir
just binradar
# ABS_WORKDIR=$(cd "workdir" && pwd); docker run -v $ABS_WORKDIR:/workdir -v /gnu/store:/gnu/store:ro -v /var/guix:/var/guix:ro --rm fuzzolic:2204 uv run /workspace/fuzzolic/fuzzolic/binradar.py -w /workdir

For batch execution, you can run these commands in benchmarks/loftix directory:

# sudo apt install -y parallel
cd benchmarks/loftix
just build-all
just list exp.list # You can edit exp.list to select benchmarks to run.
just run taosc exp.list 20
just run setup exp.list 20
just run binradar exp.list 20
# Run `just failed taosc taosc_failed.list` to check failed runs.
# You can rerun failed runs with `just resume taosc exp.list 20` based on the joblog or `just run taosc taosc_failed.list 20`.

Binradar requires binradar.env file in work directory.

POC_INPUT="poc/nullderef"
POC_DIR="poc"
BINARY="nm"
TEST_CMD="-l @@"
PATCH_LOC="0x4585dd"
TOTAL_PATCHES="10"
PATCH_RESERVE_ADDR="0x70001000"

This will be generated by benchmarks/scripts/binradar_setup.py after you run just setup.

If you want to add more configuration, you need to provide config.env file. For example, benchmarks/loftix/binutils/CVE-2017-14940/config.env contains:

POC_INPUT="poc/nullderef"
POC_DIR="poc"
BINARY="nm"
TEST_CMD="-l @@"
GUIX_SPEC="binutils@2.29"

The configuration you should provide in config.env includes:

• POC_INPUT: a test case that triggers the vulnerability (e.g., a crashing input)
• POC_DIR: a directory containing poc inputs.
• BINARY: the target binary to be patched and verified. Patched binary should be named as nm.brpatched in the same directory.
• TEST_CMD: the command to run the test case with the binary. Use @@ as a placeholder for the test case file path.
• GUIX_SPEC: the guix package spec for the target binary (e.g., binutils@2.29). This is used for binradar to find the buggy binary in guix store. If GUIX_SPEC is not given, then it uses BINARY. In that case, you should provide buggy program at benchmarks/loftix/binutils/CVE-2017-14940/nm.

The following configurations should be provided for binradar.env (will be automatically generated by binradar_setup.py):

• PATCH_LOC: the location of the patch (e.g., the address of the instruction to be patched)
• TOTAL_PATCHES: the total number of patches to be verified (e.g., if you have 2 candidate patches, set it to 2). Patch id 0 will be original program, and patch id 1, 2 will be candidate patches.
• PATCH_RESERVE_ADDR: the starting address of the reserved region in e9patch. BinRadar will ignore memory accesses in this region to avoid interference with the patch code.

All paths in the configuration should be relative to the working directory.

cd benchmarks/loftix/binutils/CVE-2017-14940
just binradar
# docker run -v /path/to/benchmarks/loftix/binutils/CVE-2017-14940/workdir:/workdir -v /gnu/store:/gnu/store:ro -v /var/guix:/var/guix:ro --rm fuzzolic:2204 uv run /workspace/fuzzolic/fuzzolic/binradar.py -w /workdir

Entrypoint is fuzzolic/binradar.py. It will read the binradar.env file in the specified working directory and run the verification process. You can also specify other options as needed. Timeout can be given as -t or --timeout option (default: 3600 seconds).

Output will be saved in the out directory in the working directory. You can check the logs and results in the output directory.

out/progress.log file contains information about the progress of the verification process. [final] [done] [id {run_id}] [remaining_patches {remaining_patches}] [binradar_remaining_patches {binradar_remaining_patches}] indicates the final result of the verification process.

• fuzzolic/binradar.py: main entry point for the verification process
• fuzzolic/binradar_verifier.py: implementation of the verification logic.
• fuzzolic/analyze_type.py: type inference used for binradar.

These are main phases:

1. PROBE: run the test cases with original binary to confirm the crash and collect information about the crash (e.g., fault address, patch function entrypoint, patch function hit count, etc.)
2. FUZZOLIC: run fuzzolic (concolic execution) with the original binary and the test cases to collect more concrete test cases.
3. DIRECTED: run modified fuzzolic with the original binary and the test cases to collect more directed test cases.
4. FUZZER: run simple binary-only fuzzer with the original binary and the test cases to collect more fuzzed test cases.
5. MINIMIZER: remove redundant or non-reachable concrete test cases.
6. VERIFIER: run patched binary with the collected test cases to check if the patch is correct. If any test case fails, the patch is rejected. If all test cases pass, the patch is verified.
7. BINRADAR: binradar - directly mutate the memory state and check if the patch is correct.
8. FINAL: finalize the verification process and save the results.

Among these phases, FUZZOLIC, DIRECTED, FUZZER and BINRADAR are run in parallel by default. You can run them sequentially by specifying --seq option. Also, you can specify which phases to run by using --run-single-phase option.

Used for concolic execution (fuzzolic, directed) and binradar. Based on QEMU 4.1.1 with modifications for symbolic execution and type inference.

type-infer branch

• Main modified files:
  • tracer/linux-user/snapshot.c, h
  • tracer/linux-user/i386/signal.c
  • tracer/linux-user/syscall.c
  • tracer/tcg/symbolic/symbolic.c, h
  • tracer/tcg/symbolic/models.c
  • tracer/tcg/symbolic-i386.c
• Forkserver: Implemented
• Type Analyzer
  • Logging memory accesses with region info: (trace_mem())
    • Heap: hook into malloc()/free()
    • Stack: hook for callq/ret
    • Global: hook into program segments in elf load
    • Other: ignored
  • Post-processing analyzer: python script (fuzzolic/analyze_type.py)
    • Recover base addresses of each memory chunk using heuristic
• Memory modification
  • Implemented in tracer/tcg

Used for solving path constraints and producing concrete test cases in fuzzolic and directed.

LibAFL/fuzzers/binary_only/qemu_stacktrace: Used for probe, minimizer, and verifier phases. Run original or patched binary with the concrete test cases and get the results.

LibAFL/fuzzers/binary_only/qemu_targeted_simple: Used for fuzzing in fuzzer phase. Collect test cases that can reach the patch location. Fuzzing is done using simple coverage-based fuzzing strategies.