### Setup Development Environment for Deobfuscation

Source: https://context7.com/malrev/abd/llms.txt

A bash script to initialize the development environment by installing necessary dependencies including Miasm, Z3, Obfuscator-LLVM, and Tigress on Ubuntu 18.04.

```bash
#!/bin/bash
# Run the setup script from the repository root
./setup.sh ./

# This installs:
# - Obfuscator-LLVM (code obfuscation compiler)
# - Miasm (reverse engineering framework)
# - Z3 SMT solver
# - Jupyter Notebook
# - Docker and Tigress obfuscator
```

--------------------------------

### Define Binary File and Entry Point (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on2/optimizer.ipynb

Specifies the path to the binary file to be analyzed and the starting address for disassembly.

```python
filename = '../hands-on1/test-add-sub.bin'
addr = 0x8048440
```

--------------------------------

### Miasm Symbolic Execution Setup

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Initializes necessary components for symbolic execution with Miasm, including machine architecture, symbolic execution engine, and expression types. It imports various modules from Miasm and other libraries like z3 and future.

```python
# -*- coding: utf-8 -*-
from miasm.analysis.machine import Machine
from miasm.arch.x86.arch import mn_x86
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.expression.expression import ExprCond, ExprId, ExprInt, ExprMem 
from miasm.expression.simplifications import expr_simp
from miasm.arch.x86.regs import *
from miasm.core import parse_asm, asmblock
from miasm.core.locationdb import LocationDB
from miasm.analysis.binary import Container
from future.utils import viewitems
from miasm.loader.strpatchwork import *
from miasm.ir.translators.translator import Translator
import warnings
import z3

```

--------------------------------

### Initialize Miasm and Disassemble Code (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on2/optimizer.ipynb

Initializes the Miasm environment, loads the binary file into a container, disassembles the code starting from a given address, and generates an intermediate representation (IR) control flow graph (CFG). It then prints the IR blocks before simplification.

```python
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)

asmcfg = mdis.dis_multiblock(addr)
ircfg = ir_arch.new_ircfg_from_asmcfg(asmcfg)

print('Before Simplification:')
for lbl, irb in viewitems(ircfg.blocks):
    print(irb)
```

--------------------------------

### Initialize Miasm Analysis Environment (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore_smt.ipynb

Sets up the necessary imports and environment for Miasm-based analysis, including machine architecture, symbolic execution engine, and expression handling.

```python
# -*- coding: utf-8 -*-
from miasm.analysis.machine import Machine
from miasm.arch.x86.arch import mn_x86
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.expression.expression import ExprCond, ExprId, ExprInt, ExprMem 
from miasm.expression.simplifications import expr_simp
from miasm.arch.x86.regs import *
from miasm.core import parse_asm, asmblock
from miasm.core.locationdb import LocationDB
from miasm.analysis.binary import Container
from future.utils import viewitems
from miasm.loader.strpatchwork import *
from miasm.ir.translators.translator import Translator
import warnings
import z3
```

--------------------------------

### Initialize ZeusVM Analysis Environment in Python

Source: https://context7.com/malrev/abd/llms.txt

Imports necessary Miasm modules for analyzing a virtual machine binary, specifically 'zeusvm.bin'. This setup includes components for machine emulation, binary container handling, expression manipulation, and symbolic execution, preparing for deeper analysis of VM-based obfuscation techniques.

```python
# -*- coding: utf-8 -*-
from miasm.analysis.machine import Machine
from miasm.analysis.binary import Container
from miasm.expression.expression import *
from miasm.core.utils import upck32
from miasm.core.locationdb import LocationDB
from miasm.arch.x86 import regs
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.expression.simplifications import expr_simp

filename = 'zeusvm.bin'


```

--------------------------------

### Execute Symbolic Exploration with Miasm

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Initiates the symbolic execution process using the previously defined `explore` function. It passes the intermediate representation, starting address, initial symbols, and configuration parameters.

```python
explore(ir_arch, 
        0, 
        symbols_init, 
        ircfg, 
        lbl_stop=0xdeadbeef, 
        final_states=final_states)

```

--------------------------------

### Import Miasm Analysis Modules (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on2/optimizer.ipynb

Imports necessary modules from the Miasm library for binary analysis, including machine definition, container handling, constant propagation, data flow analysis, and location database management.

```python
# -*- coding: utf-8 -*-
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, merge_blocks, remove_empty_assignblks
from miasm.core.locationdb import LocationDB
from future.utils import viewitems
```

--------------------------------

### Initialize Symbolic State for Miasm

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Sets up the initial symbolic state for the execution engine. This includes defining initial values for memory locations (like ESP) and registers based on the architecture.

```python
symbols_init =  {
    ExprMem(ExprId('ESP_init', 32), 32) : ExprInt(0xdeadbeef, 32)
}

for i, r in enumerate(all_regs_ids):
    symbols_init[r] = all_regs_ids_init[i]

final_states = []

```

--------------------------------

### Configure Symbolic Execution State

Source: https://github.com/malrev/abd/blob/master/hands-on5/solved/zeus_get_ir.ipynb

Initializes register and memory symbols, including stack setup and immediate value tracking, for symbolic execution.

