In my previous post I've demonstrated a very simple proof of concept of using SMT solvers for detecting opaque predicates in code. This time I'm going to demonstrate how SMT solvers can be used to eliminate dead/junk code.
Opaque predicates are often used for code obfuscation as they are complicating code analysis, especially when it's done statically. An example of an opaque predicate in x86 assembly is a conditional jump which is always continuing execution either at taken or not taken branch - regardless of user input, OS version, etc. The other, never taken branch, usually contains complete junk code or code belonging to some other routine. If we can prove that a conditional jump can be eliminated (either replaced with unconditional jump or completely removed/replaced with NOPs), then we can significantly improve and simplify code analysis.
I've decided to start playing with Z3, a powerful SMT solver developed by Microsoft which, amongst many other things, can also be used for proving the existance of opaque predicates in code.