🌟 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$$

$N$ पुनरावृत्तियों का अनुकरण करने के बजाय, Strilight पुनरावृत्त निष्पादन ट्रेस को पदानुक्रमित LoopBlock संरचनाओं में संपीड़ित करता है, उनके अमूर्त affine और पॉलीसाइक्लिक चरणों का मूल्यांकन करता है, और 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. ज़ीरो-अनरोल ट्रेस संपीड़न: बैक-एज की पहचान करता है और लाखों रैखिक निर्देश ट्रेस को $<1\text{ ms}$ में कॉम्पैक्ट पदानुक्रमित LoopBlock ग्राफ़ में संपीड़ित करता है।
2. स्ट्राइडेड इंटरवल डोमेन और डुअल-मास्क VSA: स्ट्राइड और मॉड्यूलर कॉन्ग्रुएंस का उपयोग करके रजिस्टर और मेमोरी ट्रांसफ़ॉर्मेशन ट्रैक करता है: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. पॉलीसाइक्लिक और आवधिक पैटर्न निष्कर्षण: जटिल चक्रीय मेमोरी और सब-रजिस्टर ट्रांसफ़ॉर्मेशन ($P > 1$) का पता लगाता है।
4. आयरन इनवेरिएंट कॉन्ट्रैक्ट: SMT सॉल्वरों को लूप समाप्ति सीमाओं के माध्यम से "टेलीपोर्ट" करने से रोकने के लिए सटीक प्रथम-निकास सीमा स्थिति तैयार करता है: $$\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% परीक्षण पास दर के साथ मान्य करता है:

टियर 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 समाधान

लक्ष्य स्थिति को संतुष्ट करने के लिए आवश्यक पुनरावृत्तियों ($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-बिट विंडोज़ एक्ज़ीक्यूटेबल (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 / Proprietary। उच्च-प्रदर्शन रिवर्स इंजीनियरिंग और बाइनरी विश्लेषण के लिए ❤️ के साथ विकसित।