Symbolic Execution Tools

Symbolic Execution Tools

Upstream reference: yaklang/hack-skills/symbolic-execution-tools. Final user-facing summary in Vietnamese.

0. Authorization & routing

Operates under MASTER_POLICY.md §1-§2.

1. Tool selection

2. angr — minimum viable script (crackme template)

# pip install angr claripy
import angr, claripy

proj = angr.Project('./crackme', auto_load_libs=False)

# Symbolic input — 32 printable bytes
flag_len = 32
flag = claripy.BVS('flag', 8 * flag_len)

state = proj.factory.entry_state(
    args=['./crackme'],
    stdin=flag,
)
# Constrain to printable ASCII
for i in range(flag_len):
    b = flag.get_byte(i)
    state.solver.add(b >= 0x20, b <= 0x7e)

simgr = proj.factory.simgr(state)
simgr.explore(
    find=lambda s: b'Correct' in s.posix.dumps(1),     # stdout sentinel
    avoid=lambda s: b'Wrong'  in s.posix.dumps(1),
)
if simgr.found:
    sol = simgr.found[0].solver.eval(flag, cast_to=bytes)
    print('flag =', sol)
else:
    print('no solution')

3. State factories — when to use which

4. Hooking & SimProcedures

# Replace strcmp with a fast SimProcedure
import angr
proj.hook_symbol('strcmp', angr.SIM_PROCEDURES['libc']['strcmp']())

# Custom hook — return value forced to 0
@proj.hook(0x401234, length=5)        # length must equal patched insn bytes
def force_ok(state):
    state.regs.eax = 0

Use this to:

• skip anti-debug calls (ptrace, IsDebuggerPresent)
• model scanf, printf, malloc cleanly
• short-circuit slow / opaque loops

5. Path-explosion taming

6. Z3 — direct constraint examples

# pip install z3-solver
from z3 import *

# Toy: find 8-byte input where xor(in, key) == out
key = bytes.fromhex('aabbccdd' * 2)
out = bytes.fromhex('11223344' * 2)

s = Solver()
inp = [BitVec(f'b{i}', 8) for i in range(8)]
for i in range(8):
    s.add(inp[i] ^ key[i] == out[i])
print(s.check(), [s.model()[b].as_long() for b in inp] if s.check() == sat else '-')

Use Z3 when the binary is already reduced to a system of equations (after VM lifting, or after a manual transcription of a small validator).

7. Unicorn for fast handler emulation

# pip install unicorn capstone
from unicorn import Uc, UC_ARCH_X86, UC_MODE_64
mu = Uc(UC_ARCH_X86, UC_MODE_64)

CODE_BASE = 0x400000
mu.mem_map(CODE_BASE, 0x10000)
mu.mem_write(CODE_BASE, open('handler.bin','rb').read())

mu.reg_write(UC_X86_REG_RDI, 0x41424344)    # arg1
mu.emu_start(CODE_BASE, CODE_BASE + 0x80)
print(hex(mu.reg_read(UC_X86_REG_RAX)))

Pair with vm-and-bytecode-reverse: each handler is a small native blob → emulate with Unicorn, drive PC manually.

8. Qiling — when you need syscall/OS awareness

# pip install qiling
from qiling import Qiling
ql = Qiling(['./linux_x86_64_target'], rootfs='./rootfs/x8664_linux')
ql.os.set_api('ptrace', lambda *a, **k: 0)   # hide debugger
ql.run()

Good for malware/firmware where OS calls matter and you don't want to keep porting symbolic stubs.

9. Methodology

1. Identify the target check function (string ref to "Wrong"/"Correct"; license error message; etc.).
2. Decide where to start: entry_state is safest; call_state(check_func, …) when you trust the rest.
3. Symbolize only what needs to be: keep concretes for everything else.
4. Stub expensive externals; cap loops; pin to relevant addresses.
5. explore(find=, avoid=); verify the recovered input on the real binary.
6. Hand off the discovered branch / value to binary-patcher for permanent patch, or to writerpro-pentest for keygen synthesis.

10. Anti-patterns

11. Final report (Vietnamese)

🧮 Symbolic execution hoàn tất:
  🛠️ Công cụ      : <angr | Z3 | Unicorn | Qiling | combo>
  🎯 Hàm mục tiêu : <addr / symbol>
  🔣 Input solved : <bytes hoặc số>
  ⏱️ Thời gian    : <s>
  📂 Script       : solve.py

▶  Tiếp:
   binary-patcher (vá vĩnh viễn) hoặc writerpro-pentest (sinh keygen từ ràng buộc).