```python
symbols_init = dict(regs.regs_init)
initial_symbols = symbols_init.items()
ret_addr = ExprId('RET_ADDR', 32)
vm_pc_init = ExprId('VM_PC_init', 32)
infos = {}
infos[expr_simp(ExprMem(regs.ECX_init, 32))] = vm_pc_init
infos[expr_simp(ExprMem(regs.ESP_init-ExprInt(4, 32), 32))] = ret_addr
infos[regs.ESP] = expr_simp(regs.ESP_init-ExprInt(4, 32))
for i in range(0, 5):
    infos[expr_simp(ExprMem(regs.ECX_init + ExprInt(4*(i+1), 32), 32))] = ExprId('REG%d' % i, 32)
addition_infos = dict(infos)
expr_imm8 = expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 8))
addition_infos[expr_imm8] = ExprId('imm8' , 8)
expr_imm16 = expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 16))
addition_infos[expr_imm16] = ExprId('imm16' , 16)
expr_imm32 = expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 32))
addition_infos[expr_imm32] = ExprId('imm32' , 32)
```

--------------------------------

### Check Path Feasibility using Z3 Solver (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore_smt.ipynb

Determines if a given set of path conditions is satisfiable using the Z3 SMT solver. It converts Miasm expressions to Z3 format and checks for satisfiability.

```python
def check_path_feasibility(conds):
    solver = z3.Solver()
    for lval, rval in conds:
        z3_cond = Translator.to_language("z3").from_expr(lval)
        solver.add(z3_cond == int(rval.arg))

    rslt = solver.check()

    if rslt == z3.sat:
        return True
    else:
        return False
```

--------------------------------

### Display and Validate Path Analysis Results

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore_smt.ipynb

Iterates through a list of final states to print path history, feasibility status, and path conditions. It concludes by performing assertions to verify the expected number of total, feasible, and infeasible paths.

```python
print('final states:', len(final_states))

for final_state in final_states:
    if final_state.result:
        print('Feasible path:','->'.join([str(x) for x in final_state.path_history]))
        print('\t',final_state.path_conds)
    else:
        print('Infeasible path:','->'.join([str(x) for x in final_state.path_history]))
        print('\t',final_state.path_conds)

    final_state.sb.dump(ids=False)
    print('')
    
assert len(final_states) == 2, '# of Final States is incorrect'
assert len([x for x in final_states if x.result == True]) == 1, '# of feasible is incorrect'
assert len([x for x in final_states if x.result == False]) == 1, '# of infeasible is incorrect'

print('Congrats!')
```

--------------------------------

### Simplify IR Control Flow Graph (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on2/optimizer.ipynb

Applies simplification passes to the IR CFG, including constant propagation and dead code removal. The process iterates until no further modifications are made. Finally, it prints the IR blocks after simplification.

```python
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)
deadrm = DeadRemoval(ir_arch)

modified = True
while modified:
    modified = False
    modified |= deadrm(ircfg)
    modified |= remove_empty_assignblks(ircfg)

print('After Simplification:')

for lbl, irb in viewitems(ircfg.blocks):
    print(irb)
```

--------------------------------

### Display Miasm Symbolic Execution Results

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Prints the results of the symbolic execution, iterating through the collected `final_states`. For each state, it shows whether the path was feasible, the path history, the path conditions, and dumps the final symbolic state.

```python
# Show results
print('final states:', len(final_states))

for final_state in final_states:
    if final_state.result:
        print('Feasible path:','->'.join([str(x) for x in final_state.path_history]))
        print('\t',final_state.path_conds)
    else:
        print('Infeasible path:','->'.join([str(x) for x in final_state.path_history]))
        print('\t',final_state.path_conds)

    final_state.sb.dump(ids=False)
    print('')

```

--------------------------------

### Miasm Symbolic Execution Path Exploration

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Implements the `explore` function for symbolic execution, which recursively walks through code paths. It handles conditional branches, limits recursion depth, and collects final states. Dependencies include `SymbolicExecutionEngine`, `ExprCond`, `ExprInt`, and `expr_simp`.

```python
def explore(ir, start_addr, start_symbols, 
        ircfg, cond_limit=30, uncond_limit=100, 
        lbl_stop=None, final_states=[]):

    def codepath_walk(addr, symbols, conds, depth, final_states, path):

        if depth >= cond_limit:
            warnings.warn("'depth' is over the cond_limit :%d"%(depth))
            return 

        sb = SymbolicExecutionEngine(ir, symbols)

        for _ in range(uncond_limit):

            if isinstance(addr, ExprInt):
                if addr == lbl_stop:
                    final_states.append(FinalState(True, sb, conds, path))
                    return

            path.append(addr)

            pc = sb.run_block_at(ircfg, addr)

            if isinstance(pc, ExprCond): 
    
                # Calc the condition to take true or false paths
                cond_true  = {pc.cond: ExprInt(1, 32)}
                cond_false = {pc.cond: ExprInt(0, 32)}

                # The destination addr of the true or false paths
                addr_true  = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_true), {}))

                addr_false = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_false), {}))

                # Need to add the path conditions to reach this point
                conds_true = list(conds) + list(cond_true.items())
                conds_false = list(conds) + list(cond_false.items())

                # Recursive call for the true or false path
                codepath_walk(
                        addr_true, sb.symbols.copy(), 
                        conds_true, depth + 1, final_states, list(path))

                codepath_walk(
                        addr_false, sb.symbols.copy(), 
                        conds_false, depth + 1, final_states, list(path))

                return
            else:
                addr = expr_simp(sb.eval_expr(pc))

        final_states.append(FinalState(True, sb, conds, path))
        return 

    return codepath_walk(start_addr, start_symbols, [], 0, final_states, [])

```

