In the context of a task, I had to analyse an ELF binary. I always wanted to learn more about Miasm and I as such used the opportunity to dig deeper into the tool itself and especially its powerful API. The following blog post outlines the background information and functionality of the patching script, which I wrote to automatically detect and patch out opaque predicates from a given ELF or PE binary.
This is the write-up to the project. For the full code click here.
From their official GitHub Page: Miasm is a free and open source (GPLv2) reverse engineering framework. Miasm aims to analyze / modify / generate binary programs. Here is a non exhaustive list of features:
In computer programming, an opaque predicate is an expression that evaluates to either "true" or "false", for which the outcome is known by the programmer beforehand, but which still needs to be evaluated at run time. Opaque predicates are a commonly used technique in program obfuscation, intended to add complexity to control flow and to insert dummy code or watermarks.
Imagine the following code snipplet.
if ((x * x + x) % 2 == 0) {
// Real code path (always taken)
some_func();
} else {
// Dead code (never reached)
some_other_func();
}
For simplicity's sake we assume that `x` is a variable of an integer type. That being said, trying to insert any number of in that range (in e.g. 0, 1, 2, 3, 4...) will always satfy the expression `(x * x + x) % 2 == 0` and thus execute the first branch of the code. This fact does make the else-branch obsolete, since it will never be executed for that given input (dead code).
First thing to implement was a way to parse a given ELF binary. Miasm does not have, from what I know, a way to read ELF files via its API endpoint. It does however have a function called `virt2off`, which works on PE executables only. To read ELF files I wrote the custom function `virt2off_elf`, which returns the file offset of a given address, passed as an argument. ELF files are divided into ELf-header, the program header(s) and more granuarly into individual sections (like .text, .data) that are then loaded into memory at runtime. Each of these segments has a virtual address and size in memory, plus an offset in the file itself. The script iterates over all those segments to find which one contains the virtual address from the opaque predicate we wish to remove.
def virt2off_elf(v_addr):
elf_file = ELFFile(open(file_path, "rb")) # open elf file using elftools
for seg in elf_file.iter_segments():
# Only consider loadable segments
if seg['p_type'] != 'PT_LOAD':
continue
seg_start = seg['p_vaddr'] # get start of section in virt memory
seg_end = seg_start + seg['p_filesz'] # get end of segment, start + bytes in file
if seg_start <= v_addr < seg_end:
file_off = seg['p_offset'] + (v_addr - seg_start)
# Ensure offset is within file
if file_off >= elf_file.stream.seek(0, 2): # seek from beginning to end of file
print(f"[Error] VA {hex(v_addr)} maps past end of file")
return -1
return file_off
print(f"[Error] VA {hex(v_addr)} not inside any PT_LOAD segment")
return -1
Now having openened the binary the next step is to detect opaque predicates in the file. For this we utilize the z3-solver from Microsoft. Z3 is a satisfiability modulo theories (SMT) solver and is targeted at solving problems that arise in software verification and program analysis. In our case we can use the tool to check which of the conditions in a branch can be satisfied or not. For this we have the function `check_opaque`, which accepts an expression and its targets in Miam's intermediate representation (IR).
def check_opaque(ir_expr, ir_src1, ir_src2):
solver1 = Solver()
solver2 = Solver()
translator = TranslatorZ3()
# Translate Miasm expressions to Z3
expr_z3 = translator.from_expr(ir_expr)
src1_z3 = translator.from_expr(ir_src1)
src2_z3 = translator.from_expr(ir_src2)
# Model the conditional behavior
#sat + unsat --> opaque
#unsat + sat --> opaque
#sat + sat --> impossible
#unsat + unsat --> impossible
solver1.add(expr_z3 == src1_z3)
solver2.add(expr_z3 == src2_z3)
sat1 = solver1.check()
sat2 = solver2.check()
if (sat1 == sat and sat2 == unsat): # always true, jump is taken
return "always_true"
elif (sat1 == unsat and sat2 == sat): # always false, jump is never taken
return "always_false"
else:
return "not opaque" # not an opaque predicate
By checking whether condition A or B of a given expression is reachable, we can determine if we have an always true or always false opaque predicate and act accordingly. The "always true" opaques (jump is always taken) is done by exchanging conditional jump instructions with direct jumps and in the case of "always false" opaques (the jump is never taken) by NOPing out the instruction bytes. First let us look at the `patch_jmp` function out of these two cases. The function takes a given jump instruction, a memory address to be precise, which is of the location referenced by the LocKey in Miasm's LocationDB.
def patch_jmp(jmp_instr):
# machine code instruction sizes x86-64
# depending on arch this may vary
JMP = 1
REL32 = 4
# Convert virtual address to file offset
if isinstance(cont, ContainerPE):
offset = b_stream.virt2off(jmp_instr.offset)
elif isinstance(cont, ContainerELF):
offset = virt2off_elf(jmp_instr.offset)
else:
print("[Error]: Unknown binary type")
return -1
if offset is None or offset < 0:
print(f"[Error]: Virtual adress {hex(jmp_instr.offset)} could not be converted into file offset")
return -1
# Compute relative offset for JMP rel32
# jump displacement is added to the address immediately after the jump instruction (!)
jmp_target = loc_db.get_location_offset(jmp_instr.args[0].loc_key)
rel32 = jmp_target - (jmp_instr.offset + (JMP + REL32)) # position of REL32 offset in new instruction
rel32_bytes = rel32.to_bytes(REL32, byteorder='little', signed=True) # convert integer offset into machine bytecode, rel offset can be negative
# Create JMP instruction bytes
new_instr = b'\xE9' + rel32_bytes # x86 conversion
# Build patch dictionary
for i, b in enumerate(new_instr):
patches[offset + i] = b
# If original instruction was longer than 5 bytes, pad the rest with NOPs
for i in range(len(jmp_instr.b) - len(new_instr)):
patches[offset + len(new_instr) + i] = 0x90 # length of new instruction
return 0
We first check if the binary is of an ELF or PE type, which are the two types the script supports. We then compute the relative offset `rel32` for the x86 instruction `jmp rel32` by subtracting the sum of the jump instruction's offset, the size of the jump and the relative jump location's size. It is to be noted, that all sizes are based on the x86 architecture and may differ on other ones. The result gets converted into byte representation and appended to the opcode of the jump instruction of `e9`. Finally we build a byte dictionary by iterating over the original instruction at `offset` and saving the positions at which we need to make the changes.
Similarly the `patch_nop` function takes a jump instruction as its input, depending on the binary either converts it to the correct PE or ELF offset and keeps track of the offset where it needs to apply the NOP patch via a dictionary.
def patch_nop(jmp_instr): # not raw address, needs .b attribute
# Convert virtual address to file offset
if isinstance(cont, ContainerPE):
offset = b_stream.virt2off(jmp_instr.offset)
elif isinstance(cont, ContainerELF):
offset = virt2off_elf(jmp_instr.offset)
else:
print("[Error]: Unknown binary type")
return -1
if offset is None or offset < 0:
print(f"[Error]: Virtual adress {hex(jmp_instr.offset)} could not be converted into file offset")
return -1
# Patch all bytes of that instruction
for i in range(len(jmp_instr.b)):
patches[offset + i] = 0x90
Finally there are two last things we must consider. Miasm's Symbolic Execution Engine has the power to run through the code of the binary and already predict which branches might be taken and which not (this is overly simplified!). Branches with high probability of not being taken are already going to be patched out by the Symbolic Execution Engine before we even ran our patching script. Thus we have two cases we need to consider in regards to our patching logic:
ipdb> full_expr
ExprCond(ExprOp('CC_EQ', ExprId('zf', 1)), ExprLoc(, 64), ExprLoc(, 64)) # original expression before SB
ipdb> true_addr
4219407 # resolved LocKey 30
ipdb> false_addr
4207352 # resolved LocKey 33
ipdb> stripped_dst
4207352 # destination of the jmp after SB
We can see that the false case of the original condition matches the direct jump address of the simplified expression. Hence we conclude that in this case, the opaque predicate is of the type "always false" and we can patch using the `patch_nop` function.
The patching script will be tested on two separate binaries. Firstly on a simple and manually obfuscated `sum.c` program and secondly on a larger, vastly better obfuscated binary containing a large amount of opaque predicates.
For testing purposes, I added a simple ELF binary containing the following code;
#include
#include
int sum(int a, int b){
return a + b;
}
int main(int argc, char** argv){
if (argc < 3){
fprintf(stderr, "Usage: %s <a> <b>\n", argv[0]);
return 1;
}
int a = atoi(argv[1]);
int b = atoi(argv[2]);
printf("%d + %d = %d\n", a, b, sum(a, b));
return 0;
}
We could obfuscate the resulting binary using tools like the Tigress Obfuscator. I however chose the manual approach, because it was still faster than understanding the way Tigress is supposed to be used (the tool itself is great though!). Using some tricks to avoid `gcc` from removing the opaque predicates, we get the following code.
#include
#include
#define BARRIER() asm volatile("" ::: "memory")
int sum(int a, int b) {
volatile int result = 0;
volatile int va = a;
volatile int vb = b;
/* Opaque predicate: always true */
if ((va ^ va) == 0 && (vb - vb) == 0) {
BARRIER();
/* Opaque predicate: always false */
if ((va + 1) == va) {
BARRIER();
result = 0; /* dead code */
} else {
/* More pointless logic */
int x = va;
int y = vb;
/* Always-true loop condition, executes exactly once */
for (int i = 0; (i * i) == 0; i++) {
BARRIER();
result = x + y;
break;
}
}
} else {
/* Unreachable */
BARRIER();
result = va - vb;
}
/* Another opaque predicate: always true */
if ((result - va) == vb) {
BARRIER();
return result;
} else {
BARRIER();
return va + vb; /* unreachable fallback */
}
}
int main(int argc, char** argv){
if (argc < 3){
fprintf(stderr, "Usage: %s <a> <b>\n", argv[0]);
return 1;
}
int a = atoi(argv[1]);
int b = atoi(argv[2]);
printf("%d + %d = %d\n", a, b, sum(a, b));
return 0;
}
We can compile the code using the `-O0` in `gcc -0O sum_opaques.c -o sum_opaques.out` to ensure that as little optimisation as possible is done to our code.
Analysing both the non-obfuscated and obfuscated binary, we get the following disassembler graph view in binary ninja.
Running the patching script over the obfuscated binary will lead to code more in line with the one from the original `sum.c`.
The control flow graph of the second binary can be seen in the following screenshot of binary ninja. It is a huge graph with tons of opaque predicates.
Running the script over the second sample will give us an even better perspective of the power of the patching script, but especially of Miasm.
For now, the script is limited to x86 binaries due to the use of the hardcoded x86-specific opcodes. Furthermore the script has only been tested on a handful of samples. To ensure correct operability, especially with binaries which also have many nested function calls, the script should be tested on a bigger sample set of binaries. The patching script is free to use and can be improved at your own will!
In the following I will list any issues I came accross when using the script. These issues may arised from the script, the Miasm framework or anything else.
During testing the miasm failed to disassemble a given function passed by argument. This can happen when passing a virtual address which is out of the range of the file's virtual address space. To ensure that the correct virtual address is passed to the program, use a tool like `readelf` to output the address of a symbol (in e.g. function). In my case, binary ninja mapped it into another base address space compared to what I read from the file directly. The function of `sum` was located at 0x00001189 instead of 0x00401189 as in binary ninja. Miasm will look for the OS's mapped memory address.