Advanced Binary Deobfuscation

Equivalence checking determines if two basic blocks of assembly code are functionally identical. This process follows a two-step hierarchy:

1. Syntax Comparison: A fast check to see if the instruction sequences are identical in structure. If the syntax matches, the blocks are assumed to be semantically equivalent.
2. Semantic Comparison: If syntax differs, the blocks are analyzed using symbolic execution. This involves converting the instructions into Intermediate Representation (IR), executing them symbolically using a SymbolicExecutionEngine, and using a SMT solver (like Z3) to check if any input can produce different outputs (registers or memory) between the two blocks.

To perform this, you can implement a semantic_compare function that utilizes miasm for IR translation and z3 for solving the equivalence constraints.

# High-level logic for equivalence checking
if syntax_compare(blk0, blk1):
    # If syntax matches, semantics are assumed same
    r_semantic = True
else:
    # Otherwise, perform deep semantic analysis
    r_semantic = semantic_compare(blk0, blk1, ir_arch0, ir_arch1, asmcfg)

To explore code paths using symbolic execution, use the SymbolicExecutionEngine in conjunction with a recursive walking function (like codepath_walk) and an SMT solver (like z3) to check path feasibility.

When encountering a conditional branch (ExprCond), you must:

1. Calculate the conditions for both the true and false paths.
2. Determine the destination addresses for both paths using sb.eval_expr and expr_simp.
3. Use check_path_feasibility() to verify if a path is mathematically possible before continuing the walk.
4. If a path is infeasible, record it as a FinalState with result=False.
5. If a path reaches a target address (lbl_stop), record it as a FinalState with result=True.

# Core logic for handling conditional branches in path exploration
if isinstance(pc, ExprCond):
    # 1. Define conditions
    cond_true  = {pc.cond: ExprInt(1, 32)}
    cond_false = {pc.cond: ExprInt(0, 32)}

    # 2. Calculate destination addresses
    addr_true  = expr_simp(sb.eval_expr(pc.replace_expr(cond_true), {}))
    addr_false = expr_simp(sb.eval_expr(pc.replace_expr(cond_false), {}))

    # 3. Accumulate path conditions
    conds_true = list(conds) + list(cond_true.items())
    conds_false = list(conds) + list(cond_false.items())

    # 4. Check feasibility and recurse
    if check_path_feasibility(conds_true):
        codepath_walk(addr_true, sb.symbols.copy(), conds_true, depth + 1, final_states, list(path))
    else:
        final_states.append(FinalState(False, sb, conds_true, path))

    if check_path_feasibility(conds_false):
        codepath_walk(addr_false, sb.symbols.copy(), conds_false, depth + 1, final_states, list(path))
    else:
        final_states.append(FinalState(False, sb, conds_false, path))

You can optimize and simplify binary Intermediate Representation (IR) by combining Constant Propagation (CST) with dead code removal. This process involves loading a binary, generating an IR configuration (ircfg), propagating constant expressions, and iteratively applying dead code removal and empty assignment block removal until the IR stabilizes.

Workflow Steps:

1. Initialize Environment: Create a LocationDB, a Machine instance (e.g., 'x86_32'), and a Container from the binary file.
2. Generate IR: Use the machine's disassembly engine to create an assembly configuration (asmcfg) and convert it into an IR configuration (ircfg) using ir_arch.new_ircfg_from_asmcfg(asmcfg).
3. Constant Propagation: Use propagate_cst_expr to propagate constant expressions through the IR, starting from a set of entry points and initial register states.
4. Iterative Simplification: Use a while loop to repeatedly apply DeadRemoval and remove_empty_assignblks on the ircfg until no further modifications are detected.

from miasm.analysis.machine import Machine
from miasm.analysis.binary import Container
from miasm.analysis.cst_propag import propagate_cst_expr
from miasm.analysis.data_flow import DeadRemoval, remove_empty_assignblks
from miasm.core.locationdb import LocationDB

# Setup
loc_db = LocationDB()
machine = Machine('x86_32')
cont = Container.from_stream(open(filename, 'rb'), loc_db)
mdis = machine.dis_engine(cont.bin_stream, loc_db=cont.loc_db)
ir_arch = machine.ira(mdis.loc_db)

# Generate IR configuration
addr = 0x8048440
asmcfg = mdis.dis_multiblock(addr)
ircfg = ir_arch.new_ircfg_from_asmcfg(asmcfg)

# Propagate constants
entry_points = set([mdis.loc_db.get_offset_location(addr)])
init_infos = ir_arch.arch.regs.regs_init
cst_propag_link = propagate_cst_expr(ir_arch, ircfg, addr, init_infos)

# Iterative Dead Code Removal
deadrm = DeadRemoval(ir_arch)
modified = True
while modified:
    modified = False
    modified |= deadrm(ircfg)
    modified |= remove_empty_assignblks(ircfg)

You can perform symbolic execution to explore different paths in a binary's Control Flow Graph (CFG) using the explore function. This function traverses the IR (Intermediate Representation) starting from a target address, handling conditional branches by evaluating both true and false paths. It uses a SymbolicExecutionEngine to manage symbolic states and path conditions.

Key parameters for explore:

• ir: The IR architecture object.
• start_addr: The entry point address for exploration.
• start_symbols: A dictionary mapping symbolic expressions (like memory or registers) to initial values.
• ircfg: The IR Control Flow Graph object.
• cond_limit: Maximum depth of conditional branches to explore (prevents infinite recursion).
• uncond_limit: Maximum number of unconditional blocks to process.
• lbl_stop: An optional address that, when reached, marks a successful path.
• final_states: A list to collect FinalState objects representing discovered paths.

# Initialize symbols (e.g., setting ESP)
symbols_init = {
    ExprMem(ExprId('ESP_init', 32), 32) : ExprInt(0xdeadbeef, 32)
}

final_states = []

# Run exploration
explore(
    ir_arch, 
    target_addr, 
    symbols_init, 
    ircfg, 
    lbl_stop=0xdeadbeef, 
    final_states=final_states
)

# Iterate through results
for final_state in final_states:
    print('Feasible path:', '->'.join([str(x) for x in final_state.path_history]))
    print('\t', final_state.path_conds)