[klee-dev] Targeting some specific states

[Sylvain Gault]

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
> >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