trailofbits/CoBRA
GitHub: trailofbits/CoBRA
基于系数重建的混合布尔算术表达式简化器，用于破解软件保护中的 MBA 混淆并还原可读表达式。
Stars: 59 | Forks: 4
# CoBRA
**Co**efficient-**B**ased **R**econstruction of **A**rithmetic —— 一个混合布尔算术表达式简化器。
[](LICENSE)
[](https://en.cppreference.com/w/cpp/23)
[](#testing)
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 & 255 | x & -256
$ cobra-cli --mba "(x ^ 0x10) + 2 * (x & 0x10)"
16 + x
$ cobra-cli --mba "x << 3"
8 * x
```
## 工作原理
CoBRA 对每个表达式进行分类，并将其路由到适当的流水线：
| 流水线 | 输入 | 技术 |
|----------|-------|-----------|
| **Linear** | 按位原子的加权和 | 签名向量 → CoB 蝶形变换 → 模式匹配 / ANF 清理 |
| **Semilinear** | 常量掩码原子 (`x & 0xFF`) | 常量 lowering、结构恢复、项精细化、位分区重构 |
| **Polynomial** | 变量乘积 (`x*y`, `x^2`) | 系数拆分 + 单例幂次恢复 |
| **Mixed** | 按位子表达式的乘积 | 多步重写、分解引擎（extract-solve）、ghost 残差求解 |
核心理念是 **基变换**：在所有 2^n 个布尔输入上对表达式求值以生成签名向量，然后应用蝶形递推以恢复每个 AND-product 基项的系数。模式匹配可识别所有 2 变量和 3 变量布尔函数，包括像 `67*(a|b|c)` 这样的缩放形式。对于 4 变量和 5 变量布尔表达式，**Shannon 分解** 递归地在一个变量上进行拆分，以简化为查找表所覆盖的较小情况。复杂的布尔结果会回退到 ANF（代数正规形式），并执行清理步骤以进行吸收、公共立方提取和 OR 识别。
## 功能特性
- **Linear MBA 简化** —— `&`, `|`, `^`, `~` 与 `+`, `-`、常量乘数的任意组合
- **缩放模式匹配** —— 形如 `k * f(vars) + c` 的表达式，其中 `f` 是一个按位函数；Shannon 分解将覆盖范围扩展到 4 变量和 5 变量布尔表达式
- **Semilinear 支持** —— 诸如 `x & 0xFF`, `y | 0xF0` 的常量掩码原子，支持 XOR/OR/NOT-AND 常量 lowering、结构恢复（XOR 恢复、掩码消除）、项精细化、合并以及位分区 OR 组装重构
- **Polynomial 恢复** —— 通过系数拆分处理多线性项（`x*y`）和单例幂次（`x^2`）
- **Mixed 乘积处理** —— 多步重写流水线，包含操作数简化、乘积恒等式折叠和 XOR lowering
- **分解引擎** —— extract-solve 架构，将混合表达式拆分为多项式核心和残差，并提供强化的全宽验证和针对 boolean-null 分量的 ghost 残差求解
- **常量移位** —— `<<` 解糖为乘法，按位子树上的 `>>` 通过 semilinear 流水线进行简化
- **ANF 清理** —— 吸收、公共立方提取和 OR 识别，以获得紧凑的布尔输出
- **可配置位宽** —— 1 位到 64 位模算术
- **辅助变量消元** —— 当项抵消时减少变量数量
- **Z3 验证** —— 可选的简化输出等价性检查
- **Spot-check 自检** —— 当 Z3 不可用时的轻量级随机输入验证
- **LLVM pass plugin** —— 直接集成到编译器流水线中（需要 LLVM 19-22）
## 构建
有关包括可选依赖项（LLVM, Z3）在内的完整详细信息，请参阅 [BUILD.md](BUILD.md)。
```
# 构建依赖项 (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
# 运行测试
ctest --test-dir build --output-on-failure
```
### 仅 CLI（无 LLVM）
```
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCOBRA_BUILD_LLVM_PASS=OFF \
-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
# 详细输出 (显示中间 pipeline 步骤)
cobra-cli --mba "(x&y)+(x|y)" --verbose
```
### 选项
| 标志 | 默认值 | 描述 |
|------|---------|-------------|
| `--mba ` | | 要简化的表达式 |
| `--bitwidth ` | 64 | 模算术宽度 (1-64) |
| `--max-vars ` | 16 | 最大变量数量 |
| `--verify` | off | Z3 等价性检查 |
| `--strict` | off | Semilinear 结果需要 Z3 |
| `--verbose` | off | 打印流水线内部状态 |
## 项目结构
```
lib/core/ Core simplification pipeline (45 source files)
Simplifier Top-level orchestration and route dispatch
Classifier Route: Linear / Semilinear / Polynomial / Mixed
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 (XOR/OR/NOT-AND lowering)
SemilinearSignature Per-bit signature evaluation and linear shortcut detection
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
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/ 1017 tests across 55 test files (unit + integration + dataset benchmarks)
```
## 测试
CoBRA 包含 1017 个测试，涵盖单元测试、集成测试和数据集基准测试：
```
# 运行所有测试
ctest --test-dir build --output-on-failure
# 运行特定 test suite
ctest --test-dir build -R test_simplifier --output-on-failure
# 带详细输出运行
ctest --test-dir build -V
```
数据集基准测试针对来自多个独立来源的真实世界混淆表达式进行验证。完整基准测试报告请参阅 [DATASETS.md](DATASETS.md) —— 在来自 7 个独立来源的 32 个数据集文件中，共简化了 69,942 个表达式，零失败。
## 已知局限性
- **不支持乘积嵌套在按位运算内部的表达式** —— 当乘积嵌套在按位运算符内部（例如 `(a*b) & c`, `(a*b) ^ (c*d)`）时，超出了 CoBRA 当前的表示族范围。这些情况占剩余未简化案例的大多数。
- **部分 Mixed 乘积不支持** —— 当分解引擎无法提取有效的多项式核心或残差超出支持的族时，按位-乘积子表达式的复杂组合可能无法简化。
- **无通用逻辑最小化** —— CoBRA 使用贪婪代数重写，而非 Quine-McCluskey/Espresso/BDD。
## 致谢
感谢 [Bas Zweers](https://github.com/AnalogCyberNuke) 和 [Back Engineering](https://github.com/backengineering) 团队的启发和指导，帮助塑造了这个项目。推荐观看：他们在 re//verse 2026 大会上的演讲 [Deobfuscation of a Real World Binary Obfuscator](https://www.youtube.com/watch?v=3LtwqJM3Qjg)。
## 许可证
[Apache-2.0](LICENSE)
更多示例
``` $ cobra-cli --mba "~x" ~x $ cobra-cli --mba "(x^y)*(x&y) + 3*(x|y)" (x & y) * (x ^ y) + ~2 * -(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 ```标签：AST简化, Bash脚本, C++23, DNS 反向解析, DNS枚举, MBA表达式化简, TLS抓取, 云安全监控, 云资产清单, 代码反混淆, 布尔代数, 恶意代码分析, 指令还原, 混淆对抗, 算术运算, 编译器优化, 网络安全工具, 软件安全, 逆向工程, 配置文件, 静态分析