1. 10

  2. 4

    Author here, happy to answer any questions about working with Manticore or my experience implementing the WASM spec.

    1. 2

      This is all very new to me. How is Manticore related to fuzz testing?

      1. 3

        Symbolic execution and fuzzing are kind of complementary. From https://sites.cs.ucsb.edu/~vigna/publications/2018_SPMag_MechPhish.pdf , PDF page 6:

        Mechanical Phish’s exploitation involves two major steps. The first finds crashes in the target programs. The second step takes those crashes and attempts to figure out how they can be modified to produce exploits that take control of the program.We used AFL, a well-known and highly successful evolutionary fuzzer, as the core of the bug-finding component of our CRS. […] Symbolic execution is a slow but powerful technique for determining the equations that describe the state of the program at any point in execution. To use it efficiently, Driller limits the search space of the symbolic execution to that of the inputs generated by AFL. Specifically, the symbolic execution component will follow each input in AFL’s corpus and check if there are any new locations in the program that it can reach.

        Fuzzing finds crashes, symbolic execution helps turn crashes into provable vulnerabilities.

        1. 2

          This is a great response, I’d also recommend the Driller paper (https://sites.cs.ucsb.edu/~vigna/publications/2016_NDSS_Driller.pdf) as a resource for how symbolic execution and fuzzing can fit together.

      2. 2

        Do you have an instruction limit or memory limit? If so how is it configured?

        1. 1

          Manticore doesn’t impose any built-in constraints on instruction count or memory usage. In fact, it’ll happily gobble up all of your system’s resources if you give it a particularly heavy workload. We usually run Manticore on cloud machines for that reason, but if we need to use it on a shared machine, we use Linux utilities like ulimit and nice to make it a bit less aggressive.