Skip to content
KitploitKITPLOIT
도구익스플로잇블로그
Log in
제출
도구익스플로잇블로그
제출

해킹, 침투 테스트 및 사이버 보안 도구를 당신의 보안 무기고에!

Kitploit은 해킹, 사이버 보안 및 침투 테스트 도구 디렉토리입니다. 최신 프로젝트 업데이트를 발견하여 취약점을 찾고, 시스템을 분석하고, 테스트를 자동화하고, 보안을 강화하세요.

피드문의개인정보© 2026 Kitploit

도구 디렉토리

카테고리

모든 카테고리 보기
Loading categories
strilight — 스트라이드 구간 분석을 통해 x86-64 바이너리 루프를 폐쇄형 SMT 제약 조건으로 변환하여 O(1) 기호 실행과 crackme 키 복구를 가능하게 합니다. | Kitploit
도구/GitHubGitHub/asama7706r-ui/strilight
Static AnalysisCode AnalysisReverse EngineeringBinary Analysis
GitHubasama7706r-ui/strilight

strilight

스트라이드 구간 분석을 통해 x86-64 바이너리 루프를 폐쇄형 SMT 제약 조건으로 변환하여 O(1) 기호 실행과 crackme 키 복구를 가능하게 합니다.

저장소 보기
231개월 전아직 검토되지 않음

인기

모두 보기 →

커뮤니티에서 가장 많이 사용되는 도구를 찾아보세요.

모든 도구 탐색

도구 컬렉션을 둘러보세요

모든 도구 보기 →
웹사이트
공유

Strilight (v0.2.0)

Python 및 C를 위한 고성능 대수적 루프 리프팅 및 정확한 유리수 재귀 엔진

Release Python Version Complexity Exact Arithmetic Tests License


개요: 반복할 수 있는데 왜 풀지 않는가?

전통적인 컴파일러, 런타임, JIT 엔진(예: GCC, Clang, PyPy, Numba)은 루프를 반복적인 제어 흐름 시퀀스로 취급하여 명령을 단계별로 실행합니다:

$$ \text{Runtime Cost} = \mathcal{O}(N) $$

$N = 10^6$ 또는 $10^9$일 때, 순차 실행은 수십억 개의 CPU 사이클을 소모합니다. Strilight는 **기호 대수적 리프팅(Symbolic Algebraic Lifting)**을 통해 루프 실행을 근본적으로 재설계합니다:

  1. 상태 전이 공식화: 루프 본문을 정적으로 검사하고 수학적 상태 전이 행렬을 공식화합니다:

$$ \vec{\mathbf{X}}(N) = \mathbf{A}^N \cdot \vec{\mathbf{X}}0 + \sum{k=0}^{N-1} \mathbf{A}^{N-1-k} \vec{\mathbf{B}} $$

  1. 닫힌 형식 해: 재귀 시스템을 닫힌 형식으로 풀어 실행 시간을 **$\mathcal{O}(N)$**에서 $\mathcal{O}(1)$(스칼라/주기/망원급수인 경우) 또는 $\mathcal{O}(\log N)$(고속 이진 행렬 거듭제곱 사용)으로 단축합니다.

설계 철학: 개발자 삶의 질 우선

Strilight는 난해한 마법을 도입하는 척하지 않습니다. 그것은 근본적으로 개발자 삶의 질 도구입니다.

물리 모델링, 과학 컴퓨팅, 수치 시뮬레이션에서 엔지니어들은 종종 좌절스러운 딜레마에 직면합니다:

  • 가독성 좋은 코드: 교과서 물리학을 그대로 반영하는 자연스럽고 표현력 있는 방정식이지만, 수백만 번 반복하면 느리게 실행됩니다.
  • 수동 최적화 코드: 복잡하고 수동으로 풀어낸 루프와 불분명한 산술 단축 기법으로 빠르게 실행되지만, 취약하고 디버깅이 어려우며 근본 물리학을 모호하게 만듭니다.

Strilight는 이 딜레마를 해결합니다. 물리적 또는 수학적 개념을 원하는 대로 직관적이고 자연스러운 구문으로 작성하세요. Strilight는 루프 구조를 검사하고 정확한 닫힌 형식 재귀 공식을 도출하며, 백그라운드에서 실행을 가속화합니다—코드베이스의 완전한 가독성과 단순성을 유지하면서 말입니다.


아키텍처 기반

1. $\mathbb{Q}$ 위의 정확한 유리수 산술 (정밀도 손실 제로)

부동 소수점 산술은 누적 절단 오류를 도입합니다($1/3 \times 3 \approx 0.9999999999999999$). Strilight는 유리수체 $\mathbb{Q}$ 위에서 아핀 귀납법과 스트라이드 분석을 수행합니다:

  • 승수와 오프셋은 정규 분수($\frac{p}{q}$)로 모델링됩니다.
  • C에서는 배정밀도 커널을, Python에서는 정확한 Fraction 표현을 생성하여 100% 비트 단위로 정확한 수학적 동등성을 보장합니다.

