Sylvain Gault
2014-07-07 17:05:17 UTC
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
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