This is very interesting. I wasn't aware of directed symbolic execution (I'm a newbie in that field), it sounds exactly like what I need. I'm going to read the main paper about KATCH and come back at you later.
So, in the end, the only goal of KLEE is to generate inputs covering *all* paths of a program? Sylvain Gault On Mon, Jul 07, 2014 at 07:37:19PM +0100, Cristian Cadar wrote: > Hi Sylvain, if you'd like to drive exploration toward a specific part of the > program (e.g., the klee_assert(0) in your example), you might want to take a > look at our work on KATCH: http://srg.doc.ic.ac.uk/projects/katch. If you'd > like to try the actual system, just email Paul and me directly. > > Best, > Cristian > > On 07/07/14 18:05, Sylvain Gault wrote: > >Hello everyone, > > > >I was wonder if klee was the right tool for my needs. Actually, most of > >my needs boil down to bringing the program into a specific state. Like a > >winning condition in a game or an exploitable condition for a bug (like > >AEG does). > > > >I could use klee_asserti(0) to mark the condition and make klee search > >for an assert failure (like the maze tutorial). But this kind of goal > >(bringing a program into a given state) could also be used to cut down > >state-space explosion because a lot of path aren't even worth looking > >for. Take a look at the following program that is basically an automaton > >checking a password. > > > >const char pass[] = "LeAmazingPassword"; > >void checkpass(void) { > > int i = 0; > > > > while (pass[i] != '\0') { > > int c; > > klee_make_symbolic(&c, sizeof(c), "c"); > > if (c == pass[i]) > > i++; > > else > > i = 0; > > } > > > > klee_assert(0); > >} > > > >It obviously has an infinite number of path. But only the paths that > >get out of the loop are interesting (there is also an infinite number of > >them). > > > >This example is trivial, I could easily put a klee_assume(c == pass[i]) > >but this would remove the whole point of using klee. This example could > >also work with state merging (which I couldn't make work in klee). > > > >I guess that what I'm looking for is some kind of backward or mixed > >chaining. Or some kind of analysis about the path to follow that would > >eliminate the exploration of some paths. > > > >iIs there any way to do this with klee? If klee is not the right tool > >for me, maybe you know some other tools better suited for my needs? > > > > > >Thanks in advance. > >Best regards, > > > >Sylvain Gault > > > >_______________________________________________ > >klee-dev mailing list > >[email protected] > >https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
