3 ms·

Thanks for the explanation! Do people searching for these rely on brute force to find interesting ships, or are there other techniques to designing them? It ce

by paulgb 9y ago

Thanks for the explanation! Do people searching for these rely on brute force to find interesting ships, or are there other techniques to designing them? It certainly doesn't look "designed", but almost organic.

OscarCunningham 9y ago
The ship definitely wasn't "designed", but a SAT solver was used rather than direct brute force and constraints were used to cut down the search space (for example looking for a long-and-thin ship rather than one of arbitrary shape).
- deleted 9y ago
  [deleted]
panic 9y ago
The code used to find this pattern is online if you're curious about the details: https://gitlab.com/apgoucher/metasat/tree/master https://gitlab.com/apgoucher/metasat/tree/master
nneonneo 9y ago
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...

by paulgb 9y ago

OscarCunningham 9y ago

The ship definitely wasn't "designed", but a SAT solver was used rather than direct brute force and constraints were used to cut down the search space (for example looking for a long-and-thin ship rather than one of arbitrary shape).

deleted 9y ago
[deleted]

panic 9y ago

The code used to find this pattern is online if you're curious about the details: https://gitlab.com/apgoucher/metasat/tree/master https://gitlab.com/apgoucher/metasat/tree/master

nneonneo 9y ago

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