Re:The Z3 theorem prover is now open source
by tptacek on Wednesday October 03, 2012 @08:08AM
(#4606944)
Solvers are somewhat popular in software security, both for automatically uncovering invariants (and exploitable lack of invariants), and also for modeling program binaries and solving for collections of basic blocks that can executed during a memory corruption attack to accomplish attacker goals.
[ Parent
| on HN ]
Re:The Z3 theorem prover is now open source
by krenoten on Wednesday October 03, 2012 @08:19AM
(#4606977)
Things like automatic exploit generation[1] and exploit hardening[2] in particular rely on SMT solvers to accomplish their goals. They allow for some truly remarkable things to be done. Expect skynet to utilize them heavily in its distributed automatic exploit generation (global autopwn) tooling!
1. http://security.ece.cmu.edu/aeg/ 2. http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2011_rop-abs...