[klee-dev] Targeting some specific states

[Cristian Cadar]

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
>