Coefficient-Based Reconstruction of 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 使用基于工作列表的编排器来简化表达式。每个输入作为带有状态类型标签的工作项进入工作列表。调度器根据项目状态、先决依赖关系和防止冗余工作的尝试缓存来选择下一个要运行的通行(pass)。
36 个离散的通行被组织成几个系列:AST 处理、基于签名技术、半线性技术、分解和提升。一些通行会分叉出局部替代方案或子求解,由竞争组解决;在这些组之外,工作列表返回第一个完全验证的顶层候选。所有结果通过随机输入抽样检查(默认)或 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)。表达式被分解为加权的位原子,然后结构恢复和项优化简化中间表示,最后按位分区的 OR 重组重建最终结果。
分解 针对包含位运算子表达式乘积的混合表达式。提取多项式核心,然后对残差进行分类和求解(多项式、布尔零/幻影或模板回退)。
提升 将复杂子表达式替换为虚拟变量,求解简化后的外部骨架,然后代回。
k * f(vars) + c 结合 Shannon 分解,适用于 4-5 变量布尔表达式<< 转换为乘法,>> 通过半线性技术简化详见 BUILD.md,包括可选依赖(LLVM、Z3)。
# 构建依赖(Abseil、Highway;可选 GoogleTest、LLVM、Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps
# 构建 CoBRA
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCMAKE_BUILD_TYPE=Release
cmake --build build
#(可选)构建并运行测试
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
# 基本简化
cobra-cli --mba "(x&y)+(x|y)"
# 指定位宽度
cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16
# 启用 Z3 等价性验证
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify
# 详细输出(显示中间流水线步骤)
cobra-cli --mba "(x&y)+(x|y)" --verbose
lib/core/ 核心简化引擎(约50个源文件)
Orchestrator 工作列表调度器、状态机、主简化循环
OrchestratorPasses 39 个通行注册表,带有向无环图感知调度
CompetitionGroup 多技术竞赛和胜者选择
ContinuationTypes 通行组合的延迟重组数据
JoinState 多操作数连接跟踪,用于结构重写
SignatureSimplifier 基于签名的技术(CoB、模式匹配、ANF)
SignatureVector 在 {0,1}^n 输入上求值表达式
AuxVarEliminator 通过检测抵消减少变量数
PatternMatcher 识别位运算模式(2变量/3变量表、缩放形式)
CoeffInterpolator 蝴蝶插值,用于系数恢复
CoBExprBuilder 从 CoB 系数重建表达式
AnfTransform 代数范式转换
AnfCleanup 吸收、因子提取、OR 识别
CoefficientSplitter 分离位运算与算术贡献
ArithmeticLowering 将算术片段降级为多项式中间表示(IR)
PolyNormalizer 多项式表达式的规范形式
SingletonPowerRecovery 通过有限差分检测 x^k 项
DecompositionEngine 提取-求解循环:多项式核心 + 残差求解
GhostBasis 幻影基元库(mul_sub_and, mul3_sub_and3)
GhostResidualSolver 布尔零分类和幻影残差求解
WeightedPolyFit 2-adic 加权线性求解多项式商
MixedProductRewriter 将位运算乘积展开为线性求和
TemplateDecomposer 混合表达式的有界模板匹配
ProductIdentityRecoverer 恢复和积恒等式
SemilinearNormalizer 分解为加权的位原子
SemilinearSignature 逐位签名评估和线性捷径
StructureRecovery XOR 恢复、掩码消除、项合并
TermRefiner 死位掩码约简、同系数合并
BitPartitioner 按语义特征分组位位置
MaskedAtomReconstructor 使用 OR 重写重组不相交掩码
Evaluator 编译后的表达式求值器
lib/llvm/ LLVM 通行插件(CobraPass, MBADetector, IRReconstructor)
lib/verify/ Z3 等价性验证
include/cobra/ 公开头文件
tools/cobra-cli/ 命令行前端和表达式解析器
test/ 1195 个测试,分布在约 63 个测试文件中
CoBRA 包含 1195 个测试,覆盖单元测试、集成测试和数据集基准测试:
# 运行所有测试
ctest --test-dir build --output-on-failure
# 运行特定测试套件
ctest --test-dir build -R test_simplifier --output-on-failure
# 带详细输出运行
ctest --test-dir build -V
数据集基准测试针对来自多个独立来源的真实世界混淆表达式进行验证。参见 DATASETS.md 获取完整基准测试报告——来自 7 个独立来源的 35 个数据集文件中的 75,126 个表达式。
感谢 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/ 中的测试数据集来自第三方研究项目,按其原始许可证(主要为 GPL-3.0)重新分发。详见 THIRD_PARTY_LICENSES。
| 标志 | 默认值 | 描述 |
|---|
--mba <expr> | 要简化的表达式 | |
--bitwidth <n> | 64 | 模算术宽度(1-64) |
--max-vars <n> | 16 | 最大变量数 |
--verify | 关闭 | Z3 等价性检查 |
--verbose | 关闭 | 打印流水线内部细节 |