--------------------------------

### Recursive Code Path Exploration with Symbolic Execution (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore_smt.ipynb

Explores possible code paths using symbolic execution. It handles conditional branches, limits recursion depth, and utilizes the Z3 solver for path feasibility checks. The function recursively calls itself for different execution paths.

```python
def explore(ir, start_addr, start_symbols, 
        ircfg, cond_limit=30, uncond_limit=100, 
        lbl_stop=None, final_states=[]):

    def codepath_walk(addr, symbols, conds, depth, final_states, path):

        if depth >= cond_limit:
            warnings.warn("'depth' is over the cond_limit :%d"%(depth))
            return 

        sb = SymbolicExecutionEngine(ir, symbols)

        for _ in range(uncond_limit):

            if isinstance(addr, ExprInt):
                if addr == lbl_stop:
                    final_states.append(FinalState(True, sb, conds, path))
                    return

            path.append(addr)

            pc = sb.run_block_at(ircfg, addr)

            if isinstance(pc, ExprCond):
    
                # Calc the condition to take true or false paths
                cond_true  = {pc.cond: ExprInt(1, 32)}
                cond_false = {pc.cond: ExprInt(0, 32)}

                # The destination addr of the true or false paths
                addr_true  = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_true), {}))

                addr_false = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_false), {}))

                # Need to add the path conditions to reach this point
                conds_true = list(conds) + list(cond_true.items())
                conds_false = list(conds) + list(cond_false.items())

                # TODO:
                # Please add some code to complete the SMT-based path explore
                # Hint1: use check_path_feasibility()
                # Hint2: Do not forget to add the current state to the final_states 
                # when the path condition is infeasible. 
                # e.g., final_states.append(FinalState(False, sb, conds_true/conds_false, path))
                #
                # From here --------------------------------
                
                codepath_walk(
                        addr_true, sb.symbols.copy(), 
                        conds_true, depth + 1, final_states, list(path))

                codepath_walk(
                        addr_false, sb.symbols.copy(), 
                        conds_false, depth + 1, final_states, list(path))

                # To here --------------------------------

                return
            else:
                addr = expr_simp(sb.eval_expr(pc))

        final_states.append(FinalState(True, sb, conds, path))
        return 

    return codepath_walk(start_addr, start_symbols, [], 0, final_states, [])
```

--------------------------------

### Assemble x86 Code with Miasm

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Parses and assembles x86 assembly code into an abstract control flow graph (ACFG) using Miasm. It utilizes `parse_asm.parse_txt` and `LocationDB` to manage symbol locations and code structure.

```python
# Assemble code
loc_db = LocationDB()
asmcfg = parse_asm.parse_txt(mn_x86, 32, ''' 
main:
    PUSH EBP
    MOV EBP, ESP
    MOV ECX, 0x23
    MOV EDX, EAX
    MUL EDX
    CMP EAX, -1
    JNZ label
    MOV DWORD PTR [0xDEADBEEF], ECX

label:
    MOV ECX, 0x4
    MOV EAX, ECX
    POP EBP
    RET
''', loc_db)

```

--------------------------------

### Miasm Disassembly and IR Generation

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore.ipynb

Processes assembled code by resolving patches, creating a container, disassembling it into an ACFG, and then translating it into Miasm's intermediate representation (IR). This involves `asm_resolve_final`, `Container`, `Machine`, `dis_multiblock`, and `ira`.

```python
loc_db.set_location_offset(loc_db.get_name_location('main'), 0x0)

patches = asmblock.asm_resolve_final(mn_x86, asmcfg)
patch_worker = StrPatchwork()
for offset, raw in patches.items():
    patch_worker[offset] = raw
    print('%08x'%(offset), mn_x86.dis(raw, 32))

cont = Container.from_string(array_tobytes(patch_worker.s), loc_db)

machine = Machine('x86_32')
mdis = machine.dis_engine(cont.bin_stream, loc_db=loc_db)

asmcfg2 = mdis.dis_multiblock(0)

ir_arch = machine.ira(loc_db)
ircfg = ir_arch.new_ircfg_from_asmcfg(asmcfg2)

for lbl, irb in viewitems(ircfg.blocks):
    print(irb)

```

--------------------------------

### Explore Code Paths with Symbolic Execution

Source: https://github.com/malrev/abd/blob/master/hands-on3/solved/simple_explore_smt.ipynb

This function recursively explores code paths starting from a given address. It uses a SymbolicExecutionEngine to run blocks and handles conditional branches by checking path feasibility with Z3. Limits are in place for depth and unconditional execution steps.

