Diverted state not satisfiable when using strncmp

[andreafioraldi]

Hi, I'm experimenting a bit with driller and I noticed that it fails dramatically when dealing with strncmp.
The diverted state is not satisfiable due to the symbolic length concretization (i think).
You are aware of this for sure and my question is: is there a workaround?

My test program is the following:

int main(int argc, char** argv) {
    char buf[100]; 
    memset(buf, 0, 100);
    read(0, buf, 100);
    fprintf(stderr, "%s\n", buf);
    if(strncmp(buf, "pippo", 5) == 0) {
        //0x4006ea
        if(strncmp((char*)buf +6, "franco", 6) == 0) {
            int i;
            int s = 0;
            for(i = 0; i < 12; ++i)
                s += buf[i];
            if(s == 1217)
                abort();
        }
    }
  return 0;
}

I invoke driller with:

d = driller.Driller("./test1", b"foo")
print(d.drill())

The relevant part of the logs are:

DEBUG   | 2019-02-03 11:05:44,316 | driller.driller | Drilling into b'foo'.
DEBUG   | 2019-02-03 11:05:44,316 | driller.driller | Input is b'foo'.
DEBUG   | 2019-02-03 11:05:44,631 | angr.exploration_techniques.driller_core | Found 0x4004d0 -> 0x4004e0 transition.
DEBUG   | 2019-02-03 11:05:44,631 | angr.exploration_techniques.driller_core | State at 0x4004e0 is not satisfiable even remove preconstraints.
DEBUG   | 2019-02-03 11:05:44,641 | angr.exploration_techniques.driller_core | Found 0x4007c1 -> 0x4007e6 transition.
DEBUG   | 2019-02-03 11:05:44,641 | angr.exploration_techniques.driller_core | State at 0x4007e6 is not satisfiable even remove preconstraints.
DEBUG   | 2019-02-03 11:05:44,669 | angr.exploration_techniques.driller_core | Found 0x4005c0 -> 0x4005df transition.
DEBUG   | 2019-02-03 11:05:44,669 | angr.exploration_techniques.driller_core | State at 0x4005df is not satisfiable even remove preconstraints.
DEBUG   | 2019-02-03 11:05:44,689 | angr.exploration_techniques.driller_core | Found 0x4007dd -> 0x4007d0 transition.
DEBUG   | 2019-02-03 11:05:44,689 | angr.exploration_techniques.driller_core | State at 0x4007d0 is not satisfiable even remove preconstraints.
WARNING | 2019-02-03 11:05:44,817 | angr.state_plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
DEBUG   | 2019-02-03 11:05:44,877 | angr.exploration_techniques.driller_core | Found 0x4006e1 -> 0x4006ea transition.
DEBUG   | 2019-02-03 11:05:44,905 | angr.exploration_techniques.driller_core | State at 0x4006ea is not satisfiable.

The last state is the interesting one but driller fails.
On the other hand setting set_length=False in
s.preconstrainer.preconstrain_file(self.input, s.posix.stdin, True) (in Driller._drill_input) in order to avoid to concretize the length the state is inserted in the diverted stash but the generated input is wrong.

