diff --git a/README.md b/README.md index 3441ea40..df98b8fa 100644 --- a/README.md +++ b/README.md @@ -180,7 +180,8 @@ We get the flags, then we get the 7th bit which is Sign Flag, then we use the Si Even though we solve the indirect jumps, jumps with more than 2 possible location are not supported. This is because the analysis for them are not implemented yet. This allows us to solve the vm-style branches, but have problem with real life jumptables. -### Example #3 (Themida 3.1.6.0 LION64 (Red)) +### Example #3 (Themida 3.1.6.0 LION64) + Our target program: ![image](images/themida_disas_b.png) @@ -202,27 +203,10 @@ Running Mergen: ![image](images/running_on_themida.png) Output code: [click here](docs/themida_output.ll) -So, why our result is not succesful as lifting a binary thats protected by vmp? - -Themida actively writes on .themida section. Unlike stack, we cant disregard these writes, because these values might be read by other stuff later. - -But, we have a temporary solution to that. Remove all stores into .themida section. Since our program doesnt write into memory, [I just commented all the stores.](docs/themida_output_lazy_fix.ll) Now we are left with this: - -```llvm -source_filename = "my_lifting_module" -define i64 @main(i64 %rax, i64 %rcx, i64 %rdx, i64 %rbx, i64 %rsp, i64 %rbp, i64 %rsi, i64 %rdi, i64 %r8, i64 %r9, i64 %r10, i64 %r11, i64 %r12, i64 %r13, i64 %r14, i64 %r15, ptr writeonly %memory) local_unnamed_addr #0 { - %trunc = trunc i64 %r8 to i32 - %trunc1 = trunc i64 %rdx to i32 - %trunc2 = trunc i64 %rcx to i32 - %realadd-5369771371- = add i32 %trunc1, %trunc2 - %realadd-5369582686- = add i32 %realadd-5369771371-, %trunc - %trunc457139 = zext i32 %realadd-5369582686- to i64 - ret i64 %trunc457139 -} +On the current tree this sample lifts successfully, and `python test.py themida` passes. The lifted IR surfaces the guest program's `GetStdHandle`, `WriteConsoleA`, `ReadConsoleA`, and `CharUpperA` imports again, so the older lazy-fix writeup is no longer an accurate description of mainline behavior. -attributes #0 = { mustprogress nofree norecurse nosync nounwind willreturn memory(argmem: write) } -``` +The remaining challenge is robustness rather than basic success. Themida-style dispatch still produces many spurious indirect-branch candidates during path solving, and the lifter prunes unmapped switch targets instead of trying to decode garbage. See `lifter/analysis/PathSolver.ipp` and `scripts/rewrite/themida_samples.json` for the current gate and rationale. # Technical challenges - Loops - Self Modifying Code ( especially with conditional modification) diff --git a/autoresearch.sh b/autoresearch.sh index 88fcd1a9..87c430f4 100644 --- a/autoresearch.sh +++ b/autoresearch.sh @@ -1,32 +1,15 @@ #!/usr/bin/env bash -# Cheap manifest-stats harness for the VM-sample population task. -# -# Primary metric: number of VM-shaped samples in instruction_microtests.json. -# A "VM-shaped" sample has "vm" (case-insensitive) in `name` and non-empty -# `patterns` and `semantic` lists. This rewards fully-wired samples, not stubs. set -euo pipefail cd "$(dirname "$0")" -# Generate metrics via PowerShell: natively on PATH, no stdout plumbing issues -# when run under bash on Windows. -powershell.exe -NoProfile -ExecutionPolicy Bypass -Command " - \$ErrorActionPreference = 'Stop'; - \$raw = Get-Content -Raw -LiteralPath 'scripts/rewrite/instruction_microtests.json'; - \$data = \$raw | ConvertFrom-Json; - \$samples = @(\$data.samples); - \$vm = 0; - \$totalSem = 0; - foreach (\$s in \$samples) { - \$name = ''; if (\$s.name) { \$name = [string]\$s.name }; - \$patterns = @(); if (\$s.patterns) { \$patterns = @(\$s.patterns) }; - \$semantic = @(); if (\$s.semantic) { \$semantic = @(\$s.semantic) }; - \$totalSem += \$semantic.Count; - if (\$name.ToLower().Contains('vm') -and \$patterns.Count -gt 0 -and \$semantic.Count -gt 0) { - \$vm += 1; - } - }; - Write-Output (\"METRIC vm_sample_count=\$vm\"); - Write-Output (\"METRIC total_semantic_cases=\$totalSem\"); - Write-Output (\"METRIC manifest_samples=\$(\$samples.Count)\"); -" +tmp_out="$(mktemp)" +trap 'rm -f "$tmp_out"' EXIT + +python.exe test.py themida | tee "$tmp_out" + +pass_count="$(grep -c '^PASS:' "$tmp_out" || true)" +missing_count="$(grep -c 'MISSING required import' "$tmp_out" || true)" + +printf 'METRIC themida_pass_count=%s\n' "$pass_count" +printf 'METRIC missing_required_imports=%s\n' "$missing_count" diff --git a/docs/LOOP_HANDLING.md b/docs/LOOP_HANDLING.md index 11b123e2..da55a55a 100644 --- a/docs/LOOP_HANDLING.md +++ b/docs/LOOP_HANDLING.md @@ -182,7 +182,7 @@ For changes that touch register/flag phi shape, also run the two Themida gates build_iced\lifter.exe ..\testthemida\example2-virt.bin 0x140001000 ``` -Inspect `output_diagnostics.json` for `lift_stats.instructions_lifted == 2544` and `summary.warning == 0`, `summary.error == 0`. This only certifies that the lifter walked the VM's 2544 handler instructions without reporting errors — it does **not** certify that the recovered IR is semantically equivalent to the original function. +Inspect `output_diagnostics.json` for `lift_stats.instructions_lifted > 0` and `summary.warning == 0`, `summary.error == 0`. On the current `example2-virt.bin` reference run this is a large lift (for example, 64879 instructions on the current tree), because the VM and related outlined flow are both traversed. This only certifies that the lifter walked the protected control flow without reporting errors — it does **not** certify that the recovered IR is semantically equivalent to the original function. **Correctness gate** — confirms the devirtualized IR calls the same external imports as the non-virtualized reference: @@ -192,7 +192,7 @@ python test.py themida Fails hard if any required import from `scripts/rewrite/themida_samples.json` is missing from the lifted IR. Required imports are pinned against a lift of the non-virt reference binary; regenerate with `python test.py themida --update` when the reference changes (not when the virt output changes). Passing this gate means the VM devirtualization recovered the guest program's external-call semantics, not just the VM's own state-machine activity. -This gate is currently **red** on `example2-virt.bin`: the lifter unrolls the VM but does not surface the guest's `GetStdHandle` / `WriteConsoleA` / `ReadConsoleA` / `CharUpperA` calls. That gap is the active Themida-frontier work item — the coverage gate passing while the correctness gate fails is exactly the failure mode the two-gate split is designed to make visible. +This gate is currently **green** on `example2-virt.bin`: the lifter surfaces the guest's `GetStdHandle` / `WriteConsoleA` / `ReadConsoleA` / `CharUpperA` calls again. The active frontier for Themida is keeping that recovery robust while path solving still has to discard many unmapped switch-target candidates along the way. ## Known limitations diff --git a/scripts/rewrite/themida_samples.json b/scripts/rewrite/themida_samples.json index e2d16d4b..879d9a52 100644 --- a/scripts/rewrite/themida_samples.json +++ b/scripts/rewrite/themida_samples.json @@ -3,8 +3,9 @@ "Themida preserves the guest binary's own imports (Win32 APIs) in the IAT,", "but rewrites each call site from `call [rip+IAT]` to a VM-staged", "`push target; ret` where `target` was loaded from the IAT by an upstream", - "VM handler. The lifter currently does not recognize this transfer pattern", - "as an import call, so the guest's externals do not surface in the IR.", + "VM handler. The current lifter recognizes enough of that transfer pattern", + "for `example2-virt.bin` to recover the guest imports in IR, and this gate", + "pins that behavior so regressions fail hard.", "See scripts/dev/trace_external_calls.py for a Unicorn-based tracer that", "shows the real call mechanism at runtime.", "",