🌟 Strilight

面向 x86_64 二进制分析的高性能 $O(1)$ SMT 循环提升与步长区间域

📖 1. 概述与核心问题

传统的符号执行与动态二进制插桩（DBI）引擎（如 angr、Triton 或 KLEE）都受困于臭名昭著的路径与循环爆炸问题。当遇到 l[...]

Strilight 从根本上解决了这一问题：它将循环视为步长区间域内的闭式代数递推关系：

$$\vec{\mathbf{R}}(N) = \vec{\mathbf{R}}_0 + \vec{\boldsymbol{\Delta}} \cdot N$$

Strilight 不模拟 $N$ 次迭代，而是将重复的执行轨迹压缩为层次化的 LoopBlock 结构，评估其抽象仿射与多循环步骤，并提升 e[...]

⚡ 2. 关键架构创新

graph LR
    A[Raw Machine Code / Trace] --> B[sl.disassemble & sl.compress]
    B --> C[sl.evaluate / LoopEvaluator]
    C -->|Strided Interval Domain| D[LoopSummary + Invariant Contract]
    D -->|O1 Closed-Form Lifting| E["Z3 SMT-LIB2 Solver"]
    E --> F[Instant Solution in less than 100 ms]

零展开轨迹压缩： 识别回边，并在 $<1\text{ ms}$ 内将数百万条线性指令轨迹压缩为紧凑的层次化 LoopBlock 图。
步长区间域与双掩码 VSA： 使用步长与模同余关系跟踪寄存器与内存变换： $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
多循环与周期性模式提取： 检测复杂的内存与子寄存器循环变换（$P > 1$）。
铁定不变量契约： 构建精确的首次退出边界条件，防止 SMT 求解器“瞬移”穿越循环终止边界： $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
解耦的模块化架构： 原生 Capstone 反汇编，支持可插拔的自定义 tracer 桥接。

🚀 3. 模块化分发方案

Strilight 以独立的模块化方案打包，让你只需携带流水线所需的组件：

# Profile 1: Core Engine (Pure Compressor + Embedded Def-Use Slicer + Capstone)
pip install strilight

# Profile 2: Symbolic Engine (Core Compressor + Z3 O(1) SMT Lifter)
pip install strilight[solver]

# Profile 3: Dynamic Slicing Suite (Core Compressor + Full PathTree Backward/Forward Tracker)
pip install strilight[tracker]

# Profile 4: Complete Bundle (All Engines + Full Tracker + Z3 Solver)
pip install strilight[all]

🧪 4. 测试套件分类与验证

测试套件在解耦的各个层级中以 100% 的测试通过率验证每个模块：

第 1 层：核心压缩器与抽象解释测试（需要 `strilight`）

零重型求解器依赖。可在任何平台上于 $<1\text{ second}$ 内运行：

第 2 层：动态切片与依赖跟踪器测试（需要 `strilight[tracker]`）

验证完整的动态数据流与控制依赖跟踪：

第 3 层：符号 SMT 提升器与求解器测试（需要 `strilight[solver]`）

验证 BitVector 方程生成、影子替换与 Z3 约束求解：

💡 5. 快速上手：使用 Strilight 的 3 种方式

方案 A：一行式循环分析（`sl.analyze`）

用一行代码分析任意原始 x86-64 机器码循环，并提取其闭式变换：

import strilight as sl

# Loop bytecode: add eax, 8; sub ebx, 3; inc ecx; cmp ecx, 100000; jl 0x1000
loop_bytes = bytes.fromhex("83c008 83eb03 ffc1 81f9a0860100 7ced")

# ONE-LINE ANALYSIS:
summary = sl.analyze(loop_bytes, iterations=100000)

print(summary.deltas)
# Output: {'eax': 8, 'ebx': -3, 'ecx': 1}

# View the mathematical invariant contract:
print(summary.invariant_contract.to_dict())

方案 B：逐步反汇编、压缩与评估

import strilight as sl

# 1. Disassemble machine code bytes
instructions = sl.disassemble(loop_bytes, base_address=0x1000)

# 2. Package into a symbolic loop block
block = sl.LoopBlock(body=instructions, iterations=100000)

# 3. Extract closed-form mathematical steps (Deltas & Exit Predicates)
summary = sl.evaluate(block)
print(f"Exit Condition: {summary.exit_condition}")

方案 C：使用 Z3 进行即时 $O(1)$ SMT 求解

在 $<100\text{ ms}$ 内求解满足目标条件所需的迭代次数（$N$）或输入密钥：

import strilight as sl
import z3

# Disassemble and evaluate
summary = sl.analyze(loop_bytes, iterations=100000)

# Initialize Z3 translator
translator = sl.Z3Translator()
translator.solver.add(translator.get_register('eax') == 0)
translator.solver.add(translator.get_register('ebx') == 500000)
translator.solver.add(translator.get_register('ecx') == 0)

