astean1001/ProMBA

# ProMBA ProMBA 是一个基于程序合成、项重写和等式饱和的混合布尔算术表达式去混淆工具。 ## 依赖 - opam(https://opam.ocaml.org/)：用于 ocaml 编译器 ``` $ sudo apt-get install -y opam $ opam init --auto-setup --disable-sandboxing --yes ``` - libgmp-dev(https://gmplib.org/)：用于 z3 求解器 ``` $ sudo apt-get install -y libgmp-dev ``` - python3 : 用于线性去混淆工具 ([SiMBA](https://github.com/DenuvoSoftwareSolutions/SiMBA)) 和 [MBASolver](https://github.com/softsec-unh/MBA-Solver) ``` $ sudo apt-get install -y python3 ``` - libopenblas-dev (https://www.openblas.net/) : 用于 numpy ``` $ sudo apt-get install -y libopenblas-dev ``` - fortran : 用于 numpy ``` $ sudo apt-get install -y gfortran ``` - rust : 用于等式饱和 ``` $ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh ``` - 程序合成器 : 至少需要以下工具之一 - duet (https://github.com/astean1001/duet) $ git clone https://github.com/astean1001/duet.git $ cd duet $ ./build $ make - simba (https://github.com/astean1001/simba_synth) $ git clone https://github.com/astean1001/simba_synth.git $ cd simba_synth $ ./first_build.sh - eusolver (https://bitbucket.org/abhishekudupa/eusolver) $ git clone https://bitbucket.org/abhishekudupa/eusolver.git $ cd eusolver $ ./scripts/build.sh ## 构建 ### 快速开始 - 使用预构建的 Docker 镜像 ``` $ docker pull astean1001/promba:v1 ``` ### 手动构建 0. TL;DR，使用单行命令完成 ``` $ ./build.sh ``` 1. 配置合适的 ocaml 环境并获取依赖包 ``` opam switch create promba 4.05.0 opam switch promba opam install --yes dune z3 batteries cil yojson lacaml integers ``` ### 必需的 OPAM 包 - dune : 构建系统 - z3 : SMT 求解器 - batteries : 扩展标准库 - cil : 读取 C 函数 - yojson : 读取 JSON 格式 - lacaml : 线性代数计算 (用于 MBABlast) - integers : 扩展整数数据类型 (用于 MBABlast) 2. 使用 dune 进行构建 ``` dune build ``` 编译后的可执行文件可以在 `main.exe` 找到。（或者是 `promba.exe`）由于该可执行文件是自包含的，您可以方便地将其移动或复制到任何位置并执行。 3. 设置合成器脚本 编写一个仅以 SyGuS 格式输出目标合成函数的脚本，类似于本仓库中的 `simbas.sh` 或 `duet.sh`。 4. 运行去混淆工具 直接使用包含混淆 MBA 函数的目标 C 文件运行该可执行程序即可。 包含 MBA 函数的 C 文件必须满足以下条件： - 包含每个 MBA 混淆表达式的函数必须以 'target_' 开头命名。 - 该 C 文件必须是经过 CIL 转换的文件。 ``` $ ./promba.exe [a C input file] ``` 您可以通过以下方式查看可用选项： ``` $ ./promba.exe -help ``` 例如，要解决 `loki_benchmark/loki.c` 中描述的 `target_499` 问题， ``` $ ./promba.exe -timeout 4000.0 -rulefile ./no.rules -norule -height 3 -timeout_sygus 3.0 -sygus ./simbas.sh -synth2 ./synth.sh -lsolver ./simbad -single target_499 ./loki_benchmark/loki.c ``` 您将得到以下输出： ``` [2023-09-12 12:36:01] Parsing File: ./loki_benchmark/loki.c [2023-09-12 12:36:05] Solving Problem: target_499 ... [2023-09-12 12:37:17] Deobfuscation Result: (x + (-1 * y)) [2023-09-12 12:37:17] timeout : 3.000000 [2023-09-12 12:37:17] Answer Found (Checker Solved) :: (x - y) [2023-09-12 12:37:17] Answer Found (Solver Solved) :: (x + ((- 1) * y)) ``` 并且您可以在 result.txt 中看到以下输出： ``` Name: target_499, Result: (x - y), Size: 3, OrigSize: 1120, VarNum: 2, IsPoly: false, AlterOrig: 128, AlterDeob: 0, RuleNumber: 31, RuleCount: 200, LinearReduce: 732, SynthReduce: 248, RuleReduce: 140, Time: 72.000000 ``` `result.txt` 中的每个条目具有以下含义： - Name: 问题名称 - Result: 去混淆结果的表达式 - Size: 去混淆后表达式中的 AST 节点数 - OrigSize: 原始表达式中的 AST 节点数 - VarNum: 原始表达式中使用的变量数 - IsPoly: 是否为多项式 MBA - AlterOrig: 原始表达式中的 MBA 交替 - AlterDeob: 去混淆后表达式中的 MBA 交替 - RuleNumber: 学习到的规则数量 - RuleCount: 规则被应用的次数 - LinearReduce: 线性去混淆工具减小的尺寸 - SynthReduce: 程序合成器减小的尺寸 - RuleReduce: 项重写器减小的尺寸 - Time: 总执行时间 ## 如何评估数据集 您可以通过 `./run_test.` 来评估基准测试。 ## 参考文献 [1] Jaehyung, L., Woosuk L. (2023, November). Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Term Rewriting. In Proceedings of the 30th ACM Conference on Computer and Communications Security (CCS) 2023

标签：DNS 反向解析, 代码安全分析, 去混淆, 可视化界面, 可配置连接, 客户端加密, 漏洞数据库, 程序分析, 程序合成, 请求拦截, 逆向工具, 项重写