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.

Various websites have slightly different definitions of dead code, this article targets garbage instructions which are executed, but have no effect on the final result. Sometimes unreachable code is also called dead code, however this is not a subject of this article. Below are some examples of what's being targeted.

mov eax, 1
mov eax, 2
add eax, ebx

The mov eax, 1 instruction assigns a value, however it is never used and mov eax, 2 instruction is going to override its effects. In this case mov eax, 1 is a garbage instruction and can safely be eliminated.

mov eax, 0x1918632
shr eax, 0x10
add eax, 0x913
and eax, 0x1fff
mov ecx, eax
mov ecx, 0x10000
mov eax, 0x1918632
and ecx, 0x600
mov ecx, 0x800
or ecx, ecx
jne jump_target

This is one type of garbage code used by Themida. The conditional jump on the end is an opaque predicate which can easily be handled as shown in the previous post. As for the other instructions, most can be completely removed. Only two reigsters are used so this looks like a perfect minimal example of the logic we want to apply automatically. We are going to disregard previously described opaque predicates for now, let's just remove instructions which have no effect on the final x86 state of this particular basic block:

• we're going to leave jne as it's a conditional end of the basic block
• or ecx, ecx is going to overwrite all flags which are modified by previous instructions
• eax will have value 0x1918632
• ecx will have value 0x800

That leaves us with:

mov eax, 0x1918632
mov ecx, 0x800
or ecx, ecx
jne jump_target

For the simplicity of the proof of concept, we are going to focus on the state of a single basic block. Therefore, although this is an obvious opaque predicate, we are not going to replace it with an uncoditional jump because the code at jump_target may be using the expected EFLAGS which will be computed by or ecx, ecx. In reality it doesn't, but multi-basic-block optimization is out of the scope of this post - keep in mind that this is nothing more than a simple demonstration of code deobfuscation using SMT solvers, more complex examples will be handled in the future posts.

Stack instructions and memory operand translations are not implemented, they're a completely separate topic and will be demonstrated in another post. Translations from x86 into Z3 expressions are only partially implemented (e.g. some EFLAGS are not computed at all).

The idea

Just like in the previous post, we are going to analyze a single basic block. The code at the end of the basic block is assumed to expect the exact x86 state (both register and flag state) as when all instructions are executed. If we eliminate an instruction and we can prove that the x86 state on the end of the basic block is 100% identical, we can safely remove such instruction. There are cases when two or more instructions are garbage code, but can be proven only when they're removed all at once - such cases are also out of the scope of this post.

Testing a single instruction

void translate_instructions(z3::context& z3c, x86_ctx& state, instruction_list_t& instructions, instruction_list_t::iterator skip)
{
    for (instruction_list_t::iterator iter = instructions.begin(); iter != instructions.end(); ++iter)
    {
        if (iter != skip)
        {
            translate_instruction(z3c, **iter, state);
        }
    }
}

bool can_eliminate_instruction(instruction_list_t& instructions, instruction_list_t::iterator instruction)
{
    x86_ctx     base;
    z3::context c;

    create_initial_state(c, base);

    x86_ctx orig = base;
    x86_ctx opt  = base;

    translate_instructions(c, orig, instructions, instructions.end());
    translate_instructions(c, opt, instructions, instruction);

    z3::solver s(c);

    s.add(!(*orig.eax == *opt.eax && *orig.ebx == *opt.ebx && *orig.ecx == *opt.ecx
        && *orig.edx == *opt.edx && *orig.esi == *opt.esi && *orig.edi == *opt.edi
        && *orig.ebp == *opt.ebp && *orig.of == *opt.of && *orig.zf == *opt.zf
        && *orig.sf == *opt.sf));

    return (s.check() == z3::unsat);
}

The logic is quite simple: create a representation of initial x86 state - base variable. Create copies of the state representing the unmodified code and code without the instruction being tested - orig and opt variables. Ask Z3 to prove that the variables computed in both states will have the same values.

Examples

>eliminate_dead_code.exe test1.bin
disassembled 3 instructions
 > mov eax, 1
 > mov eax, 2
 > add eax, ebx
Removing: mov eax, 1
after dead code elimination: 2 ins
 > mov eax, 2
 > add eax, ebx

>eliminate_dead_code.exe test2.bin
disassembled 10 instructions
 > mov eax, 0x1918632
 > shr eax, 0x10
 > add eax, 0x913
 > and eax, 0x1fff
 > mov ecx, eax
 > mov ecx, 0x10000
 > mov eax, 0x1918632
 > and ecx, 0x600
 > mov ecx, 0x800
 > or ecx, ecx
Removing: mov eax, 0x1918632
Removing: shr eax, 0x10
Removing: add eax, 0x913
Removing: and eax, 0x1fff
Removing: mov ecx, eax
Removing: mov ecx, 0x10000
Removing: and ecx, 0x600
after dead code elimination: 3 instructions
 > mov eax, 0x1918632
 > mov ecx, 0x800
 > or ecx, ecx

>eliminate_dead_code.exe test3.bin
disassembled 5 instructions
 > sub edx, eax
 > add eax, 1
 > cmp edx, 5
 > and ecx, ebx
 > xor edx, edx
Removing: sub edx, eax
Removing: cmp edx, 5
after dead code elimination: 3 instructions
 > add eax, 1
 > and ecx, ebx
 > xor edx, edx

>eliminate_dead_code.exe test4.bin
disassembled 6 instructions
 > sub edx, eax
 > add eax, 1
 > cmp edx, 5
 > mov ebx, edx
 > and ecx, ebx
 > xor edx, edx
Removing: cmp edx, 5
after dead code elimination: 5 instructions
 > sub edx, eax
 > add eax, 1
 > mov ebx, edx
 > and ecx, ebx
 > xor edx, edx

DOWNLOAD: dead_code_elimination.cpp

Next Post Previous Post