CoBRA

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)**은 복잡한 하위 표현식을 가상 변수로 대체하고 단순화된 외부 골격을 푼 다음 다시 치환합니다.

기능

• 선형 MBA 단순화 — 시그니처 벡터와 CoB 변환을 통한 비트별 원자의 가중 합
• 스케일 패턴 매칭 — 4-5 변수 부울 표현식에 대한 Shannon 분해를 사용하는 k * f(vars) + c
• 반선형 지원 — XOR/OR/NOT-AND 상수 변환, 구조 복원, 항 정제, 비트 분할 재구성을 통한 상수 마스크 원자 처리
• 다항식 복원 — 계수 분할과 유한 차분을 통한 다중선형 항 및 단일 거듭제곱 검출
• 혼합 곱 처리 — 코어 추출, 잔차 풀이, 고스트 잔차 분류를 포함한 분해 엔진
• 하위 표현식 리프팅 — 복잡한 하위 트리를 가상 변수로 대체하여 문제 차원 축소
• 워크리스트 오케스트레이터 — 중복 제거와 제한된 검색을 갖춘 DAG 인지 패스 스케줄링
• 경쟁 그룹 — 로컬 대안 분기와 하위 풀이는 연속(continuation)을 사용한 비용 기반 승자 선택을 사용
• 상수 시프트 — <<는 곱셈으로 디슈가링되고, >>는 반선형 기법으로 단순화됩니다
• ANF 정리 — 흡수, 공통 큐브 인수분해, OR 인식
• 비트폭 구성 가능 — 1비트~64비트 모듈러 연산
• 보조 변수 제거 — 항이 상쇄될 때 변수 수 감소
• Z3 검증 — 단순화된 출력의 선택적 동치 확인
• 스팟 체크 자체 테스트 — Z3를 사용할 수 없을 때의 경량 무작위 입력 검증
• LLVM 패스 플러그인 — 컴파일러 파이프라인에 직접 통합 (LLVM 19-22 필요)

빌드

선택적 의존성(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

LLVM 패스 플러그인 사용

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