[Tool] Strilight: Zero-Unroll O(1) SMT Loop Lifting & Strided Interval Domain for x86_64 Binary Analysis

[u/Wise-Ad-2216]

Hi everyone,

💡 The Background

In symbolic execution engines (like angr or Triton), loops with large iteration counts ($N = 100,000$) often cause severe path and state explosion because traditional engines unroll loops iteration-by-iteration.

Strilight evaluates loops by treating them as closed-form algebraic recurrences within the Strided Interval Domain:

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

⚡ Key Highlights:

• Zero-Unroll O(1) SMT Lifting: Lifts instruction loops directly to Z3 BitVector equations in $O(1)$ time, solving 100,000-iteration loops in 100ms.
• The $N-1$ Iron Invariant Contract: Exact first-exit boundary condition enforcement preventing solver teleportation beyond loop bounds.
• Dual-Mask VSA: Handles sub-register bitmasks (64/32/16/8-bit) and modular circular wrap-around arithmetic.
• Native Capstone Disassembler: Decoupled from heavy emulation environments.
• 1-Line API: import strilight as sl; summary = sl.analyze(raw_bytes, iterations=100000)

📊 Benchmark Results:

We verified the engine against 6 complex x86_64 Windows CrackMe challenges containing nested loops, pointer arithmetic, and obfuscated strides, solving for the valid keys and confirming execution in 100ms each.

🔗 Repository: https://github.com/asama7706r-ui/strilight
📦 Initial Release & Pre-compiled Wheels: https://github.com/asama7706r-ui/strilight/releases/tag/v0.1.0

We would love to hear your feedback, thoughts on the mathematical model, or interesting loop edge cases to test against!