DEBUG   | 2019-02-03 11:26:54,536 | angr.exploration_techniques.driller_core | Found 0x4004d0 -> 0x4004e0 transition.
DEBUG   | 2019-02-03 11:26:54,536 | angr.exploration_techniques.driller_core | State at 0x4004e0 is not satisfiable even remove preconstraints.
DEBUG   | 2019-02-03 11:26:54,546 | angr.exploration_techniques.driller_core | Found 0x4007c1 -> 0x4007e6 transition.
DEBUG   | 2019-02-03 11:26:54,546 | angr.exploration_techniques.driller_core | State at 0x4007e6 is not satisfiable even remove preconstraints.
DEBUG   | 2019-02-03 11:26:54,573 | angr.exploration_techniques.driller_core | Found 0x4005c0 -> 0x4005df transition.
DEBUG   | 2019-02-03 11:26:54,573 | angr.exploration_techniques.driller_core | State at 0x4005df is not satisfiable even remove preconstraints.
DEBUG   | 2019-02-03 11:26:54,592 | angr.exploration_techniques.driller_core | Found 0x4007dd -> 0x4007d0 transition.
DEBUG   | 2019-02-03 11:26:54,592 | angr.exploration_techniques.driller_core | State at 0x4007d0 is not satisfiable even remove preconstraints.
WARNING | 2019-02-03 11:26:55,105 | angr.state_plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
DEBUG   | 2019-02-03 11:26:55,487 | angr.exploration_techniques.driller_core | Found 0x4006e1 -> 0x4006ea transition.
DEBUG   | 2019-02-03 11:26:55,534 | angr.exploration_techniques.driller_core | Found a completely new transition, putting into 'diverted' stash.
DEBUG   | 2019-02-03 11:26:55,534 | driller.driller | Found a diverted state, exploring to some extent.
DEBUG   | 2019-02-03 11:26:55,535 | driller.driller | [test1] dumping input for 0x4006e1 -> 0x4006ea.
DEBUG   | 2019-02-03 11:26:55,535 | driller.driller | Generated: b'70697000000000000000000000000000000000000000000000000000000000000000000000000000000000008080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080806f70'
DEBUG   | 2019-02-03 11:26:55,536 | driller.driller | [test1] started symbolic exploration at Sun Feb  3 11:26:55 2019.
DEBUG   | 2019-02-03 11:26:55,877 | driller.driller | [test1] stopped symbolic exploration at Sun Feb  3 11:26:55 2019.
DEBUG   | 2019-02-03 11:26:55,878 | driller.driller | [test1] dumping input for 0x4000058 -> 0x4000058.
DEBUG   | 2019-02-03 11:26:55,878 | driller.driller | Generated: b'70697000000000000000000000000000000000000000000000000000000000000000000000000000000000008080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808066406f70'
DEBUG   | 2019-02-03 11:26:55,879 | driller.driller | [test1] dumping input for 0x10406c0 -> 0x10406c0.
DEBUG   | 2019-02-03 11:26:55,879 | driller.driller | Generated: b'706970000000000000000000000000000000000000000000000000000000000000000000000000000000000080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080806f636e617266206f70'
DEBUG   | 2019-02-03 11:26:55,880 | driller.driller | [test1] dumping input for 0x4000058 -> 0x4000058.
DEBUG   | 2019-02-03 11:26:55,880 | driller.driller | Generated: b'706970000000000000000000000000000000000000000000000000000000000000000000000000000000000080808080808080808080808080808080808080808080808080808080808080808080808080808080808080808080806f636e617266406f70'

This is interesting because the generated input is almost right but the bytes are in the wrong place.

• how is -> how should be
• pip\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80op -> pippo
• pip\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80f@op -> pippo@f
• pip\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80ocnarf op -> pippo franco
• pip\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80ocnarf@op -> pippo@franco

Another case is when i give an input with size > len("pippo") like "foooooooo" the results are correct also with the regular set_length=True

In this specific case filling with 0 is enough but in general this can alter the behaviour (think about a program that takes different paths using the return value of read) so I'd love to know if there is a more general workaround that you use.

I'm using angr from git (cloned yesterday).

[salls]

I remember we had issues with letting driller generate different sized inputs. However we found AFL would typically generate long enough inputs that worked. For some specific programs we tried extending all inputs from AFL to make sure the inputs were long enough

[andreafioraldi]

So you used a solution like mine but this is not entirely correct.
Thinking about it yesterday i figured out that maybe replacing the read simprocedure will solve this issue.
Look at the following pseudocode:

read(buf, size) {
    nbytes = read_from_stdin(buf, size)
    while(nbytes < size) {
        sym = BVS(8)
        solver.add(read_memory(buf + nbytes, 1) == sym)
        store_memory(buf + nbytes, sym)
        nbytes++
    }
}

This should be an option when extending with 0 is not correct.
When I have some free time I'll try it and maybe I will add an option to the Driller class like "enable_stdin_extension".

[rhelmot]

a word of warning: we've tried a lot of things to do this and none of them work well. my though on the matter is that length preservation is a fundamental limitation of the driller technique without some major reworking.

[salls]

It’s not bad to do both. Run with preserved lengths and without

[andreafioraldi]

Yeah @rhelmot I noticed this when i tried to run driller on a medium sized real-world software. Exteding the input gives me RecursioError when claripy tries to solve the collected constraints.
This is a choice that ultimately depends on the software you are testing.