```python
def explore(ir, start_addr, start_symbols, 
        ircfg, cond_limit=30, uncond_limit=100, 
        lbl_stop=None, final_states=[]):

    def codepath_walk(addr, symbols, conds, depth, final_states, path):

        if depth >= cond_limit:
            warnings.warn("'depth' is over the cond_limit :%d"%(depth))
            return 

        sb = SymbolicExecutionEngine(ir, symbols)

        for _ in range(uncond_limit):

            if isinstance(addr, ExprInt):
                if addr == lbl_stop:
                    final_states.append(FinalState(True, sb, conds, path))
                    return

            path.append(addr)

            pc = sb.run_block_at(ircfg, addr)

            if isinstance(pc, ExprCond):
    
                # Calc the condition to take true or false paths
                cond_true  = {pc.cond: ExprInt(1, 32)}
                cond_false = {pc.cond: ExprInt(0, 32)}

                # The destination addr of the true or false paths
                addr_true  = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_true), {}))

                addr_false = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_false), {}))

                # Need to add the path conditions to reach this point
                conds_true = list(conds) + list(cond_true.items())
                conds_false = list(conds) + list(cond_false.items())

                # TODO:
                # Please add some code to complete the SMT-based path explore
                # Hint1: use check_path_feasibility()
                # Hint2: Do not forget to add the current state to the final_states 
                # when the path condition is infeasible. 
                # e.g., final_states.append(FinalState(False, sb, conds_true/conds_false, path))
                #
                # From here --------------------------------
                
                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))

                # To here --------------------------------

                return
            else:
                addr = expr_simp(sb.eval_expr(pc))

        final_states.append(FinalState(True, sb, conds, path))
        return 

    return codepath_walk(start_addr, start_symbols, [], 0, final_states, [])

```

--------------------------------

### Set up analysis environment and analyze VM handlers (Python)

Source: https://context7.com/malrev/abd/llms.txt

This snippet demonstrates setting up the analysis environment using Miasm, including initializing the machine, location database, and container from a binary file. It then prepares initial symbols for VM analysis, defines VM-specific expressions, and iterates through VM handlers to perform disassembly, IR conversion, and state exploration. Finally, it simplifies and displays state changes for each handler.

```python
# Set up analysis environment
machine = Machine('x86_32')
loc_db = LocationDB()
with open(filename, 'rb') as f:
    cont = Container.from_stream(f, loc_db)
bs = cont.bin_stream
mdis = machine.dis_engine(bs, loc_db=cont.loc_db)
ir_arch = machine.ir(mdis.loc_db)

# Prepare initial symbols for VM analysis
symbols_init = dict(regs.regs_init)
initial_symbols = symbols_init.items()

# Define VM-specific expressions
vm_pc_init = ExprId('VM_PC_init', 32)
ret_addr = ExprId('RET_ADDR', 32)

infos = {}
infos[expr_simp(ExprMem(regs.ECX_init, 32))] = vm_pc_init
infos[expr_simp(ExprMem(regs.ESP_init - ExprInt(4, 32), 32))] = ret_addr
infos[regs.ESP] = expr_simp(regs.ESP_init - ExprInt(4, 32))

# Virtual registers (REG0-REG4)
for i in range(5):
    infos[expr_simp(ExprMem(regs.ECX_init + ExprInt(4*(i+1), 32), 32))] = \
        ExprId('REG%d' % i, 32)

# Immediate operands
addition_infos = dict(infos)
addition_infos[expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 8))] = ExprId('imm8', 8)
addition_infos[expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 32))] = ExprId('imm32', 32)

# Analyze each VM handler
mnemonic_array_addr = 0x427018

for i in range(69):
    addr = int(hex(upck32(bs.getbytes(mnemonic_array_addr + 4*i, 4))), 16)
    print(f"Handler {i} at {hex(addr)}")

    asmcfg = mdis.dis_multiblock(addr)
    ircfg = ir_arch.new_ircfg_from_asmcfg(asmcfg)

    final_states = []
    explore(ir_arch, addr, symbols_init, ircfg, final_states=final_states)

    for state in final_states:
        if state.result:
            # Simplify and display state changes
            for expr, value in sorted(state.sb.symbols.items()):
                expr_s = expr_simp(expr.replace_expr(addition_infos))
                value_s = expr_simp(value.replace_expr(addition_infos))
                if expr_s != value_s:
                    print(f"  {expr_s} = {value_s}")

```

--------------------------------

### Initialize sandbox and DSE for argv[1] symbolization (Python)

Source: https://context7.com/malrev/abd/llms.txt

This Python snippet sets up a Miasm sandbox for Linux x86_64 to perform Dynamic Symbolic Execution (DSE). It initializes the sandbox with a specific binary, configures DSE with a code coverage strategy, and sets up a return address sentinel. It also defines memory regions for arguments and symbolizes argv[1] by adding ASCII constraints and linking symbolic to concrete memory.

