[klee-dev] Question about seed mode in klee used for concolic execution

[刘松]

Hi

I am trying to run klee with jbig2dec and encountered a problem that is
difficult to solve.  I generate a ktest file as seed, which containing
PoC(Poof of Concept) that can crash the jbig2dec. But it seems that klee
was not following the path given by the seed.

I used *WLLVM* to compile with debug info and *extract-bc* to generate the
bytecode. You can get it using the following command:

$ tar-zxvf jbig2dec-0.13.tar.gz
$ cd jbig2dec-0.13
$ make distclean
$ export LLVM_COMPILER=clang
$ CC=wllvm ./configure --disable-shared CFLAGS='-g'
$ make
$ extract-bc jbig2dec

and used the following command to run klee:

$ klee -libc=uclibc -posix-runtime -seed-out=./poc_fixed2.ktest
-only-replay-seeds jbig2dec.bc --sym-args 2 2 4 A --sym-files 1 792

KLEE: NOTE: Using klee-uclibc : /usr/local/lib/klee/runtime/klee-uclibc.bca
KLEE: NOTE: Using model: /usr/local/lib/klee/runtime/libkleeRuntimePOSIX.bca
KLEE: output directory is
"/home/varas/Public/vancir/jbig2dec-0.13/klee-out-55"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: __isoc99_sscanf
KLEE: KLEE: using 1 seeds

KLEE: 1 seeds remaining over: 1 states
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 59887888) at
/home/varas/Downloads/klee/runtime/POSIX/fd.c:1044
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled.
Using alignment of 8.
KLEE: WARNING: seeds patched for violating constraint
KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: WARNING ONCE: flushing 32768 bytes on read, may be slow and/or crash:
MO53112[32768] allocated at jbig2_default_alloc():  %call = call noalias
i8* @malloc(i64 %0) #4, !dbg !5461
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: ERROR: /home/varas/Public/vancir/jbig2dec-0.13/jbig2.c:36:
concretized symbolic size
KLEE: NOTE: now ignoring this error at this location
KLEE: seeding done (0 states remain)

KLEE: done: total instructions = 3780361
KLEE: done: completed paths = 7
KLEE: done: generated tests = 1

$ cd klee-last
$ ls
assembly.ll  info  messages.txt  run.istats  run.stats  test000001.kquery
test000001.ktest  test000001.model.err  warnings.txt
$

As we can see, klee neither crash the jbig2dec program  nor generate test
case.

Did I run klee in wrong command or are there some details not taken into
account? This problem has been bothering me for a week. I am looking
forward to your solution.

Best Regards
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: poc_fixed2.ktest
Type: application/octet-stream
Size: 1129 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20180723/9b3815c8/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: jbig2dec-0.13.tar.gz
Type: application/gzip
Size: 442571 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20180723/9b3815c8/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: klee-last.tar.gz
Type: application/gzip
Size: 734815 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20180723/9b3815c8/attachment-0001.bin>