2. 다변수 결합 재귀 시스템 ($\mathcal{O}(\log N)$)

서로 상호 의존하는 변수(예: 위치가 속도에 의존하고 속도가 가속도에 의존하는 물리 시뮬레이션)는 자동으로 변수 결합 행렬($\mathbf{A}$)로 추출됩니다. Strilight는 $\mathbf{A}$에 대해 이진 거듭제곱을 수행하여 수백만 번의 반복을 2나노초 이내에 실행합니다.

3. 투명한 @accelerate 데코레이터 (작동 방식)

표준 Python 함수에 @accelerate를 데코레이팅하면 함수 정의 시점에 자동화된 파이프라인이 실행됩니다(호출당 런타임 분석 오버헤드 제로):

  1. AST 추출: 함수 AST를 검사하고 for 루프 구문을 식별하며 유도 변수를 추출합니다.
  2. 닫힌 형식 합성: 루프를 동등한 닫힌 형식 점화 모델 또는 이진 행렬 거듭제곱 커널로 변환합니다.
  3. 제자리 스플라이싱: 루프 AST 노드를 제자리에서 교체하고, 호출 가능 객체를 메모리로 컴파일하며, 모듈 네임스페이스를 오염시키지 않고 런타임 전역(Fraction, math)을 주입합니다.
  4. 계약 리플렉션: 컴파일된 함수 객체에 _loop_summary와 _invariant_contract를 첨부하여 다운스트림 컴파일러와 검증 도구가 기본 전이 행렬 $\mathbf{A}$를 검사할 수 있게 합니다.
  5. 우아한 폴백: 비선형 인덱싱이나 지원되지 않는 동적 호출이 발생하면 Strilight는 진단 경고를 출력하고 충돌 없이 네이티브 실행으로 깔끔하게 폴백합니다.
from strilight import accelerate

@accelerate
def compute_simulation(steps: int) -> int:
    acc = 0
    for i in range(steps):
        acc += (i * 3) + 7
    return acc

# Executes in O(1) time (~0.001 ms even if steps = 100,000,000)
result = compute_simulation(100_000_000)