```python
# -*- coding: utf-8 -*-
from miasm.analysis.sandbox import Sandbox_Linux_x86_64
from miasm.analysis.dse import DSEPathConstraint
from miasm.analysis.machine import Machine
from miasm.expression.expression import ExprMem, ExprId, ExprInt, ExprAssign
from miasm.core.locationdb import LocationDB
from miasm.jitter.csts import PAGE_READ, PAGE_WRITE
from future.utils import viewitems

# Parse sandbox options
parser = Sandbox_Linux_x86_64.parser(description='DSE deobfuscator')
options = parser.parse_args(args=[])
options.filename = 'flattening_volatile.bin'
options.strategy = 'code-cov'
options.mimic_env = True

# Initialize sandbox
loc_db = LocationDB()
sb = Sandbox_Linux_x86_64(loc_db, options.filename, options, globals())
machine = Machine('x86_64')

# Set up return address sentinel
ret_addr = 0x1337beef
sb.jitter.add_breakpoint(ret_addr, lambda j: setattr(j, 'run', False) or False)
sb.jitter.push_uint64_t(ret_addr)
sb.jitter.init_run(0x1040)

# Set up argument memory
MEM_ARGV_ADDR = 0x7ff70000
MEM_ARGV1_ADDR = 0x7ff80000

sb.jitter.vm.add_memory_page(MEM_ARGV_ADDR, PAGE_READ | PAGE_WRITE,
    b'\x42' * 8 + b'\x00\x00\xf8\x7f\x00\x00\x00\x00', 'argv')
sb.jitter.vm.add_memory_page(MEM_ARGV1_ADDR, PAGE_READ | PAGE_WRITE,
    b'\x00' * 8, 'argv1')

sb.jitter.cpu.RDI = 2  # argc
sb.jitter.cpu.RSI = MEM_ARGV_ADDR  # argv

# Initialize DSE with code coverage strategy
strategy = DSEPathConstraint.PRODUCE_SOLUTION_CODE_COV
dse = DSEPathConstraint(machine, loc_db, produce_solution=strategy)
dse.attach(sb.jitter)
dse.update_state_from_concrete()

# Symbolize argv[1]
regs = sb.jitter.ir_arch.arch.regs
argv1 = [ExprId(f'Argv[1][{i}]', 8) for i in range(8)]
argv1_addr = [ExprMem(ExprInt(MEM_ARGV1_ADDR + i, 64), 8) for i in range(8)]

# Add ASCII constraints
for arg in argv1:
    const = dse.z3_trans.from_expr(arg)
    dse.cur_solver.add(31 < const)
    dse.cur_solver.add(const < 127)

# Link symbolic to concrete memory
dse.update_state({addr: val for addr, val in zip(argv1_addr, argv1)})

```

--------------------------------

### Perform Symbolic Execution Exploration

Source: https://github.com/malrev/abd/blob/master/hands-on3/solved/simple_explore_smt.ipynb

Initiates symbolic execution on the intermediate representation graph. It explores possible execution paths starting from a given entry point, with specified initial states and a stop condition.

```python
explore(ir_arch, 
        0, 
        symbols_init, 
        ircfg, 
        lbl_stop=0xdeadbeef, 
        final_states=final_states)
```

--------------------------------

### Solve Constraint Satisfaction Problems with Z3

Source: https://context7.com/malrev/abd/llms.txt

Demonstrates the use of the Z3 SMT solver to define boolean and integer variables, add logical constraints, and retrieve satisfying models.

```python
from z3 import *

malicious, benign = Bools('malicious, benign')
s = Solver()
s.add(Or(malicious, benign), Or(Not(malicious), benign), Or(Not(malicious), Not(benign)))
print(s.check())

# Combined boolean and integer constraints
x = Int('x')
s.add(And(x*x-x == 2))
print(s.check())
print(s.model())
```

--------------------------------

### Initialize Miasm Analysis Environment in Python

Source: https://context7.com/malrev/abd/llms.txt

Sets up the necessary Miasm components for analyzing a binary file, specifically for x86 architecture. It loads a container, creates a machine object, disassembles code, and builds an intermediate representation (IR) graph. This is a prerequisite for performing detailed code analysis.

```python
# -*- coding: utf-8 -*-
from miasm.analysis.machine import Machine
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.ir.ir import IRCFG
from miasm.arch.x86.regs import *
from miasm.core.locationdb import LocationDB
from miasm.analysis.binary import Container
from miasm.ir.translators.translator import Translator
from future.utils import viewitems
import z3

# Example usage
filename = 'vipasana.bin'
target_addr = 0x434DF0

loc_db = LocationDB()
with open(filename, 'rb') as f:
    cont = Container.from_stream(f, loc_db)

machine = Machine('x86_32')
mdis = machine.dis_engine(cont.bin_stream, loc_db=cont.loc_db)
ir_arch = machine.ira(mdis.loc_db)
asmcfg = mdis.dis_multiblock(target_addr)

# Compare all pairs of basic blocks
for src_blk in asmcfg.blocks:
    for dst_blk in asmcfg.blocks:
        if src_blk._loc_key == dst_blk._loc_key:
            continue
        if semantic_compare(src_blk, dst_blk, ir_arch, ir_arch, asmcfg):
            print(f"Blocks {src_blk._loc_key} and {dst_blk._loc_key} are equivalent")

```

--------------------------------

### Assemble and Explore x86 Code

Source: https://context7.com/malrev/abd/llms.txt

Demonstrates the process of parsing assembly code, resolving patches, and performing symbolic execution to identify feasible paths in a binary.