# Lift loop summary in O(1) into Z3
translator.translate_loop_summary(summary, max_iterations=100000)

# Goal: When does EAX reach 800,000?
translator.solver.add(translator.get_register('eax') == 800000)

# Solve in milliseconds!
if translator.solver.check() == z3.sat:
    model = translator.solver.model()
    solved_N = model.eval(summary.loop_counter_var).as_long()
    print(f"[+] Solved N = {solved_N:,} iterations in O(1) time!")

📊 6. 真实二进制基准测试结果

已针对包含嵌套循环、子寄存器切片与混淆步长模式的复杂 64 位 Windows 可执行文件（CrackMe Suite）进行测试：

真值验证： 所有恢复出的密钥均通过 subprocess 执行原生编译的二进制文件（.exe）并断言返回 ACCESS GRANTED 响应来验证。

📚 7. API 参考

高层门面函数：

sl.analyze(code_bytes, iterations=1000, ...)：一行式反汇编 + 评估。
sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64)：基于 Capstone 的原始字节反汇编器。
sl.compress(trace, min_iterations=3)：层次化轨迹压缩器。
sl.evaluate(block_or_trace, k_passes=100)：抽象状态与不变量评估器。

核心类：

sl.Instruction：统一的汇编指令表示。
sl.LoopBlock：带迭代边界的层次化循环节点。
sl.LoopSummary：包含增量、循环模式与常量集的闭式变换摘要。
sl.LoopInvariantContract：形式化的结构退出不变量描述符及 SMT 边界规则生成器。
sl.StridedInterval：具有步长对齐与模同余关系的数学区间表示。
sl.Z3Translator：将循环摘要转换为 Z3 BitVector 约束的符号 SMT 提升器。

📄 许可证

双许可证：MIT / 专有。

以 ❤️ 为高性能逆向工程与二进制分析而打造。

`test_facade.py`	高层开发者 API（`sl.analyze`、`sl.disassemble`、`sl.compress`、`sl.evaluate`）	`strilight` 门面
`test_capstone_decoupling.py`	原始机器码字节反汇编与自定义 tracer 桥接注册	`Instruction`、`[...]
`test_invariant_contract.py`	数学不变量契约与 $N-1$ 铁定约束边界描述符	`LoopInvari[...]
`test_interval.py`	核心区间界定、区间算术与运算	`Interval`
`test_disjoint_set.py`	不相交内存集合、非连续范围算术与并集运算	`DisjointIntervalSet`
`test_strided_interval_notion.py`	步长区间域、GCD 同余桥接与子寄存器位掩码	`Stri[...]
`test_circular_theorems.py`	循环模运算回绕定理（$x \pmod{2^w}$）	`StridedInterval` 数学运算
`test_loop_compressor.py`	轨迹折叠与循环回边检测，生成 `LoopBlock` 树	`TraceCompressor`
`test_nested_loops.py`	多级嵌套循环压缩（$O(N \cdot M)$ 层次化折叠）	`TraceCompressor` 树
`test_vsa_evaluator.py`	值集分析模拟遍与仿射增量提取	`LoopEvaluator`
`test_polycyclic.py`	内存与寄存器中的多循环周期性模式（$P > 1$）	`LoopEvaluator`

`test_tracker.py`	后向/前向指令切片、寄存器/内存定义-使用链	`Tracker`、`BackwardTracker`
`test_lazy_tracker.py`	惰性求值与无关循环块跳过	`Tracker` 优化
`test_loop_taint.py`	循环污点传播与循环退出控制依赖跟踪	`Tracker` 污点
`test_path_tree.py`	分支决策缓存与死路路径消除	`PathTree`
`test_stop_dict.py`	API 污点边界定义	`stop_dict`
`test_hooks.py`	指令与内存访问拦截回调	`hooks`

`test_translator.py`	将完整 x86-64 指令翻译为 Z3 BitVector（算术、标志位、跳转、内存）	`Z3Translator`
`test_translator_edge_cases.py`	深度 AST 穷举、内存别名链与边界约束	`Z3Translato[...]
`test_deep_doubts.py`	有符号回绕、三次牛顿归纳与 Bezout 同余	数学证明

1	`crackme_boss.exe`	662	SAT	`1729`	`ACCESS GRANTED`	~60 ms	[PASS]
2	`crackme_subregs.exe`	671	SAT	`1337`	`ACCESS GRANTED`	~75 ms	[PASS]
3	`crackme_nested_loops.exe`	1369	SAT	`1337`	`ACCESS GRANTED`	~110 ms	[PASS]
4	`crackme_pointers.exe`	859	SAT	`1337`	`ACCESS GRANTED`	~85 ms	[PASS]
5	`crackme_license.exe`	657	SAT	`1337`	`ACCESS GRANTED`	~65 ms	[PASS]
6	`crackme_strided_circular.exe`	829	SAT	`1337`	`ACCESS GRANTED`	~95 ms	[PASS]

strilight

最受欢迎