3 ms·

The discoverer developed a program called ikpx (https://gitlab.com/apgoucher/metasat/blob/master/ikpx.py https://gitlab.com/apgoucher/metasat/blob/master/ikpx.p

The discoverer developed a program called ikpx (https://gitlab.com/apgoucher/metasat/blob/master/ikpx.py https://gitlab.com/apgoucher/metasat/blob/master/ikpx.py), part of his larger "MetaSAT" project, which poses the problem of finding an oblique glider as a set of SAT constraints. Additional heuristic constraints were added to limit the search space. ikpx passes the resulting ball of constraints to a SAT solver, which does the computational work of attempting to find a satisfying solution. 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.

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 ago
  Take 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...

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 ago
Take 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...