```python
loc_db = LocationDB()
asmcfg = parse_asm.parse_txt(mn_x86, 32, '''
main:
    PUSH EBP
    MOV EBP, ESP
    MOV ECX, 0x23
    MOV EDX, EAX
    MUL EDX
    CMP EAX, -1
    JNZ label
    MOV DWORD PTR [0xDEADBEEF], ECX
label:
    MOV ECX, 0x4
    MOV EAX, ECX
    POP EBP
    RET
''', loc_db)

loc_db.set_location_offset(loc_db.get_name_location('main'), 0x0)
patches = asmblock.asm_resolve_final(mn_x86, asmcfg)
patch_worker = StrPatchwork()
for offset, raw in patches.items():
    patch_worker[offset] = raw

cont = Container.from_string(array_tobytes(patch_worker.s), loc_db)
machine = Machine('x86_32')
mdis = machine.dis_engine(cont.bin_stream, loc_db=loc_db)
asmcfg2 = mdis.dis_multiblock(0)
ir_arch = machine.ira(loc_db)
ircfg = ir_arch.new_ircfg_from_asmcfg(asmcfg2)

symbols_init = {ExprMem(ExprId('ESP_init', 32), 32): ExprInt(0xdeadbeef, 32)}
final_states = []
explore(ir_arch, 0, symbols_init, ircfg, lbl_stop=0xdeadbeef, final_states=final_states)
```

--------------------------------

### Initialize and Solve Boolean Constraints with Z3

Source: https://github.com/malrev/abd/blob/master/hands-on3/sat_smt.ipynb

This snippet initializes a Z3 solver instance and applies a set of Boolean constraints. It demonstrates how to check for satisfiability and retrieve the resulting model.

```python
from z3 import *
malicious, benign = Bools('malicious, benign')
s = Solver()
s.add(Or(malicious, benign), 
      Or(Not(malicious), benign), 
      Or(Not(malicious), Not(benign)))
print(s.sexpr())
print(s.check())
print(s.model())
```

--------------------------------

### Initialize Symbolic Constraints and Memory State

Source: https://github.com/malrev/abd/blob/master/hands-on6/cff_dse.ipynb

Sets up symbolic expressions for argv[1] and applies ASCII range constraints using the Z3 solver. It maps these symbolic values to memory addresses to prepare the DSE state.

```python
regs = sb.jitter.ir_arch.arch.regs
argv1 = [] 
for i in range(8):
    argv1.append(ExprId('Argv[1][%d]'%(i), 8))
    const = dse.z3_trans.from_expr(argv1[i])
    dse.cur_solver.add(31 < const) 
    dse.cur_solver.add(const < 127)

argv1_addr = []
for i in range(8):
    argv1_addr.append(ExprMem(ExprInt(MEM_ARGV1_ADDR + i, 64), 8))

s = {}
for addr, argv in zip(argv1_addr, argv1):
    s[addr] = argv
    
dse.update_state(s)
```

--------------------------------

### Check Path Feasibility with Z3

Source: https://context7.com/malrev/abd/llms.txt

Integrates the Z3 SMT solver with Miasm to verify the satisfiability of path conditions during symbolic execution, allowing for the pruning of infeasible code paths.

```python
from miasm.ir.translators.translator import Translator
import z3

def check_path_feasibility(conds):
    solver = z3.Solver()
    for lval, rval in conds:
        z3_cond = Translator.to_language("z3").from_expr(lval)
        solver.add(z3_cond == int(rval.arg))
    result = solver.check()
    return result == z3.sat

def explore_with_smt(ir, start_addr, start_symbols, ircfg, cond_limit=30, uncond_limit=100, lbl_stop=None, final_states=[]):
    def codepath_walk(addr, symbols, conds, depth, final_states, path):
        if isinstance(pc, ExprCond):
            cond_true = {pc.cond: ExprInt(1, 32)}
            cond_false = {pc.cond: ExprInt(0, 32)}
            conds_true = list(conds) + list(cond_true.items())
            conds_false = list(conds) + list(cond_false.items())
            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))
```

--------------------------------

### Initialize Miasm Analysis Environment

Source: https://github.com/malrev/abd/blob/master/hands-on2/deadcode_unremoval.ipynb

Sets up the necessary Miasm components including the LocationDB, architecture definitions, and binary container for x86_32 assembly analysis.

```python
from miasm.analysis.machine import Machine
from miasm.arch.x86.arch import mn_x86
from miasm.core import parse_asm, asmblock
from miasm.core.locationdb import LocationDB
from miasm.analysis.binary import Container

loc_db = LocationDB()
asmcfg = parse_asm.parse_txt(mn_x86, 32, ''' 
main:
    PUSH EBP
    MOV EBP, ESP
    MOV ECX, 0x23
    MOV ECX, 0x4
    MOV EAX, ECX
    POP EBP
    RET
''', loc_db)
```

--------------------------------

### Assemble x86 Assembly Code using Miasm (Python)

Source: https://github.com/malrev/abd/blob/master/hands-on3/simple_explore_smt.ipynb

Parses and assembles a given x86 assembly code snippet into an intermediate representation (IR) using Miasm. It defines a location database and uses `parse_asm` to process the assembly text.

