4 ms·

Funny Klee [1] wasn't mentioned. [1]: https://github.com/klee/klee https://github.com/klee/klee

• nickpsecurity 9y ago
  I recommend people look through their whole publication list here: http://klee.github.io/publications/ http://klee.github.io/publications/ That group does some amazing work bridging neat theories and putting things into practice. I wish more researchers would build on KLEE to see just how much more it could accomplish. That is, on top of more developers using tools like it.
• touisteur 9y ago
  Or cbmc (some interesting papers : http://www.cprover.org/cbmc/applications/ http://www.cprover.org/cbmc/applications/), they're on GitHub : https://github.com/diffblue/cbmc https://github.com/diffblue/cbmc), seems to also handle java, not sure... Or angr (http://angr.io http://angr.io) which works on binaries and is in python and is loads of fun to use... On small codebases ? Still some people have used it in combination with AFL to help the fuzzer when it's stuck ('driller' : https://github.com/shellphish/driller https://github.com/shellphish/driller) Or manticore (you'll need IDA Pro there ?) : https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/ https://blog.trailofbits.com/2017/04/27/manticore-symbolic-e... There's a good survey there : https://arxiv.org/abs/1610.00502 https://arxiv.org/abs/1610.00502 (no cbmc though). But nickpsecurity is right, Klee seems to be the place where most of the interesting stuff seems to be happening right now. The recent improvements in SMT/SAT solvers bring back lots of techs that were thought impractical (formal proof, symbolic execution...) a while back.