Discussion:
Targeting some specific states
(too old to reply)
Sylvain Gault
2014-07-07 17:05:17 UTC
Permalink
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
Cristian Cadar
2014-07-07 18:37:19 UTC
Permalink
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
Post by Sylvain Gault
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Sylvain Gault
2014-07-07 20:28:36 UTC
Permalink
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
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
Post by Sylvain Gault
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Loading...