The theorem prover cranks for 10 seconds and returns that the formula is unsatisfiable, in other words, that it was not able to generate a counterexample where sequence(1).eax != sequence(2).eax. Assuming the soundness of Z3 with respect to propositional logic over the bitvector and array theories of finite domain, we have just generated a mathematical proof that the sequences have the same effect on the eax register. Z3 can be configured to output the proof explicitly so that it may be checked by other tools.
Equivalence checking for verification of deobfuscation results
I had written a deobfuscation procedure (e.g., a program of the type described here) for a commercial VM ("VM" meaning virtualization obfuscator in this context), and I wanted to know whether my deobfuscation was correct, since I felt like I might've taken some shortcuts along the way. Given access to some obfuscating transformation O, and access to a deobfuscating transformation D, we want to know if D(O(p)) is a semantics-preserving translation for all programs p. We'll settle for random testing: generating a "random" executable according to some guidelines, obfuscating it, deobfuscating it, and comparing (by equivalence checking) the deobfuscated program against the original, pre-obfuscated version. As it turns out, the translation D(O(p)) is not semantics-preserving because VM itself has many bugs that could affect the translation of the original x86 into the VM bytecode.
The procedure in the last paragraph can provide us with straight-line sequences of code (or control flow graphs) such that one is the original, and the other is the obfuscated version with deobfuscation applied. We can then apply equivalence checking to determine whether these sequences are semantically equivalent.
It turns out that they often are not. For example, consider this obfuscated sequence (which has been mostly deobfuscated for the sake of easy illustration):
mov cx, word ptr [esp]
add esp, 2
ror dword ptr ss:[esp], cl
pushfd
And the corresponding deobfuscated sequence:
pop cx
ror dword ptr ss:[esp], cl
pushfd
The former example has a similar effect as the latter one, but it modifies the flags before the rol instruction executes. The rol instruction does not change the flags if cl is zero, therefore, the two sequences are not semantically equivalent if cl = 0. The theorem prover finds this bug, the same bug for ror word ptr and ror byte ptr, and the equivalent bugs for rcr, rcl, rol, shl, shr, and sar. This is a total of 21 buggy VM handlers.
Similarly, obfuscation can also affect the value of the flags register prior to the execution of the inc and dec instructions. Consider this deobfuscated sequence:
pop eax
dec dword ptr ss:[esp]
pushfd
inc and dec do not change the value of the carry flag, but add and sub do. Therefore, obfuscation applied upon the vicinity of the pop eax instruction can destroy the value of the carry flag in these circumstances. As there are three sizes that these instructions might be applied to, there are 6 bugs of this variety.
The theorem prover also found more subtle bugs. Consider the following deobfuscated instruction sequence, where esi points to the VM bytecode.
lodsd dword ptr ds:[esi]
sub eax, ebx
xor eax, 7134B21Ah
add eax, 2564E385h
xor ebx, eax
movzx ax, byte ptr ds:[eax]
push ax
The program's obfuscator would alter the behavior of this snippet by introducing writes to the stack that were not present in the original version, therefore the state of the stack after execution of the obfuscated and non-obfuscated sequences would differ. The memory read on the second-to-last line might therefore target the area below the stack pointer, which would cause it to read a different value in the obfuscated and deobfuscated world. This bug is unlikely to manifest itself in the obfuscation of a real-world program, although it demonstrates the ruthless efficacy of theorem proving towards this problem: the ability to discover tricky situations like this one by considering all possible concrete behaviors of the individual snippets, and generate countermodels for inequal scenarios, no matter how far-fetched.
When taking these factors into consideration, I am able to say that my deobfuscator is correct modulo the bugs in the original obfuscator, which demonstrably number at least 33 (or about 20% of the total handlers).