4 ms·
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
by tokenrove 12y ago
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 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/ http://research.microsoft.com/en-us/projects/codedigger/
- TheLoneWolfling 12y agoI 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.
- ulber 12y agoMy 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 :)
- rurban 12y agoThen 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.