```python
# Assemble code
loc_db = LocationDB()
asmcfg = parse_asm.parse_txt(mn_x86, 32, ''' 
main:
    PUSH EBP
    MOV EBP, ESP
    MOV ECX, 0x23
    MOV EDX, EAX
    MUL EDX
    CMP EAX, -1
    JNZ label
    MOV DWORD PTR [0xDEADBEEF], ECX

label:
    MOV ECX, 0x4
    MOV EAX, ECX
    POP EBP
    RET
''', loc_db)
```

--------------------------------

### Generate Obfuscated Binaries with OLLVM

Source: https://context7.com/malrev/abd/llms.txt

Automates the generation of obfuscated binaries using Control Flow Flattening, Bogus Control Flow, and Instruction Substitution techniques via the Obfuscator-LLVM compiler.

```bash
#!/bin/bash
# o-llvm.sh - Apply various obfuscation techniques

CLANG=../obfuscator/build/bin/clang
FILENAMES=src/*.c

for FILE in ${FILENAMES}; do
  FILE_NO_EXT=${FILE%.*}

  # Control Flow Flattening
  ${CLANG} -m32 ${FILE} -o "${FILE_NO_EXT##*/}-fla.bin" -mllvm -fla

  # Bogus Control Flow
  ${CLANG} -m32 ${FILE} -o "${FILE_NO_EXT##*/}-bcf.bin" -mllvm -bcf -mllvm -bcf_prob=100

  # Instruction Substitution
  ${CLANG} -m32 ${FILE} -o "${FILE_NO_EXT##*/}-sub.bin" -mllvm -sub
done
```

--------------------------------

### Initialize Miasm Analysis Environment

Source: https://github.com/malrev/abd/blob/master/hands-on4/solved/eqcheck.ipynb

Initializes the Miasm analysis environment by loading a binary file into a container, setting up the machine architecture (x86_32), performing disassembly, and creating Intermediate Representation (IR) architectures for comparison.

```python
loc_db = LocationDB()
with open(filename, 'rb') as fstream:
    cont = Container.from_stream(fstream, loc_db)
    
machine = Machine('x86_32')
mdis = machine.dis_engine(cont.bin_stream, loc_db=cont.loc_db)
ir_arch0 = machine.ira(mdis.loc_db)
ir_arch1 = machine.ira(mdis.loc_db)

asmcfg = mdis.dis_multiblock(target_addr)
```

--------------------------------

### Initialize Miasm Sandbox and DSE Environment

Source: https://github.com/malrev/abd/blob/master/hands-on6/cff_dse.ipynb

Configures the Miasm Sandbox_Linux_x86_64 parser and initializes the DSE engine. It sets up the binary container, defines memory pages for process arguments, and attaches the DSE instance to the jitter.

```python
from miasm.analysis.sandbox import Sandbox_Linux_x86_64
from miasm.analysis.binary import Container
from miasm.core.locationdb import LocationDB
from miasm.analysis.dse import DSEPathConstraint
from miasm.analysis.machine import Machine
from miasm.jitter.csts import PAGE_READ, PAGE_WRITE

loc_db = LocationDB()
options.filename = 'flattening_volatile.bin'
sb = Sandbox_Linux_x86_64(loc_db, options.filename, options, globals())

# Memory setup
MEM_ARGV_ADDR = 0x7ff70000
sb.jitter.vm.add_memory_page(MEM_ARGV_ADDR, PAGE_READ | PAGE_WRITE, b'\x42' * 8 + b'\x00\x00\xf8\x7f\x00\x00\x00\x00', 'Binary')

# DSE initialization
machine = Machine('x86_64')
dse = DSEPathConstraint(machine, loc_db, produce_solution=DSEPathConstraint.PRODUCE_SOLUTION_CODE_COV)
dse.attach(sb.jitter)
dse.update_state_from_concrete()
```

--------------------------------

### Perform Path Exploration for Binary Deobfuscation

Source: https://context7.com/malrev/abd/llms.txt

This script implements a dynamic symbolic execution loop to explore program paths and find specific inputs that satisfy a target condition. It uses a snapshot-based approach to restore state, inject concrete values into memory, and iteratively discover new solutions using Z3 constraint solving.

```python
todo = set([(ExprInt(0x42, 8),) + (ExprInt(0x41, 8),) * 7])
done = set()
snapshot = dse.take_snapshot()

while todo:
    arg_value = todo.pop()
    if arg_value in done:
        continue
    done.add(arg_value)

    dse.restore_snapshot(snapshot, keep_known_solutions=True)

    for i in range(8):
        sb.jitter.eval_expr(ExprAssign(argv1_addr[i], arg_value[i]))

    sb.jitter.init_run(0x1040)
    sb.jitter.continue_run(step=False)

    if sb.jitter.cpu.RAX == 0:
        print('FOUND:', ''.join(chr(int(x)) for x in arg_value))
        break

    for sol_ident, model in viewitems(dse.new_solutions):
        sol_expr = []
        for i in range(8):
            try:
                val = model.eval(dse.z3_trans.from_expr(argv1[i])).as_long()
            except AttributeError:
                val = 0
            sol_expr.append(ExprInt(val, 8))
        todo.add(tuple(sol_expr))
```

--------------------------------

### Initialize Miasm Disassembly Environment

Source: https://github.com/malrev/abd/blob/master/hands-on5/solved/zeus_get_ir.ipynb

