Hacker News Reader

One of my favorite uses is concolic testing which has really been enabled by SMT solvers (of which Z3 is one of the best): http://en.wikipedia.org/wiki/Concolic_testing

Check out MS's Code Digger, which uses Z3 as well: http://research.microsoft.com/en-us/projects/codedigger/

View on HN

I wonder if that could be implemented as an extension to AFL.

I.e. mutate random values for a while, then use an SMT solver to try to find any remaining code paths that haven't been followed by AFL.

I have a feeling AFL would be faster for "simple" paths, but an SMT solver may be handy for getting those last few paths.

My experience with concolic testing has been that single path satisfiability queries tend to be quite cheap and it's actually a bit challenging to write the tooling around the solver in such a way that the solver would actually become the bottleneck. This is not to say that combinations of concolic testing with other testing methods is not an interesting research topic :)

Then rather use cmbc, which does exactly that. It translates C code into SMT rules, allows assertions on symbolic variables and solves them. And note that for harder crypto problems Z3 is not the best, it's just the easiest to use.

Reply on news.ycombinator.com