🌟 Strilight

x86_64 바이너리 분석을 위한 고성능 $O(1)$ SMT 루프 리프팅 및 Strided Interval 도메인

📖 1. 개요 및 핵심 문제

전통적인 Symbolic Execution 및 DBI(Dynamic Binary Instrumentation) 엔진(angr, Triton, KLEE 등)은 악명 높은 **경로 및 루프 폭발 문제(Path & Loop Explosion Problem)**를 겪습니다. 루프를 만[...]

Strilight는 루프를 Strided Interval 도메인 내의 **폐쇄형 대수 점화식(closed-form algebraic recurrences)**으로 취급하여 이 문제를 근본적으로 해결합니다:

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

$N$번의 반복을 시뮬레이션하는 대신, Strilight는 반복 실행 트레이스를 계층적 LoopBlock 구조로 압축하고, 추상 아핀(affine) 및 다환(polycyclic) 단계를 평가한 다음, 루프를 [...]

⚡ 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. Zero-Unroll 트레이스 압축: 백엣지(back-edge)를 식별하고 수백만 개의 선형 명령어 트레이스를 $<1\text{ ms}$ 만에 간결한 계층적 LoopBlock 그래프로 압축합니다.
2. Strided Interval 도메인 및 이중 마스크 VSA: 스트라이드와 모듈러 합동(congruence)을 사용하여 레지스터 및 메모리 변환을 추적합니다: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. 다환 및 주기 패턴 추출: 복잡한 순환 메모리 및 서브레지스터 변환($P > 1$)을 탐지합니다.
4. Iron Invariant Contract: SMT 솔버가 루프 종료 경계를 "순간이동(teleport)"하는 것을 방지하기 위해 정확한 최초 탈출 경계 조건을 정식화합니다: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. 분리형 모듈러 아키텍처: 네이티브 Capstone 디스어셈블리와 플러그 가능한 커스텀 트레이서 브리지.

🚀 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% 테스트 통과율로 모든 모듈을 검증합니다:

Tier 1: 코어 컴프레서 및 추상 해석 테스트 (strilight 필요)

무거운 솔버 의존성 없음. 모든 플랫폼에서 $<1\text{ 초}$ 소요:

Tier 2: 동적 슬라이싱 및 의존성 트래커 테스트 (strilight[tracker] 필요)

전체 동적 데이터 흐름 및 제어 의존성 추적을 검증합니다:

Tier 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 해결

목표 조건을 충족하는 데 필요한 반복 횟수($N$) 또는 입력 키를 $<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. 실제 바이너리 벤치마크 결과

중첩 루프, 서브레지스터 슬라이싱 및 난독화된 스트라이드 패턴을 포함하는 복잡한 64비트 Windows 실행 파일(CrackMe Suite)로 테스트했습니다:

Ground-Truth 검증: 복구된 모든 키는 서브프로세스를 통해 네이티브 컴파일 바이너리(.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 / 독점(Proprietary). 고성능 리버스 엔지니어링 및 바이너리 분석을 위해 ❤️로 개발되었습니다.