SymRadar

SymRadar is a patch verification tool for vulnerability repair. SymRadar performs patch verification by covering near the ciritical input-space area by extracting concrete snapshot and construct abstract snapshot to enable symbolic execution. This repository contains implementation of SymRadar: PoC-Centered Bounded Verification for Vulnerability Repair (ICSE '26) and experiment scripts.

Directory Structure

symradar

This is our main technical contribution. It contains KLEE-based symbolic execution tool which supports under-constrained symbolic execution and lazy initialization. It can handle concrete snapshot extraction, abstract snapshot construction from concrete snapshot, and patch verification based on UC-SE and lazy initialization. Several optimizations and heuristics are applied to support such features.

Benchmarks

CPR

CPR is a automated vulnerability repair tool that generate patches for vulnerable program. CPR's output is our main patch validation target. This directory contains benchmarks and scripts for experiments.

Getting Started

This is example with one subject. Check CPR directory to run full experiments.

1. Docker image for experiments

docker pull hsh814/symradar:2025-12-24
docker run -d -it --name symradar hsh814/symradar:2025-12-24 bash

2. Running a simple example (libjpeg/CVE-2018-19664)

cd /root/projects/CPR
# 1. Compile patches generated by CPR
sympatch.py single /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/concrete
# 2. Build target programs
symutil.py build 19664
# 3. Run target program with concrete input to collect plausible patches
symradar.py filter 19664
# 4. Extract concrete snapshot
symradar.py snapshot 19664 -p high
# 5. Construct abstract snapshot and run symbolic execution
symradar.py run 19664 -p high

1. CPR generated patches are stored in CPR/patches/extractfix/libjpeg/CVE-2018-19664/concrete/uni_klee_runtime_new.c. Use sympatch.py to compile them.
2. You also need to build target programs into LLVM bitcode, which is required for symbolic execution. This can be done by symutil.py build.
3. Before running experiment, you need to identify plausible patches from given patches. symradar.py filter will do the work.
4. Use symradar.py snapshot to extract concrete snapshot from given exploit.
5. Run symradar.py run to execute SymRadar. It first construct abstract snapshot from concrete snapshot, and run symbolic execution.

Expected output (in /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/patched):

patched
|-- djpeg
|-- djpeg.bc
|-- exploit.jpg
|-- filter/
|-- high-0/
|-- snapshot-high/

filter directory contains list of plausible patches in filter/filtered.json. snapshot-high contains a concrete snapshot in (snapshot-high/snapshot-last.json). high-0 is a directory containing experiment results.

3. Analyzing the results

symradar.py analyze 19664 -p high

You can look patched/high-0/table_v3.sbsv file to get experiment result.

[stat] [states] [original 30] [independent 897]
[sym-in] [id 0] [base 32] [test 32] [cnt 3] [patches [11, 56, 119]]
[sym-in] [id 0] [base 30] [test 30] [cnt 3] [patches [11, 56, 119]]
[sym-in] [id 0] [base 47] [test 47] [cnt 3] [patches [11, 56, 119]]
[sym-in] [id 0] [base 45] [test 45] [cnt 3] [patches [11, 56, 119]]
[remain] [crash] [id 0] [base 32] [test 32] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[remain] [crash] [id 0] [base 30] [test 30] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[remain] [crash] [id 0] [base 47] [test 47] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[remain] [crash] [id 0] [base 45] [test 45] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[strict] [id 0] [base 32] [test 32] [cnt 3] [patches [11, 56, 119]]
[strict] [id 0] [base 30] [test 30] [cnt 3] [patches [11, 56, 119]]
[strict] [id 0] [base 47] [test 47] [cnt 3] [patches [11, 56, 119]]
[strict] [id 0] [base 45] [test 45] [cnt 3] [patches [11, 56, 119]]
[strict-remain] [crash] [id 0] [base 32] [test 32] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[strict-remain] [crash] [id 0] [base 30] [test 30] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[strict-remain] [crash] [id 0] [base 47] [test 47] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[strict-remain] [crash] [id 0] [base 45] [test 45] [exit-loc /root/projects/CPR/patches/extractfix/libjpeg/CVE-2018-19664/src/wrbmp.c:561:3:12359] [exit-res ret] [cnt 3] [patches [11, 56, 119]]
[sym-out] [default] [inputs 4] [cnt 3] [patches [11, 56, 119]]
[sym-out] [remove-crash] [inputs 4] [cnt 3] [patches [11, 56, 119]]
[sym-out] [strict] [inputs 4] [cnt 3] [patches [11, 56, 119]]
[sym-out] [strict-remove-crash] [inputs 4] [cnt 3] [patches [11, 56, 119]]
[meta-data] [default] [correct 11] [all-patches 90] [sym-input 4] [is-correct True] [patches [11, 56, 119]]
[meta-data] [remove-crash] [correct 11] [all-patches 90] [sym-input 4] [is-correct True] [patches [11, 56, 119]]
[meta-data] [strict] [correct 11] [all-patches 90] [sym-input 4] [is-correct True] [patches [11, 56, 119]]
[meta-data] [strict-remove-crash] [correct 11] [all-patches 90] [sym-input 4] [is-correct True] [patches [11, 56, 119]]

[meta-data] [remove-crash] [correct 11] [all-patches 90] [sym-input 4] [is-correct True] [patches [11, 56, 119]] This line shows result patches. It means correct patch is 11, a number of total patches is 90, a number of generated symbolic inputs is 4, a result of whether correct patch is included in remaining patches is true, and final remaining patches is 11, 56, 119.

Publication

Seunghoen Han, Youngjae Kim, Yeseung Lee, Jooyong Yi SymRadar: PoC-Centered Bounded Verification for Vulnerability Repair. In Proceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE '26)