[JoshTriplett]

https://en.wikipedia.org/wiki/Symbolic_execution

Quite possible. More commonly done with higher-level languages rather than machine code, but certainly possible with machine code. A good fuzzer could do this too.

The fuzzer from the article, american-fuzzy-lop (https://code.google.com/p/american-fuzzy-lop/), does something similar to this as it moves forward in execution, trying to find interesting inputs that cause the program to take a different code path. Symbolic execution could accelerate that process, allowing afl to immediately identify the relevant things to fuzz, rather than randomly mutating and looking for interestingness. On the other hand, unless the program in question runs very slowly, or uses many complex compound instructions before a single conditional branch, random mutation seems likely to produce results rapidly from sheer speed.

Symbolic execution does seem like it would work well if you want to reach a specific point in the program, and you have rather complex conditionals required to get there. But it would still have trouble with complex cases. Consider a file format with a SHA256 hash in it, where the header must have a valid hash to parse. Symbolic execution would have a very hard time figuring out the input relationship required to get past that hash check.

[darkmighty]

Yea I thought of hashes too. Because there are hashes proven (?) to be secure, it follows that it's impossible to make a universally efficient fuzzer (i.e. one that necessarily spends much less than ~exp(parser size) time).

[ynik]

There are no hashes that are proven to be secure. And we aren't likely to get such a proof any time soon: secure hashes can only exist if P != NP.

[userbinator]

But it would still have trouble with complex cases.

It seems to me that all these methods would eventually run into the Halting Problem. Trying to fuzz through a hash (or other crypto) this way would essentially involve having to break it by a slightly more "intelligent" version of bruteforce.

[im2w1l]

I guess one solution could be to give up if the computation becomes too complicated.

>The left side was computed by summing this and this. That was in turn computed by xoring that and... Screw it. The left side can not be controlled. Now, the right side was loaded from this part of the file. Aha! Let's just change that part instead.

[amelius]

I'm no expert but perhaps this symbolic engine could be something to build as a valgrind module.