[klee-dev] Guided Search - Help
Alberto Barbaro
barbaro.alberto at gmail.com
Sat Oct 20 11:30:00 BST 2018
Hi Andrew,
Thanks a lot. I understand now, so it would follow all the paths because
the input is symbolic.
In my mind I would like to have a searcher that would follow only and only
one path with symbolic data. This path should be generated with a concrete
file. This is I'm working on a searcher but I cannot do it properly for now.
Thanks
On Sat, Oct 20, 2018, 09:58 Andrew Santosa <asantosa1999 at gmail.com> wrote:
> Hi Alberto,
>
> Please keep in mind that, although KLEE still tries to follow the seed's
> path, the state it maintains is no longer
> the concrete state, but the symbolic state. So, the symbolic file A no
> longer contains a concrete RGB value at coordinate
> (1, 1), but instead a symbolic value. By looking at the log you sent,
> especially the following lines, this symbolic value could
> have been concretized by KLEE into a value you were not expecting.
>
> KLEE: WARNING ONCE: silently concretizing (reason: floating point)
> expression (Select w32 (Slt 4294967295
> N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8
> 55 A-data))
> 16)
> (Shl w32 (ZExt w32 (Read w8
> 54 A-data))
> 24))
> (Shl w32 (ZExt w32 (Read w8 56
> A-data))
> 8))
> (ZExt w32 (Read w8 57 A-data))))
> N0
> 4294967295) to value 541597261
> (/home/klee/target/libpng-1.6.35/png.c:3371)
>
> Best,
> Andrew
> On Saturday, 20 October 2018, 1:51:56 AM GMT+8, Alberto Barbaro <
> barbaro.alberto at gmail.com> wrote:
>
>
> Hi all,
> I think we are getting there but I'm still missing something. So I was
> able to generate pngpixel.bc and successfully use it. My next step was to
> generate the seed an I used the following command:
>
> gen-bout --sym-file ../images/png-files-download.png && mv file.bout
> png-files-download.bout
>
> Now, as suggested, I have used that seed with klee:
>
> klee at a8a6399e6799:~/seeds$ time klee -only-seed
> -seed-out=png-files-download.bout -only-replay-seeds --posix-runtime
> -libc=uclibc ../target/libpng-1.6.35/contrib/examples/pngpixel.bc 1 1 A
> --sym-files 1 89760
> KLEE: NOTE: Using klee-uclibc :
> /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca
> KLEE: NOTE: Using POSIX model:
> /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca
> KLEE: output directory is
> "/home/klee/seeds/../target/libpng-1.6.35/contrib/examples/klee-out-41"
> KLEE: Using STP solver backend
> KLEE: WARNING: undefined reference to function: floor
> KLEE: WARNING: undefined reference to function: modf
> KLEE: WARNING: undefined reference to function: pow
> KLEE: KLEE: using 1 seeds
>
> KLEE: 1 seeds remaining over: 1 states
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 147249744) at
> /home/klee/klee-gen-bout/runtime/POSIX/fd.c:980
> 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 ONCE: ioctl: (TCGETS) symbolic file, incomplete model
> KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash:
> MO504[8192] allocated at global:crc_table
> KLEE: 1 seeds remaining over: 1 states
> KLEE: 1 seeds remaining over: 1 states
> KLEE: WARNING ONCE: silently concretizing (reason: floating point)
> expression (Select w32 (Slt 4294967295
> N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8
> 55 A-data))
> 16)
> (Shl w32 (ZExt w32 (Read w8
> 54 A-data))
> 24))
> (Shl w32 (ZExt w32 (Read w8 56
> A-data))
> 8))
> (ZExt w32 (Read w8 57 A-data))))
> N0
> 4294967295) to value 541597261
> (/home/klee/target/libpng-1.6.35/png.c:3371)
> KLEE: WARNING: seeds patched for violating constraint
> KLEE: WARNING ONCE: calling external: floor(4621195801218788662) at
> /home/klee/target/libpng-1.6.35/png.c:3375
> KLEE: 1 seeds remaining over: 1 states
> KLEE: WARNING ONCE: calling external: vprintf(146758144, 154438432) at
> /home/klee/klee_build/klee-uclibc/libc/stdio/fprintf.c:35
>
> libpng warning: ����: gamma value does not match sRGB
>
> From my initial understanding now klee should follow only one path but i
> feel that is not the case because at this point the input is symbolic so it
> would follow all the paths.. I'm a bit confused at the moment.
>
> Just to clarify, the expect output should be:
>
> klee at a8a6399e6799:~/seeds$
> ../target/libpng-1.6.35/contrib/examples/pngpixel 1 1
> ../images/png-files-download.png
> RGBA 255 255 255 255
> klee at a8a6399e6799:~/seeds$
>
> What am I missing? :)
>
> Thanks for your help!
>
> Alberto
>
> Il giorno mar 16 ott 2018 alle ore 14:27 Alberto Barbaro <
> barbaro.alberto at gmail.com> ha scritto:
>
> Thanks I'll try that one later :)
>
> On Tue, Oct 16, 2018, 14:08 Sang Phan <phanquocsang at gmail.com> wrote:
>
> You need to pass -allow-seed-extension (or -allow-seed-truncation) when
> the seed is shorter (or longer) than the symbolic file
>
> On Tue, Oct 16, 2018 at 12:38 AM Alberto Barbaro <
> barbaro.alberto at gmail.com> wrote:
>
> Hi Andrew and Sang,
> Thanks a lot for your explanation. I tried and I think we are getting
> there.
>
> @Andrew: so as you suggested I tried klee -seed-out=file.bout first.bc
> -only-seed A -sym-files 1 10. Now klee is complaining about the different
> file size. When I generated the file.bout of course the file was just 1
> byte, now I would like to use a symbolic file. Can you suggest me how to
> solve my problem please?
>
> @Sang: I'll have a look and try to use it and get back to you.
>
> Once I solved this problem I'll try to create a PR so next time should be
> easier for all of us.
>
> Thanks again
>
>
> On Tue, Oct 16, 2018, 00:50 Sang Phan <phanquocsang at gmail.com> wrote:
>
> Hi Alberto,
>
> What you described is called concolic execution (
> https://en.wikipedia.org/wiki/Concolic_testing)
> So the easiest way is to use an existing concolic execution engine, and
> you will have what you want out-of-the-box.
>
> KLEE had a concolic execution engine, called ZESTI, but it is no longer
> supported. You may want to try Crete, it is based on KLEE, but maintained
> by a different group.
> https://github.com/SVL-PSU/crete-dev
> I have not checked it.
>
> KLEE can be run with (concrete) seeds, and when there is only one seed, it
> is somewhat similar to concolic execution. But you need to:
> + tell KLEE that you only want to run seed (-only-seed) and you only want
> to replay seeds (-only-replay-seeds), and
> + re-start KLEE for each run of each seed.
>
> Cheers,
> Sang
>
> On Sun, Oct 14, 2018 at 5:25 AM Alberto Barbaro <barbaro.alberto at gmail.com>
> wrote:
>
> Hi all,
> I have already asked this in the past and received few suggestions but I
> was not able to do it. I'm trying to test pngpixel[1] that takes as input
> an image file. My goal is to execute pngpixel with a real file and
> subsequently execute pngpixel with a symbolic file and follow the path
> followed by the first execution.I would like to describe my approach so
> before spending to much time on it and I can understand if I'm doing it
> right or not :)
>
> 1 - Execute pngpixel enabling -debug-print-instructions=src:file
> 2 - Inside my searcher create a map from instruction.txt so I know which
> is the next instruction
> 3 - Inside the update() function for my searcher, get the current
> instruction, get the next instruction,
> 4 - Check for each state in addedStates if the next instruction would be
> execute at the next step in the state
> 5 - If yes add the state using state.push_back(state) else remove the
> state ( adding the state to removedStates? )
>
> I'm sure this flow is not optimized but at least is it correct? How would
> you approach this problem?
>
> Thanks for your time
> Alberto
>
> [1]
> https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list