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

[Sang Phan]

Hi,

The PoC was also generated by KLEE, is it right?
args       : ['jbig2dec.bc', '--sym-args', '2', '2', '4', 'A',
'--sym-files', '1', '792']

So you ran KLEE without seed to find a test case that crashed the
program. Then run KLEE with this test case as seed? is that correct?

In the klee-last folder, there is a new test case test000001.ktest.
What is the problem with it?


Sang



On Mon, Jul 23, 2018 at 4:30 AM, 刘松 <vancirprince at gmail.com> wrote:
> 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
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>