🌟 Strilight

High-Performance $O(1)$ SMT Loop Lifting & Strided Interval Domain for x86_64 Binary Analysis

📖 1. Overview & The Core Problem

Traditional Symbolic Execution and Dynamic Binary Instrumentation (DBI) engines (such as angr, Triton, or KLEE) suffer from the notorious Path & Loop Explosion Problem. When encountering a l[...]

Strilight solves this fundamentally by treating loops as closed-form algebraic recurrences within the Strided Interval Domain:

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

Instead of simulating $N$ iterations, Strilight compresses repetitive execution traces into hierarchical LoopBlock structures, evaluates their abstract affine & polycyclic steps, and lifts the e[...]

⚡ 2. Key Architectural Innovations

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. Zero-Unroll Trace Compression: Identifies back-edges and compresses millions of linear instruction traces into compact hierarchical LoopBlock graphs in $<1\text{ ms}$.
2. Strided Interval Domain & Dual-Mask VSA: Tracks register and memory transformations using strides and modular congruences: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Polycyclic & Periodic Pattern Extraction: Detects complex cyclic memory and sub-register transformations ($P > 1$).
4. The Iron Invariant Contract: Formulates the exact first-exit boundary condition to prevent SMT solvers from "teleporting" through loop termination bounds: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Decoupled Modular Architecture: Native Capstone disassembly with pluggable custom tracer bridges.

🚀 3. Modular Distribution Profiles

Strilight is packaged as independent modular profiles so you only carry the components your pipeline needs:

# 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. Test Suite Taxonomy & Verification

The test suite validates every module with 100% test pass rate across the decoupled layers:

Tier 1: Core Compressor & Abstract Interpretation Tests (Requires strilight)

Zero heavy solver dependencies. Runs in $<1\text{ second}$ on any platform:

Tier 2: Dynamic Slicing & Dependency Tracker Tests (Requires strilight[tracker])

Validates full dynamic data-flow and control-dependency tracking:

Tier 3: Symbolic SMT Lifter & Solver Tests (Requires strilight[solver])

Validates BitVector equation generation, shadow substitutions, and Z3 constraint solving:

💡 5. Quickstart: 3 Ways to Use Strilight

Option A: One-Line Loop Analysis (sl.analyze)

Analyze any raw x86-64 machine code loop and extract its closed-form transformation in a single line:

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())

Option B: Disassemble, Compress & Evaluate Step-by-Step

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}")

Option C: Instant $O(1)$ SMT Solving with Z3

Solve for the number of iterations ($N$) or the input key required to satisfy a goal condition in $<100\text{ ms}$:

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. Real-World Binary Benchmark Results

Tested against complex 64-bit Windows executables (CrackMe Suite) containing nested loops, sub-register slicing, and obfuscated stride patterns:

Ground-Truth Verification: All recovered keys are verified by executing the native compiled binary (.exe) via subprocess and asserting the ACCESS GRANTED response.

📚 7. API Reference

High-Level Facade Functions:

• sl.analyze(code_bytes, iterations=1000, ...): One-liner disassembly + evaluation.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): Raw byte disassembler via Capstone.
• sl.compress(trace, min_iterations=3): Hierarchical trace compressor.
• sl.evaluate(block_or_trace, k_passes=100): Abstract state & invariant evaluator.

Core Classes:

• sl.Instruction: Unified assembly instruction representation.
• sl.LoopBlock: Hierarchical loop node with iteration bounds.
• sl.LoopSummary: Closed-form transformation summary containing deltas, cyclic patterns, and constant sets.
• sl.LoopInvariantContract: Formal structural exit invariant descriptor and SMT boundary rule generator.
• sl.StridedInterval: Mathematical interval representation with stride alignment and modular congruence.
• sl.Z3Translator: Symbolic SMT lifter converting loop summaries to Z3 BitVector constraints.

📄 License

Dual License: MIT / Proprietary. Developed with ❤️ for high-performance reverse engineering and binary analysis.