Sets up the Miasm machine, container, and disassembly engine for an x86_32 binary file.

```python
filename = 'zeusvm.bin'
machine = Machine('x86_32')
loc_db = LocationDB()
with open(filename, 'rb') as fstream:
    cont = Container.from_stream(fstream, loc_db)
bs = cont.bin_stream
mdis = machine.dis_engine(bs, loc_db=cont.loc_db)
ir_arch = machine.ir(mdis.loc_db)
```

--------------------------------

### Resolve Assembly Patches and Create Miasm Container

Source: https://github.com/malrev/abd/blob/master/hands-on2/solved/deadcode_unremoval.ipynb

Resolves assembly patches from an assembly configuration and creates a Miasm Container object. This involves using `asm_resolve_final` to get the raw bytes, a `StrPatchwork` worker to manage patches, and `Container.from_string` to build the binary representation. It's a crucial step before disassembly.

```python
loc_db.set_location_offset(loc_db.get_name_location('main'), 0x0)

patches = asmblock.asm_resolve_final(mn_x86, asmcfg)
patch_worker = StrPatchwork()
for offset, raw in patches.items():
    patch_worker[offset] = raw
    
cont = Container.from_string(array_tobytes(patch_worker.s), loc_db=loc_db)
```

--------------------------------

### Miasm Symbolic Execution Engine Initialization

Source: https://github.com/malrev/abd/blob/master/hands-on5/vm_explore.ipynb

Initializes the Miasm symbolic execution engine by preparing register and memory symbols. It sets up virtual machine semantics, including program counter and return address, and defines additional virtual registers and immediate values.

```python
# -*- coding: utf-8 -*-
from miasm.analysis.machine import Machine
from miasm.analysis.binary import Container
from miasm.expression.expression import *
from miasm.core.utils import *
from miasm.core.locationdb import LocationDB
from miasm.arch.x86 import regs
from miasm.ir.symbexec import SymbolicExecutionEngine, get_block
from miasm.expression.simplifications import expr_simp

class FinalState:
    def __init__(self, result, sym, path_conds, path_history):
        self.result = result
        self.sb = sym
        self.path_conds = path_conds
        self.path_history = path_history

def explore(ir, start_addr, start_symbols, 
        ircfg, cond_limit=30, uncond_limit=100, 
        lbl_stop=None, final_states=[]):

    def codepath_walk(addr, symbols, conds, depth, final_states, path):
    
        if depth >= cond_limit:
            warnings.warn("'depth' is over the cond_limit :%d"%(depth))
            return 

        sb = SymbolicExecutionEngine(ir, symbols)

        for _ in range(uncond_limit):

            if isinstance(addr, ExprInt):
                if addr == ret_addr:
                    final_states.append(FinalState(True, sb, conds, path))
                    return

            path.append(addr)

            pc = sb.run_block_at(ircfg, addr)

            if isinstance(pc, ExprCond):
    
                # Calc the condition to take true or false paths
                cond_true  = {pc.cond: ExprInt(1, 32)}
                cond_false = {pc.cond: ExprInt(0, 32)}

                # The destination addr of the true or false paths
                addr_true  = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_true), {}))

                addr_false = expr_simp(
                    sb.eval_expr(pc.replace_expr(cond_false), {}))

                # Need to add the path conditions to reach this point
                conds_true = list(conds) + list(cond_true.items())
                conds_false = list(conds) + list(cond_false.items())

                # Recursive call for the true or false path
                codepath_walk(
                        addr_true, sb.symbols.copy(), 
                        conds_true, depth + 1, final_states, list(path))

                codepath_walk(
                        addr_false, sb.symbols.copy(), 
                        conds_false, depth + 1, final_states, list(path))

                return
            else:
                addr = expr_simp(sb.eval_expr(pc))

        final_states.append(FinalState(True, sb, conds, path))
        return 

    return codepath_walk(start_addr, start_symbols, [], 0, final_states, [])

# Preparing the initial symbols for regs and mems
symbols_init = dict(regs.regs_init)
initial_symbols = symbols_init.items()

# Prepare VM Semantics
# VM_PC_init and RET_ADDR
vm_pc_init = ExprId('VM_PC_init', 32)
ret_addr = ExprId('RET_ADDR', 32)

infos = {}
infos[expr_simp(ExprMem(regs.ECX_init, 32))] = vm_pc_init
infos[expr_simp(ExprMem(regs.ESP_init-ExprInt(4, 32), 32))] = ret_addr
infos[regs.ESP] = expr_simp(regs.ESP_init-ExprInt(4, 32))

# Virtual registers
for i in range(0, 5):
    infos[expr_simp(ExprMem(regs.ECX_init + ExprInt(4*(i+1), 32), 32))] = ExprId('REG%d' % i, 32)

# Additional info
addition_infos = dict(infos)

# imm
expr_imm8 = expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 8))
addition_infos[expr_imm8] = ExprId('imm8' , 8)

expr_imm16 = expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 16))
addition_infos[expr_imm16] = ExprId('imm16' , 16)

expr_imm32 = expr_simp(ExprMem(vm_pc_init + ExprInt(0x1, 32), 32))
addition_infos[expr_imm32] = ExprId('imm32' , 32)

```