extra conditions in fuzzball?

[christop...@gmail.com]

Hi, I'm trying to add conditions to constrain the fuzzball's search, and it seems like the -extra-condition flag is the right way to do that. But I can't figure out the syntax for anything but numeric constants. For registers, temps and symbolic variables the parser complains about undeclared variables, and for variable declarations it complains about "var". Does anyone have any examples of how to do this?
thanks

  -cc

[Stephen McCamant]

>>>>> "CC" == christophcmichael <christop...@gmail.com> writes:

CC> Hi, I'm trying to add conditions to constrain the fuzzball's
CC> search, and it seems like the -extra-condition flag is the right
CC> way to do that. But I can't figure out the syntax for anything but
CC> numeric constants. For registers, temps and symbolic variables the
CC> parser complains about undeclared variables, and for variable
CC> declarations it complains about "var". Does anyone have any
CC> examples of how to do this? thanks

I think there might be a couple of pitfalls you're running into here.

First, the kind of variables it makes sense to have in an
-extra-condition are symbolic input variables. The argument to
-extra-condition is a mathematical condition of the sort that goes in
the path condition, so it has to always have the same meaning. The
contents of registers change over time, and -extra-condition doesn't
have any way of specifying at what point in time the condition should
be evaluated, so it wouldn't be sensible to put a variable
representing a machine register in the condition.

Second, the symbolic input variables that it currently works to put
into an -extra-condition are restricted by some implementation details
of FuzzBALL. We try to parse the extra-condition condition at the time
we switch into symbolic mode for the first time. So it will only work
with symbolic variables that are also introduced at that early stage
(the relevant code is the function make_symbolic_init in
execution/exec_set_options.ml). Some options introduce their symbolic
variables later, which is too late for the -extra-condition parsing to
succeed.

My first impulse was to demonstrate -extra-condition using the
"examples/simplie-func" example from the README file, but in fact
-skip-call-ret-symbol is an example of a symbolic-input-introducing
option that currently doesn't work with -extra-condition, because the
symbolic variable isn't introduced until the call instruction is
encountered in the program.

So instead it might be useful to demonstrate another relatively easy
way of introducing symbolic inputs into a program you control, which
is to make global variables that you initialize by address. Here's a
variant of simple.c I'll call simple-global.c:

#include <stdio.h>
#include <stdlib.h>
int the_input;
int simple(int x) {
int path = 0;
if (x & 1) {
printf("x is odd\n");
path++;
} else {
printf("x is even\n");
}
path <<= 1;
if (x % 11 == 0) {
printf("x is a multiple of 11\n");
path++;
} else {
printf("x is not a multiple of 11\n");
}
printf("Took path %d\n", path);
}
int main(int argc, char **argv) {
int input;
if (argc == 1) {
input = the_input;
} else if (argc == 2) {
input = atoi(argv[1]);
} else {
fprintf(stderr, "Usage: simple [<integer>]\n");
exit(-1);
}
simple(input + 10);
return 0;
}

Notice that the code doesn't write to "the_input", but if you run the
program without command-line arguments it will take the input from
that global variable. Normally the kernel (or FuzzBALL simulating the
kernel) would initialize the memory to zero, but you can make it
symbolic with -symbolic-word ("word" = 32-bit value in FuzzBALL). You
need to know the address of the global, which you can get with "nm":

% nm simple-global | fgrep the_input
0804a038 B the_input

This kind of symbolic variable works as expected with
-extra-condition. For instance here's how you can require that the
input be even:

% fuzzball -linux-syscalls -symbolic-word 0x0804a038=n \
-trace-stopping simple-global \
-extra-condition '(n:reg32_t & 0x1:reg32_t) == 0:reg32_t' -- \
./simple-global
x is even
x is a multiple of 11
Took path 1
Stopping when program called exit() at 0xb7f01010
x is even
x is not a multiple of 11
Took path 0
Stopping when program called exit() at 0xb7f01010

You see that of the four execution paths that are possible when n is
unconstrained, only two are possible when it is required to be even.

I can see why it might be confusing that not all of these options work
conveniently together. Perhaps the above example will be enough to get
you starting doing what you'd like to do, or perhaps you could
describe more about your use case to think about whether it motivates
enhancements or new features that would be more broadly useful.

One possibility that occurs to me would be to create a new option that
combines some of the features of -extra-condition and
-check-condition-at. As I mentioned before -extra-condition takes a
condition over symbolic inputs which will be required to be true at
all times. The use of "condition" is a little bit different in
-check-condition-at, which takes a condition expressed in terms of
machine state (registers and memory, rather than symbolic variables)
and a program location specified by an instruction address. Every time
that condition is reached, we evaluate the machine state condition
into a symbolic expression condition, and then check whether that
condition (or its negation) are satisfiable. We could take ideas from
both of these options to create something that might be called
-extra-condition-at, which could take a machine-state condition
instead of a symbolic expression condition. It would take a code
location, and every time that code location was hit, we could create a
new extra condition based on the evaluation of the machine-state
condition at that point.

Hope this helps,

