13 ms·
>It's a clever approach as modern SAT solvers are surprisingly powerful. I actually use this approach myself in some of my (personal) work, e.g. to automaticall
by ChickeNES 9y ago
>It's a clever approach as modern SAT solvers are surprisingly powerful. I actually use this approach myself in some of my (personal) work, e.g. to automatically find execution paths through a target binary for reverse-engineering purposes.
I'm interested in the latter, do you have any readings/blogposts/books you would recommend?
- nneonneo 9y agoTake a look at Angr (http://angr.io/ http://angr.io/), which implements symbolic execution + SMT solving to analyze program execution (not my work, although I know a number of the authors). SAT/SMT solving can be quite handy for assisting fuzzers in selecting good paths, which is something I've investigated in the past. Angr can help with that too, although the most recent developments in practical fuzzing have been in coverage-testing approaches (like afl) rather than in symbolic execution approaches. I also play CTFs a fair bit, and in those we sometimes use Z3 and Boolector (two numerically-oriented SMT solvers) to solve challenges. As an example: https://github.com/pwning/public-writeup/tree/master/9447ctf2015/re330-nobranch https://github.com/pwning/public-writeup/tree/master/9447ctf...