Concolic Execution engine component in savior
2 tools are specially creatd for savior
-converter
-klee
this tool convert between concrete inputs and klee ktest files
- convert binary to ktest
converter --mode=a2k --afl-name=inputs/id_000000 --ktest-name=000001.ktest --bitmodel=64 --inputmode=symfile
- convert ktest back to binary
converter --mode=k2a --afl-name=id_000000 --ktest-name=input.ktest --bitmodel=64 --inputmode=symfile
-take a look at an example command generated by savior
/root/work/savior/KLEE/klee-build/bin/klee --libc=uclibc --disable-inject-ctor-and-dtor=true --posix-runtime --concolic-explorer=true --named-seed-matching=true --allow-external-sym-calls --use-non-intrinsics-memops=false --check-overshift=false --solver-backend=z3 --max-solver-time=5 --disable-bound-check=true --disable-ubsan-check=true -remove-unprioritized-states --free-mode=false --fixup-afl-ids=true --relax-constraint-solving=false --savior-ubsan=false --max-memory=0 --max-time-per-seed=150 --afl-covered-branchid-file=../tests/tcpdump/obj-savior/.afl_coverage_combination --klee-covered-branchid-outfile=../tests/tcpdump/obj-savior//out/.tmp_se_0.cov --edge-sanitizer-heuristic --seed-out-dir=../tests/tcpdump/obj-savior//klee_new_input/klee_instance_conc_1 --sync-dir=../tests/tcpdump/obj-savior//out/klee_instance_conc_000001/queue ../tests/tcpdump/obj-savior//savior-tcpdump.dma.bc -evnnnr A --sym-files 1 1376
here we explain a few options introduced by savior
*concolic mode
--concolic-explorer, requires --named-seed-matching
*disable checks
--disable-bound-check and --disable-ubsan-check
Sometimes the replayed path itself will trigger a UBSAN bug, but KLEE will abort the initial state desipte in reality the execution may continue without problem. This is to be consistent with UBSAN alert behavior.
*single seed replay mode
klee --libc=uclibc --posix-runtime --concolic-explorer=true --solver-backend=z3 --seed-out=tests/tcpdump/seed_ktests/000000.ktest --sync-dir=./out savior-tcpdump.dma.bc -evnnnr A --sym-files 1 1376
*"fork server" batch replay mode
klee --libc=uclibc --posix-runtime --concolic-explorer=true --seed-out-dir=tests/tcpdump/seed_ktests --sync-dir=./sync_dir savior-tcpdump.dma.bc -evnnnr A --sym-files 1 1376
In fork-server mode, the file size is just a place holder, internally, klee will automatically adjust the size to reflect the biggest size among all the input seeds.
Other advantages are:
-
Skipping the lengthy initialization process such as bitcode linking.
-
The klee/solver caches are available for the following seeds.
*state filtering
-remove-unprioritized-states
If set, state that explpored new edge will be mark with privileged 2, state that explore new sanitizer handler edge will be mark wit priviledge 3, and the rest of the states will be marked as not-interesting. KLEE will skip the uninteresting states when consulting solver to solver the state conditions.
--free-mode
If set, ignore other state filtering flags, freely generate inputs correspond to all the states.
*timeouts
--max-time-per-seed=X
In fork-server mode, each seed gets X seconds quota. This is to prevent when there is a seed requires significant amount of time to explore and block other seeds from being executed.
*afl infomation
--afl-covered-branchid-file
the file records what edge id has been covered by AFL so far, KLEE will mark them as uninteresting branches.
*klee infomation
--klee-covered-branchid-outfile
KLEE output this file to indicate what branches have been explored by KLEE during this round of execution. It can be used by coordinator for prioritizing inputs.
*state scheduler
--edge-sanitizer-heuristic
KLEE's state scheduler will schedule states that explore sanitizer instrumentation edges with priority and invoke solvers to solve such states first.
*optimistic solving
--relax-constraint-solving
If the constraint solving fails, KLEE will remove the constraints one by one in reverse order and try to solve again.
*output directory
--sync-dir
KLEE will output the synthesized inputs to the specified directory