4. 계약 기반 C 소스 지시문 (#pragma strilight)

Python의 동적 리플렉션과 달리, Strilight의 C 코드 변환은 OpenMP 스타일의 pragma 지시문을 통해 명시적인 개발자-계약 모델을 엄격히 따릅니다. 엔진은 C 소스 코드를 암묵적으로 변경하지 않으며, 변환은 명시적인 개발자 계약 조항(contract, target, include, model)에 의해서만 수행됩니다:

  • #pragma strilight accelerate: 주석이 달린 C for 루프를 동등한 닫힌 형식의 수학적 표현으로 변환하도록 Strilight에 명시적으로 권한을 부여합니다.
  • #pragma strilight fuse: 동일한 반복 도메인을 공유하는 지정된 인접 루프들을 통합된 $\mathcal{O}(\log N)$ 이진 행렬 재귀 커널로 융합하도록 Strilight에 지시하는 명시적 개발자 지시문입니다.
// Example of contract-guided multi-loop fusion via developer directive
int simulate_motion(int n) {
    int pos = 0, vel = 10;

    #pragma strilight fuse
    for (int i = 0; i < n; i++) {
        pos += vel;
    }
    for (int i = 0; i < n; i++) {
        vel += 2;
    }
    return pos;
}

5. 파일 간 심볼 및 상수 해석 (CrossFileResolver)

수치 시뮬레이션은 종종 별도의 헤더 파일이나 구성 모듈에 매개변수를 정의합니다. Strilight의 CrossFileResolver는:

  • 로컬 모듈 임포트와 C #include / #define 지시문을 정적으로 추적합니다.
  • 임의의 런타임 코드를 실행하거나 안전하지 않은 eval을 사용하지 않고, AST 평가를 통해 파일 간 리터럴 상수 표현식(예: SOLAR_MASS = 4 * PI * PI)을 평가합니다.

6. 배열 슬라이스 유도 및 순환 테이블 조회

  • 순환 배열 조회: 순환 테이블 조회(table[i % P])를 $\mathcal{O}(1)$의 사전 계산된 누적 합 닫힌 공식으로 승격시킵니다.
  • 제자리 배열 슬라이스 변형: 상수 채우기와 등차수열을 분류하여 최적의 하드웨어 memset 호출 또는 벡터 슬라이스 할당(arr[:N] = ...)을 합성합니다.

7. 물리적 및 운동학적 가속의 내부 동작 원리

역학 및 천체물리학 시뮬레이션(예: $N$-체 시스템, 궤도 역학, 입자 운동학)에서 물리적 물체는 급격한 충돌이나 방향 변화 없이 매끄럽고 교란되지 않은 궤적을 따라 상당한 기간을 보내는 경우가 많습니다:

  • 해석적 궤적 합성: Strilight가 입자나 천체가 교란되지 않은 중력 또는 선형 궤적을 따르고 있음을 식별하면, 반복적인 시간 단계 루프를 가능한 최소한의 수학적 연산(해석적 케플러/조화 궤도 공식화)으로 축소합니다—좌표 정밀도를 희생하지 않으면서.
  • 복잡한 이벤트로의 전환: 복잡한 이벤트(이산 충돌, 경계 벽 충돌, 또는 불규칙한 다체 결합)가 발생하면, 실행은 특수한 충돌 결합 행렬($\mathbf{A}$) 또는 국소화된 시뮬레이션 단계로 전환됩니다.
  • 코드 위험 제로: Strilight는 완전히 비침투적입니다. Python에서는 단일 @accelerate 데코레이터이며, C에서는 표준 #pragma입니다. 알고리즘이나 비즈니스 로직을 변경하지 않고 언제든지 추가하거나 제거할 수 있습니다.
  • 결정적이고 우아한 폴백: Strilight가 비구조적 부작용, 알 수 없는 외부 호출, 또는 비아핀 동역학을 가진 루프를 만나면, 가속 시도를 결정적이고 깔끔하게 중단하고 네이티브 실행으로 폴백합니다. 프로그램은 절대 충돌하지 않습니다.

8. AI 코딩 어시스턴트와 함께 작업하고 가속된 코드 검사하기

최신 AI 코딩 어시스턴트(예: Claude, Gemini, GPT, Jules)는 대수 공식과 닫힌 형식 방정식 위에서 작동할 때 뛰어난 성능을 발휘합니다. Strilight는 개발자와 AI 에이전트가 합성된 코드와 수학적 계약을 직접 검사하는 것을 간단하게 만듭니다:

Python에서 수학적 계약 검사하기:

from strilight import accelerate

@accelerate
def compute_energy(steps: int) -> int:
    total = 0
    for i in range(steps):
        total += 15
    return total

# Execute once to trigger definition-time synthesis
result = compute_energy(100)

# Inspect the underlying mathematical contract:
summary = compute_energy._loop_summary
print("Extracted Induction Formulas:", summary.to_induction_formulas())
print("Invariant Contract:", compute_energy._invariant_contract.to_dict())

독립형 가속 C 소스 생성:

검사 가능하고 사람이 읽을 수 있는 가속 C 커널을 생성하려면 C 소스 코드를 accelerate_c_source에 직접 전달할 수 있습니다:

import strilight as sl

c_source = """
long long simulate(void) {
    long long total = 0;
    #pragma strilight accelerate target(total)
    for (int i = 0; i < 1000000; i++) {
        total += 42;
    }
    return total;
}
"""

accelerated_c = sl.accelerate_c_source(c_source)
print(accelerated_c)
# Emits: total += (42LL * 1000000);

9. 현실적인 기대치와 개발자 계약

우리는 엔지니어링 투명성을 믿습니다:

  • 일괄 보장 없음: Strilight는 임의의, 제약 없는 모든 루프가 마법처럼 $\mathcal{O}(1)$이 된다고 주장하지 않습니다. 고도로 불규칙한 포인터 추적, 임의의 동적 I/O, 또는 비대수적 외부 함수 호출은 근본적으로 축소 불가능합니다.
  • 예측 가능한 성공: 구조화된 루프—스칼라 리덕션, 다변수 선형 결합, 순환 배열, 계약 기반 루프—의 경우 Strilight는 안정적으로 성공합니다. C에서는 명시적 pragma 절(target, include, model)을 제공하면 결정론적 변환 보장이 제공됩니다.

벤치마크 결과

높은 반복 횟수의 수치 루프 전반에서 평가하여, 네이티브 실행과 Strilight 가속을 비교했습니다:

벤치마크 시나리오반복 횟수 ($N$)네이티브 기준선Strilight 가속측정된 속도 향상정밀도 충실도
결합 4x4 선형 시스템 (Python)$1,000,000$$75.2\text{ ms}$$0.0002\text{ ms}$$376,000\times$100% 비트 단위 정확
결합 4x4 선형 시스템 (GCC -O2)$1,000,000$$1.1\text{ ms}$$0.00002\text{ ms}$$55,000\times$100% 비트 단위 정확
순환 배열 조회 합산$1,000,000$$74.8\text{ ms}$$0.0044\text{ ms}$$17,000\times$100% 비트 단위 정확
행성 N-바디 천체 역학$100,000$$7.17\text{ ms}$$0.051\text{ ms}$$140\times$해석적 궤도 일치

아키텍처 및 실행 파이프라인

도구 다운로드