trailofbits/cobra산술 연산의 계수 기반 재구성 — 난독화 해제를 위한 혼합 부울-산술(MBA) 표현식 단순화 도구
Coefficient-Based Reconstruction of Arithmetic — 혼합 부울-산술(Mixed Boolean-Arithmetic) 표현식 단순화기.
CoBRA는 산술(+, -, *) 연산자와 비트 연산(&, |, ^, ~) 및 시프트(<<, >>) 연산자가 섞여 있는 표현식을 디난독화합니다. 이는 소프트웨어 난독화에서 흔히 사용되는 기법입니다.
$ cobra-cli --mba "(x&y)+(x|y)"
x + y
$ cobra-cli --mba "((a^b)|(a^c)) + 65469 * ~((a&(b&c))) + 65470 * (a&(b&c))" --bitwidth 16
67 + (a | b | c)
$ cobra-cli --mba "((a^b)&c) | ((a&b)^c)"
c ^ a & b
$ cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16
x
$ cobra-cli --mba "(x ^ 0x10) + 2 * (x & 0x10)"
16 + x
$ cobra-cli --mba "x << 3"
8 * x
$ cobra-cli --mba "~x"
~x
$ cobra-cli --mba "(x^y)*(x&y) + 3*(x|y)"
(x ^ y) * (x & y) + 3 * (x | y)
$ cobra-cli --mba '-357*(x&~y)*(x&y)+102*(x&~y)*(x&~y)+374*(x&~y)*~(x^y)
-306*(x&~y)*~(x|y)-17*(x&~y)*~(x|~y)-105*~(x|~y)*(x&y)+30*~(x|~y)*(x&~y)
+110*~(x|~y)*~(x^y)-90*~(x|~y)*~(x|y)-5*~(x|~y)*~(x|~y)+34*(x&~y)*~x
-85*(x&~y)*~y+10*~(x|~y)*~x-25*~(x|~y)*~y'
22 * (x & y) + -17 * x + -5 * y
CoBRA는 워크리스트 기반 오케스트레이터를 사용하여 표현식을 단순화합니다. 각 입력은 상태 종류(state kind)로 태그된 작업 항목으로 워크리스트에 들어갑니다. 스케줄러는 항목의 상태, 사전 요구 의존성, 그리고 중복 작업을 방지하는 시도 캐시를 기반으로 다음에 실행할 패스를 선택합니다.
36개의 개별 패스는 AST 처리, 시그니처 기반 기법, 반선형(semilinear) 기법, 분해, 리프팅 계열로 구성됩니다. 일부 패스는 경쟁 그룹에 의해 해결되는 로컬 대안 또는 하위 풀이를 분기합니다. 이러한 그룹 외부에서는 워크리스트가 완전히 검증된 첫 번째 최상위 후보를 반환합니다. 모든 결과는 무작위 입력 스팟 체크(기본) 또는 Z3 동치 증명(--verify)으로 검증됩니다.
Input Expression
|
[Worklist Scheduler]
|
Work items flow through state kinds:
|
kFoldedAst ──> AST processing passes
| (classify, lower, rewrite)
|
+──> kSignatureState ──> Signature techniques
| (pattern match, CoB, ANF, polynomial recovery)
|
+──> kSemilinearNormalizedIr ──> Semilinear techniques
| (normalize, recover structure, refine, reconstruct)
|
+──> kCoreCandidate / kRemainderState ──> Decomposition
| (extract core, classify residual, solve)
|
+──> kLiftedSkeleton ──> Lifting
| (virtual variable substitution, outer solve)
|
+──> kCandidateExpr ──> Verification
(spot-check or Z3 proof)
|
Simplified Expression
시그니처 기반 기법은 모든 부울 입력에 대해 표현식을 평가하여 시그니처 벡터를 얻습니다. CoB 버터플라이 변환은 AND-곱 기저 계수를 복원합니다. 패턴 매칭, ANF, 다항식 복원은 서로 다른 복잡도 수준을 처리합니다.
반선형 기법은 상수 마스크(예: x & 0xFF)를 가진 표현식을 처리합니다. 표현식을 가중 비트별 원자(weighted bitwise atom)로 분해한 다음, 구조 복원과 항 정제(term refinement)가 중간 표현을 단순화하고, 비트 분할 OR-조립이 최종 결과를 재구성합니다.
**분해(Decomposition)**는 비트별 하위 표현식의 곱을 포함하는 혼합 표현식을 대상으로 합니다. 다항식 코어를 추출한 다음, 잔차를 분류하고 풉니다(다항식, 부울-널/고스트, 또는 템플릿 폴백).
**리프팅(Lifting)**은 복잡한 하위 표현식을 가상 변수로 대체하고 단순화된 외부 골격을 푼 다음 다시 치환합니다.
k * f(vars) + c<<는 곱셈으로 디슈가링되고, >>는 반선형 기법으로 단순화됩니다선택적 의존성(LLVM, Z3)을 포함한 자세한 내용은 BUILD.md를 참조하세요.
# Build dependencies (Abseil, Highway; optionally GoogleTest, LLVM, Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps
# Build CoBRA
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCMAKE_BUILD_TYPE=Release
cmake --build build
# (Optional) Build and run tests
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release -DCOBRA_BUILD_TESTS=ON
cmake --build build-deps
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCMAKE_BUILD_TYPE=Release \
-DCOBRA_BUILD_TESTS=ON
cmake --build build
ctest --test-dir build --output-on-failure
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCOBRA_BUILD_LLVM_PASS=ON \
-DCMAKE_BUILD_TYPE=Release
cmake --build build
# Basic simplification
cobra-cli --mba "(x&y)+(x|y)"
# Specify bitwidth
cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16
# Enable Z3 equivalence verification
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify
# Verbose output (show intermediate pipeline steps)
cobra-cli --mba "(x&y)+(x|y)" --verbose
lib/core/ Core simplification engine (~50 source files)
Orchestrator Worklist scheduler, state machine, main simplification loop
OrchestratorPasses 39-pass registry with DAG-aware scheduling
CompetitionGroup Multi-technique racing and winner selection
ContinuationTypes Deferred recombination data for pass composition
JoinState Multi-operand join tracking for structural rewrites
SignatureSimplifier Signature-based techniques (CoB, pattern matching, ANF)
SignatureVector Evaluate expression on {0,1}^n inputs
AuxVarEliminator Reduce variable count by detecting cancellations
PatternMatcher Recognize bitwise patterns (2-var/3-var tables, scaled)
CoeffInterpolator Butterfly interpolation for coefficient recovery
CoBExprBuilder Reconstruct expressions from CoB coefficients
AnfTransform Algebraic Normal Form conversion
AnfCleanup Absorption, factoring, OR recognition
CoefficientSplitter Separate bitwise vs. arithmetic contributions
ArithmeticLowering Lower arithmetic fragment to polynomial IR
PolyNormalizer Canonical form for polynomial expressions
SingletonPowerRecovery Detect x^k terms via finite differences
DecompositionEngine Extract-solve loop: polynomial core + residual solving
GhostBasis Ghost primitive library (mul_sub_and, mul3_sub_and3)
GhostResidualSolver Boolean-null classification and ghost residual solving
WeightedPolyFit 2-adic weighted linear solve for polynomial quotients
MixedProductRewriter Expand bitwise products into linear sums
TemplateDecomposer Bounded template matching for mixed expressions
ProductIdentityRecoverer Recover product-of-sums identities
SemilinearNormalizer Decompose into weighted bitwise atoms
SemilinearSignature Per-bit signature evaluation and linear shortcut
StructureRecovery XOR recovery, mask elimination, term coalescing
TermRefiner Dead-bit mask reduction, same-coefficient merge
BitPartitioner Group bit positions by semantic profile
MaskedAtomReconstructor Reassemble with OR-rewrite for disjoint masks
Evaluator Compiled expression evaluator
lib/llvm/ LLVM pass plugin (CobraPass, MBADetector, IRReconstructor)
lib/verify/ Z3-based equivalence verification
include/cobra/ Public headers
tools/cobra-cli/ CLI frontend and expression parser
test/ 1195 tests across ~63 test files
CoBRA에는 단위, 통합, 데이터셋 벤치마크를 포함한 1195개의 테스트가 있습니다:
# Run all tests
ctest --test-dir build --output-on-failure
# Run a specific test suite
ctest --test-dir build -R test_simplifier --output-on-failure
# Run with verbose output
ctest --test-dir build -V
데이터셋 벤치마크는 여러 독립 소스의 실제 난독화된 표현식으로 검증합니다. 전체 벤치마크 보고서는 DATASETS.md를 참조하세요 — 7개의 독립 소스에 걸친 35개 데이터셋 파일의 75,126개 표현식.
{0,1} 입력에서 올바르지만 전체 비트폭에서는 올바르지 않은 CoB 후보를 생성합니다(AND-곱 기저와 산술 곱셈의 차이). 이들은 감지되어 verify-failed로 정확히 보고됩니다.Bas Zweers와 Back Engineering 팀이 이 프로젝트를 구성하는 데 도움을 준 영감과 지도에 감사드립니다. 추천 영상: 그들의 re//verse 2026 발표 Deobfuscation of a Real World Binary Obfuscator.
지속적인 검토와 테스트에 기여한 Jack Royer, Matteo Favaro, Arnau Gàmez 및 기타 익명 기여자들에게도 감사드립니다.
Apache-2.0. test/datasets/의 테스트 데이터셋은 제3자 연구 프로젝트에서 원래 라이선스(주로 GPL-3.0)에 따라 재배포된 것입니다. 자세한 내용은 THIRD_PARTY_LICENSES를 참조하세요.
| Flag | Default | Description |
|---|
--mba <expr> | 단순화할 표현식 | |
--bitwidth <n> | 64 | 모듈러 연산 비트폭 (1-64) |
--max-vars <n> | 16 | 최대 변수 개수 |
--verify | off | Z3 동치 확인 |
--verbose | off | 파이프라인 내부 정보 출력 |