search

moralismercatus / crete

Open source concolic testing tool for binaries
1 stars 1 forks source link

New crete-coverage only supports POSIX file API #134

Closed moralismercatus closed 9 years ago

moralismercatus commented 9 years ago

In fact, all programs that derive from crete::Executor suffer from the same bias.

The problem is that when a file is specified as concolic, two separate test case elements are created. One for stdlibc's file API (fopen, etc.) and one for POSIX API. Since crete-coverage seeks replay the binaries natively, without hooks, these two representations must converge to a single, real file. Presently, there is no way to detect which of the two elements were actually used by the program.

As all current efforts are focused on the POSIX file API, that element is simply chosen.

moralismercatus commented 9 years ago

One possibility is to have the likes of open() and fopen() write maps to file as their hooks are executed (filename -> posix or not?) that can then be sent by crete-run to guest-data on the host and then consumed by crete-coverage and its kin.

There was some discussion about being able to encode this information in the concolic variable name in the test case (as is done with -posix), but I'm not sure if that's feasible.

moralismercatus commented 9 years ago

We've decided to handle the shortcoming by comparing the values of each of the POSIX or stdlibc elements against zero. Whichever is non-zero will be selected, as the default Klee generates for concolic data without constraints is zero. There is a corner-case where the initial input is non-zero, but this should only influence the first test case. So, there's a rare possibility that one test case is mistaken. Willing to live with that for the time being.