-- Stephen

[christop...@gmail.com]

Hi, thanks for the reply. When I said I couln't get symbolic variables to parse I was
in fact defining the variable with skip-call-ret-symbol.

What I'm trying to achieve is to make fuzzball check the feasibility of a series of abstract states.
I can check symbolically, but since the states are abstract I can't create a single set of concrete
inputs that would allow me to verify the symbolic computation by just tracing the code. Originally
I was also thinking that doing my own symbolic check would only duplicate functionality that was
already in fuzzball, and maybe I could make fuzzball do it for me.

From what you said, and from playing around in fuzzball, it sounds like the best approach is to go
ahead and compute path conditions in terms of input variables, since something like
extra-condition-at would make fuzzball explore all the way to the state where the condition was defined
before realizing that it was infeasible. But in order to specify constraints on the input variables I have to
make -extra-condition work with skip-call-ret-symbol. I haven't tried it but it sounds like -extra-condition
also won't work with symbolic values supplied by fuzzball for uninitialized memory locations. Implementing
that sounds like basically the same problem as implementing extra-condition-at.

I added a partial implemention of this in eip_hook in sym_path_frag_machine, where I basically just did
the same thing that extra-condition does, namely adding my condition to path_cond and pushing it to the query
engine. Does that make sense, or am I just mucking with internal data and making fuzzball hallucinate that it's
doing what I want?

[Stephen McCamant]

>>>>> "CCM" == christophcmichael <christop...@gmail.com> writes:

CCM> Hi, thanks for the reply. When I said I couln't get symbolic
CCM> variables to parse I was in fact defining the variable with
CCM> skip-call-ret-symbol.

OK. Would it be sufficient in your context to use
-skip-call-ret-symbol-once, because the introduction of the variable
occurs only once on each execution path? I think that would be a
relatively easier case for adding -extra-condition support, since
there would just be one variable we could create at the time the
option was parsed instead of when it was first hit. The version
without -once is more complex because it creates an unbounded family
of variables if the call is encountered repeatedly. I believe right
now it just uses numeric suffixes on the variable names, but to allow
them all to be parsed maybe it should be an array instead.

CCM> What I'm trying to achieve is to make fuzzball check the
CCM> feasibility of a series of abstract states. I can check
CCM> symbolically, but since the states are abstract I can't create a
CCM> single set of concrete inputs that would allow me to verify the
CCM> symbolic computation by just tracing the code. Originally I was
CCM> also thinking that doing my own symbolic check would only
CCM> duplicate functionality that was already in fuzzball, and maybe I
CCM> could make fuzzball do it for me.

I'm not completely clear on what you mean by an "abstract state" in
this context, but what you're saying generally seems to make sense to
me.

CCM> From what you said, and from playing around in fuzzball, it
CCM> sounds like the best approach is to go ahead and compute path
CCM> conditions in terms of input variables, since something like
CCM> extra-condition-at would make fuzzball explore all the way to the
CCM> state where the condition was defined before realizing that it
CCM> was infeasible. But in order to specify constraints on the input
CCM> variables I have to make -extra-condition work with
CCM> skip-call-ret-symbol.

CCM> I haven't tried it but it sounds like -extra-condition also won't
CCM> work with symbolic values supplied by fuzzball for uninitialized
CCM> memory locations. Implementing that sounds like basically the
CCM> same problem as implementing extra-condition-at.

Actually I think this might be worth trying. During symbolic
execution, the symbolic variables for uninitialized memory locations I
believe just look like indexing into a "mem" memory variable, which I
think might be the same variable that we use for accesses to memory in
code. (This collision of names is probably a bit confusing. The
separation is clearer for registers, where for instance R_EAX is the
mutable variable that represents %eax, while initial_eax is the
symbolic variable that holds the input value in the register if
-symbolic-regs is supplied. For instance if the code has R_EAX = R_EAX
+ 1 followed by R_EAX = R_EAX * 2, you'll reach a state in which R_EAX
contains "2*initial_eax + 2".) Or it might be that this doesn't work
now, but one could make it work just by adding "mem" to the
declaration list used when parsing the extra condition.

CCM> I added a partial implemention of this in eip_hook in
CCM> sym_path_frag_machine, where I basically just did the same thing
CCM> that extra-condition does, namely adding my condition to
CCM> path_cond and pushing it to the query engine. Does that make
CCM> sense, or am I just mucking with internal data and making
CCM> fuzzball hallucinate that it's doing what I want?

It might work, though I think this is the kind of situation where you
need to be careful whether your expressions contain the correct
variables, versus similarly named variables that the tool will
consider distinct. That's the reason we want to declare the variables
before parsing them in -extra-condition, to be sure we're getting the
right ones. FuzzBALL generally keeps variables separate based on an
internal unique numeric identifier, and you can think of the name as
being a comment. So if -skip-call-ret-symbol mentions "x", and you
create a new variable "x" in your extra condition, you might see that
in the solver input one of them is x_42 and the other is x_179. In
that case the formula is syntactically legal but doesn't represent the
constraint you want.

-- Stephen