1. 5

This is a quick intro to SMT (specifically Z3) and its application to exploitation. I’m pretty interested in Eclipser, which we even use a bit at work, and things like MACKE, AEG, &c. However, this article is a pretty great intro to the basics, and I figured I’d share here as well.

  1.  

  2. 4

    Also, when large XORs are involved, cryptominisat can shine where Z3’s SAT backend chokes (due to the exponentially-sized representation of XOR in CNF).

    We’re working on getting CMS as an alternate SAT backend to Z3 to get the best of both worlds.

    1. 1

      Oh that would be great; we’ve had some interesting challenges with Z3 as well, mostly for very large proofs (someone internally posted the other day that they were using 43GB of memory for Z3 for some symbolic execution…).

    2. 4

      Important note on this story: since the article was written, RetDec added support for 64-bit decompilation on x86 and ARM, in case you want to use KLEE but don’t have the cash to shell out for Hex-Rays

      1. 1

        We also have McSema and Remill to help with lifting, and are working quite a bit on KLEE, esp. KLEE-native to help there as well. RetDec is pretty nice as well, there’s some interesting use cases for it.