Skip to content
KitploitKITPLOIT
工具博客
提交
工具博客
提交

黑客、渗透测试和网络安全工具,武装您的安全武器库!

Kitploit 是一个黑客、网络安全和渗透测试工具的目录。发现最新的项目更新,查找漏洞、分析系统、自动化测试并加强你的安全。

··订阅源·联系·隐私·© 2026 Kitploit

工具目录

分类

查看所有分类
Loading categories
CoBRA — 基于系数的算术重构——一个用于去混淆的混合布尔算术(MBA)表达式简化器 | Kitploit
工具/GitHubGitHub/trailofbits/cobra
静态分析代码分析逆向工程密码学二进制分析
GitHubtrailofbits/cobra

CoBRA

基于系数的算术重构——一个用于去混淆的混合布尔算术(MBA)表达式简化器

查看仓库
323168天前Kitploit 审核通过

最受欢迎

查看全部 →

发现我们社区最常用的工具。

探索所有工具

浏览我们的工具集合

查看所有工具 →
分享

CoBRA

Coefficient-Based Reconstruction of Arithmetic — 混合布尔算术表达式简化器。

License: Apache-2.0 C++23 Tests

CoBRA 反混淆交织使用算术(+、-、*)与位运算(&、|、^、~)和移位(<<、>>)运算符的表达式——这是软件混淆中常用的一种技术。

root@kitploit:~
$ 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
更多示例
root@kitploit:~
$ 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)进行验证。

root@kitploit:~
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 重组重建最终结果。

分解 针对包含位运算子表达式乘积的混合表达式。提取多项式核心,然后对残差进行分类和求解(多项式、布尔零/幻影或模板回退)。

提升 将复杂子表达式替换为虚拟变量,求解简化后的外部骨架,然后代回。

特性

  • 线性 MBA 简化 — 通过签名向量和 CoB 变换的加权位原子和
  • 缩放模式匹配 — k * f(vars) + c 结合 Shannon 分解,适用于 4-5 变量布尔表达式
  • 半线性支持 — 常量掩码原子,带有 XOR/OR/NOT-AND 常量降级、结构恢复、项优化、按位分区重建
  • 多项式恢复 — 多线性项和单个幂次,通过系数分裂和有限差分
  • 混合乘积处理 — 分解引擎,核心提取、残差求解和幻影残差分类
  • 子表达式提升 — 将复杂子树替换为虚拟变量以降低问题维度
  • 工作列表编排器 — 有向无环图感知的通行调度,去重和有界搜索
  • 竞争组 — 局部替代分支和子求解使用基于代价的胜者选择与延续
  • 常量移位 — << 转换为乘法,>> 通过半线性技术简化
  • ANF 清理 — 吸收、公共立方因子提取和 OR 识别
  • 可配置位宽度 — 1 位到 64 位模算术
  • 辅助变量消除 — 当项抵消时减少变量数
  • Z3 验证 — 可选简化输出的等价性检查
  • 随机抽样自检 — 当 Z3 不可用时进行轻量级随机输入验证
  • LLVM 通行插件 — 直接集成到编译器流水线中(需要 LLVM 19-22)

构建

详见 BUILD.md,包括可选依赖(LLVM、Z3)。

root@kitploit:~
# 构建依赖(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

使用 LLVM Pass 插件

root@kitploit:~
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCOBRA_BUILD_LLVM_PASS=ON \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

用法

root@kitploit:~
# 基本简化
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

选项

项目结构

root@kitploit:~
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 个测试,覆盖单元测试、集成测试和数据集基准测试:

root@kitploit:~
# 运行所有测试
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 个表达式。

已知局限

  • 深度交织的混合多项式 MBA — 剩余不支持的表达式主要是大型、高度重复的 AST,交织了算术和位运算运算符。基于影响排序的子表达式提升恢复了其中许多,但在提升后仍然耗尽工作列表预算的表达式仍不支持
  • 布尔域重建发散 — 少量表达式产生的 CoB 候选在 {0,1} 输入上正确,但在全宽度下不正确(AND-积基与算术乘法)。这些会被检测到并正确报告为验证失败
  • 无通用逻辑最小化 — CoBRA 使用贪婪代数重写,而非奎因-麦克拉斯基/Espresso/BDD

致谢

感谢 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关闭打印流水线内部细节