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.
Here are some simple and common opaque predicates:
xor eax, eax
jno skip
inc eax
skip:
mov ebx, eaxThe snippet from above is using an opaque predicate: jno skip will always be taken because the xor instruction clears the OF flag regardless of the result it computes.
Another case would be the use of junk operations on known values:
mov eax, 1
mov ebx, 2
add eax, ebx
cmp eax, 4
je skip
inc eax
skip:
mov ebx, eaxThis piece of code always computes 1 + 2 and compares the result to 4 which, obviously, will never be true and thus the je skip jump will never be taken.
Z3 is capable of proving whether an expression is true based on multiple constraints we specify. In order to use this ability for testing opaque predicates, we are going to translate x86 code into a set of constraints and ask Z3 to prove that a condition tested by a conditional jump can be proven to be a constant (e.g. OF == FALSE or OF == TRUE). If we are trying to prove that OF == FALSE and Z3 finds a case when OF == TRUE, we are going to ask it once again - this time to prove that OF == TRUE. If it finds a case when OF == FALSE, it means that the conditional jump is not an opaque predicate - otherwise it is.
Considering this is nothing more than a proof of concept, please keep in mind several things:
I am going to use capstone-engine for disassembly.
void disassemble_data(const uint8_t* data, size_t data_len, cs_insn** instructions, size_t* count)
{
csh csh;
if (cs_open(CS_ARCH_X86, CS_MODE_32, &csh) == CS_ERR_OK)
{
if (cs_option(csh, CS_OPT_DETAIL, CS_OPT_ON) == CS_ERR_OK)
{
*count = cs_disasm(csh, data, data_len, 0, 0, instructions);
}
else
throw std::exception("could not configure capstone");
}
else
throw std::exception("cs_open() failed");
}
void disassemble_input(const char* input_file, cs_insn** instructions, size_t* count)
{
*count = 0;
std::ifstream input_stream(input_file, std::ios::binary);
if (input_stream)
{
input_stream.seekg(0, std::ios::end);
size_t input_size = static_cast<size_t>(input_stream.tellg());
if (input_size)
{
boost::scoped_array<uint8_t> data(new uint8_t[input_size]);
input_stream.seekg(std::ios::beg);
if (input_stream.read(reinterpret_cast<char*>(data.get()), input_size))
{
disassemble_data(data.get(), input_size, instructions, count);
}
else
throw std::exception("could not read from input file");
}
else
throw std::exception("input file is empty");
}
else
throw std::exception("could not open input file");
}The disassemble_input function is going to read a binary file and disassemble the raw bytes found inside, returning disassembled instructions.
After getting the disassembled instructions, we will locate the first occurrence of a conditional jump. Instructions prior to the conditional jump will be used to build Z3 expressions which will be added as constraints.
struct x86_ctx
{
z3::expr* eax;
z3::expr* ebx;
z3::expr* ecx;
z3::expr* edx;
z3::expr* esi;
z3::expr* edi;
z3::expr* ebp;
z3::expr* of;
z3::expr* zf;
z3::expr* sf;
}For the purpose of this post a minimal x86 register set is implemented. Operations on registers which are not 32bits wide are not supported. The EFLAGS register has been split into multiple boolean values indicating the flag state.
Every disassembled instruction is going to be represented by the above state. The first instruction will be assigned registers and flags with unspecified values - assuming that anything can be input to the basic block:
void create_initial_state(z3::context& z3c, x86_ctx& ctx)
{
ctx.eax = new z3::expr(z3c.bv_const("init_eax", 32));
ctx.ebx = new z3::expr(z3c.bv_const("init_ebx", 32));
ctx.ecx = new z3::expr(z3c.bv_const("init_ecx", 32));
ctx.edx = new z3::expr(z3c.bv_const("init_edx", 32));
ctx.esi = new z3::expr(z3c.bv_const("init_esi", 32));
ctx.edi = new z3::expr(z3c.bv_const("init_edi", 32));
ctx.ebp = new z3::expr(z3c.bv_const("init_ebp", 32));
ctx.of = new z3::expr(z3c.bool_const("init_of"));
ctx.zf = new z3::expr(z3c.bool_const("init_zf"));
ctx.sf = new z3::expr(z3c.bool_const("init_sf"));
}During translation of a disassembled instruction, we are going to create a new x86 state. Registers which are overwritten will be assigned expressions based on the state of the previous instruction (or initial state when translating the first instruction). The unmodified registers will have the state copied from the previous instruction.
For example, this is a minimal example of XOR translation:
void translate_xor(z3::context& z3c, const cs_insn& ins, x86_ctx& old_state, x86_ctx& new_state)
{
auto& x86 = ins.detail->x86;
if (x86.op_count == 2)
{
auto& op1 = x86.operands[0];
auto& op2 = x86.operands[1];
z3::expr& e1 = **get_val_expr(z3c, old_state, op1);
z3::expr& e2 = **get_val_expr(z3c, old_state, op2);
z3::expr** dst = get_val_expr(z3c, new_state, op1);
*dst = new z3::expr(z3c, e1 ^ e2);
new_state.of = new z3::expr(z3c.bool_val(false));
new_state.zf = new z3::expr(**dst == 0);
new_state.sf = new z3::expr(**dst < 0);
}
else
throw std::exception("bad operand count");
}get_val_expr is a helper function which returns a pointer to a pointer to a variable/value expression - allowing easy fetching of registers for constructing expressions simulating x86 instructions and assigning the constructed expressions to a new x86 state. It's not very elegant, in fact it's ugly as hell, but it's simple enough for a quick proof of concept.
After the basic block has been translated into a series of Z3 expressions, we have to translate the conditional jump into a constraint and tell Z3 to perform the magic:
opaque_predicate_t test_condition(z3::context& z3c, x86_ctx& state, cs_insn& jcc)
{
z3::expr* cc;
z3::solver s1(z3c);
z3::solver s2(z3c);
switch (jcc.id)
{
case X86_INS_JO:
cc = new z3::expr(**get_flag_expr(state, FLAG_OF));
break;
case X86_INS_JNO:
cc = new z3::expr(!**get_flag_expr(state, FLAG_OF));
break;
case X86_INS_JE:
cc = new z3::expr(**get_flag_expr(state, FLAG_ZF));
break;
case X86_INS_JNE:
cc = new z3::expr(!**get_flag_expr(state, FLAG_ZF));
break;
case X86_INS_JS:
cc = new z3::expr(**get_flag_expr(state, FLAG_SF));
break;
case X86_INS_JNS:
cc = new z3::expr(!**get_flag_expr(state, FLAG_SF));
break;
case X86_INS_JL:
cc = new z3::expr(**get_flag_expr(state, FLAG_SF) != **get_flag_expr(state, FLAG_OF));
break;
case X86_INS_JLE:
cc = new z3::expr(**get_flag_expr(state, FLAG_ZF)
|| **get_flag_expr(state, FLAG_SF) != **get_flag_expr(state, FLAG_OF));
break;
default:
throw std::exception("bad jcc");
}
s1.add(*cc);
s2.add(!(*cc));
if (s1.check() == z3::unsat) return opaque_predicate_not_taken_k;
if (s2.check() == z3::unsat) return opaque_predicate_taken_k;
return not_opaque_predicate_k;
}>test_opaque_predicate.exe test1.bin
disassembled 4 instructions
> xor eax, eax
> jo 5
> inc eax
> mov ebx, eax
2. instruction is conditional
> testing: jo 5
opaque predicate: never taken>test_opaque_predicate.exe test2.bin
disassembled 4 instructions
> xor eax, eax
> je 5
> inc eax
> mov ebx, eax
2. instruction is conditional
> testing: je 5
opaque predicate: always taken>test_opaque_predicate.exe test3.bin
disassembled 4 instructions
> xor eax, ebx
> je 5
> inc eax
> mov ebx, eax
2. instruction is conditional
> testing: je 5
not an opaque predicate>test_opaque_predicate.exe test4.bin
disassembled 8 instructions
> and eax, 0x3fffffff
> and ebx, 0x3fffffff
> xor ecx, edx
> xor edx, edi
> add eax, ebx
> jo 0x14
> inc eax
> mov ebx, eax
6. instruction is conditional
> testing: jo 0x14
opaque predicate: never taken>test_opaque_predicate.exe test5.bin
disassembled 8 instructions
> and eax, 0x3fffffff
> and ebx, 0x3fffffff
> xor ecx, edx
> xor edx, edi
> xor eax, ebx
> je 0x14
> inc eax
> mov ebx, eax
6. instruction is conditional
> testing: je 0x14
not an opaque predicateDOWNLOAD: test_opaque_predicate.cpp