http://doar-e.github.io/blog/2013/09/16/breaking-kryptonites-obfuscation-with-symbolic-execution/
http://research.microsoft.com/en-us/projects/boogie/
https://github.com/Z3Prover/z3
This is cool because python should be able to hit up all of this. Especially that first link.
I expect this should be nice to have with IDA and your python IDE to go exploring with.
yeah, but z3's bv2int appears broken in some cases. this returns 'unsat' in smt-lib, but 'sat' in z3. in these cases, you might need to invert your logic to use int2bv instead.
ReplyDelete; two 32-bit integers
(declare-const a1 (_ BitVec 32))
(declare-const a2 (_ BitVec 32))
; two integers
(declare-const t1 Int)
(declare-const t2 Int)
; each integer `t should be equiv to the bvints `a
(assert (= t1 (bv2int a1)))
(assert (= t2 (bv2int a2)))
(assert (not (= a1 a2))) ; now suggest that both bvints are not allowed to be the same
(assert (= t1 t2)) ; but allow the integers that they're based on to be the same
; which is bad logic, and shouldn't be possible
(check-sat) ; satisfiable? shouldn't be...
(get-model) ; and why is `t != `a?