search

evanmak / savior-source

source code for savior fuzzer
Apache License 2.0
126 stars 27 forks source link

Wrong values within Klee testcases #9

Closed cponcelets closed 4 years ago

cponcelets commented 4 years ago

Dear SAVIOR team,

I am doing a simple example for SAVIOR and figured out a strange behavior from Klee. You can find the example attached to this post. It includes a Makefile generating the instrumented binaries and the configuration.

The idea is simple, I want a file starting with the "POTS_LFA" magic number (having the hex value 41464c5f53544f50) as you can see below:

#echo "POTS_LFA" > test.in
#cat test.in
POTS_LFA
#./savior-example < test.in
read 41464c5f53544f50 compared against 41464c5f53544f50
Magic number passed

However, this is the result I have when I try a testcase klee generated to solve the magic number constraint:

./savior-example < output_folder/klee_instance_conc_000001/queue/id\:000002
read 41464c5f53544faf compared against 41464c5f53544f50

Note that in this case the printf is before the check at line 14. The reason I pushed it after into the attached code is to prevent from disturbing klee.

As you can see, the problem is that the last byte is wrong, the sequence is "AFL_STO¯" hence the check is not passed.

More surprising, Klee is actually working if I remove --concolic-explorer=true from the list of options. I show you the commands I executed:

#/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=/root/work/example-folder/.afl_coverage_combination --klee-covered-branchid-outfile=/root/work/example-folder/output_folder/.tmp_se_0.cov --edge-sanitizer-heuristic --seed-out-dir=/root/work/example-folder/klee_new_input/klee_instance_conc_1 --sync-dir=/root/work/example-folder/output_folder/klee_instance_conc_000001/queue /root/work/example-folder/savior-example.dma.bc --sym-stdin 27

#cat output_folder/klee_instance_conc_000001/queue/id\:000002
�OTS_LFA0 &?!�

Without --concolic-explorer=true (and with fresh folders created to store the testcases):

#/root/work/savior/KLEE/klee-build/bin/klee --libc=uclibc --disable-inject-ctor-and-dtor=true --posix-runtime --named-seed-mat-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=/root/work/example-folder/.afl_coverage_combination --klee-covered-branchid-outfile=/root/work/example-folder/output_folder/.tmp_se_0.cov --edge-sanitizer-heuristic --seed-out-dir=/root/work/example-folder/klee_new_input/klee_instance_conc_4 --sync-dir=/root/work/example-folder/output_folder/klee_instance_conc_000004/queue /root/work/example-folder/savior-example.dma.bc --sym-stdin 27

#cat /root/work/example-folder/output_folder/klee_instance_conc_000004/queue/id:000001
POTS_LFAAAAAAAAAAAAAAAAAAAA

I am using the Dockerfile, which has clang version 3.6.0 and KLEE 1.4.0.0. Except this detail, SAVIOR seems to work normally.

Best example.tar.gz

evanmak commented 4 years ago

Hi,

The cmd looks correct. What is the initial input you provide to KLEE when concolic mode is enabled?

In addition, can you please list all the files under output_folder/klee_instance_conc_000001/queue and check their content?

cponcelets commented 4 years ago

Hi @evanmak, thank you for your quick answer.

The input file is created within the Makefile, I should have done a different script for that. It is created in seed_folder and contains a\n from the command:

mkdir -p "seed_folder" && echo "a" > seed_folder/seed1.txt

For SAVIOR, there is actually only one more empty file (output_folder/klee_instance_conc_000001/queue/id\:000001).

Here is the complete list:

# ls output_folder/klee_instance_conc_000001/queue/
id:000001  id:000002
# cat output_folder/klee_instance_conc_000001/queue/id:000001
# cat output_folder/klee_instance_conc_000001/queue/id:000002
�OTS_LFA0 &?!�
evanmak commented 4 years ago

interesting, it should've forked the state for the if true branch in your test program, maybe it is the -remove-unprioritized-states flag, can you remove it and set --free-mode=true?

cponcelets commented 4 years ago

Yes, with this command one more file is printed containing the good values. Here is the command and the testcases generated:

# /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 --free-mode=true --fixup-afl-ids=true --relax-constraint-solving=false --savior-ubsan=false --max-memory=0 --max-time-per-seed=150 --afl-covered-branchid-file=/root/work/example-folder/.afl_coverage_combination --klee-covered-branchid-outfile=/root/work/example-folder/output_folder/.tmp_se_0.cov --edge-sanitizer-heuristic --seed-out-dir=/root/work/example-folder/klee_new_input/klee_instance_conc_5 --sync-dir=/root/work/example-folder/output_folder/klee_instance_conc_000005/queue /root/work/example-folder/savior-example.dma.bc --sym-stdin 27

# ls output_folder/klee_instance_conc_000005/queue/
id:000001  id:000002  id:000003
# cat output_folder/klee_instance_conc_000005/queue/id\:000001
# cat output_folder/klee_instance_conc_000005/queue/id\:000002
�OTS_LFA0 &?!�
# cat output_folder/klee_instance_conc_000005/queue/id\:000003
POTS_LFA0 &?!�
evanmak commented 4 years ago

Does free_mode=true mean that the concolic execution is disabled?

No, it is still concolic, only branches along the path will be forked.

Should I change the way SAVIOR is calling klee?

It depends, since solver is sometimes the bottleneck of SymExec, savior uses an optimization internally, which is to skip solving for a branch/state when it is not "prioritized". In this case, since savior only cares about the UBSAN instrumentation, we deem those instrumented branches "prioritized". This way, savior can scale better.

So, if the program you are fuzzing is small and do not have scaling issue, feel free to enable free_mode, which means just solve for every branch.

cponcelets commented 4 years ago

I see, thank you for the information. It would be great to set this option when starting moriarty or in the configuration file.

evanmak commented 4 years ago

actually you can set it under the [klee conc_explorer] section: https://github.com/evanmak/savior-source/blob/9633ede3eee25febd88dfd039665f77cffd8c330/coordinator/SEs/klee_conc_explorer.py#L37

cponcelets commented 4 years ago

Thank you I missed this configuration field.

I also checked by adding an underflow in the true branch and indeed the concolic engine prints one more testcase. Here is the output of the same commands with example.c.tar.gz:

# ls output_folder/klee_instance_conc_000001/queue/
id:000001  id:000002  id:000003

# cat output_folder/klee_instance_conc_000001/queue/id\:000001
# cat output_folder/klee_instance_conc_000001/queue/id\:000002
POTS_LFAIIIII IIIIIIIIIIIIIIIIIYIIIII�
# cat output_folder/klee_instance_conc_000001/queue/id\:000003
�OTS_LFAIIIII IIIIIIIIIIIIIIIIIYIIIII�

Thank you again for your answers. Best