JonathanSalwan/Triton

GitHub: JonathanSalwan/Triton

一款支持动态符号执行与污点分析的多架构二进制分析库，帮助安全研究者构建逆向工程、漏洞挖掘和软件验证等定制化分析工具。

Stars: 4125 | Forks: 577

**Triton** 是一个动态二进制分析库。它提供了内部组件，允许你构建自己的程序分析工具， 自动化逆向工程，执行软件验证或仅仅进行代码仿真。 * 动态**符号**执行 * 动态**污点**分析 * **x86**, **x86-64**, **ARM32**, **AArch64** 和 **RISC-V 32/64** ISA 语义的 AST 表示 * 表达式**合成** * SMT **简化**过程 * 提升到 **LLVM** 以及 **Z3** 并支持往返转换 * 连接到 **Z3** 和 **Bitwuzla** 的 **SMT solver** 接口 * **C++** 和 **Python** API


由于 **Triton** 算是一个业余项目，如果它不是完全可靠，请**不要责怪我们**。[提交 issue](https://github.com/JonathanSalwan/Triton/issues) 或 [拉取请求](https://github.com/JonathanSalwan/Triton/pulls) 总是比喷人更好 =)。当然，你可以在推特上关注开发动态 [@qb_triton](https://twitter.com/qb_triton)。

      Codecov      

# 快速开始 * [安装说明](#install) * [Python API](https://triton-library.github.io/documentation/doxygen/py_triton_page.html) * [C++ API](https://triton-library.github.io/documentation/doxygen/annotated.html) * [Python 示例](https://github.com/JonathanSalwan/Triton/tree/master/src/examples/python) * [他们已经在使用 Triton](#they-already-used-triton) ## 入门指南 ``` from triton import * >>> # Create the Triton context with a defined architecture >>> ctx = TritonContext(ARCH.X86_64) >>> # Define concrete values (optional) >>> ctx.setConcreteRegisterValue(ctx.registers.rip, 0x40000) >>> # Symbolize data (optional) >>> ctx.symbolizeRegister(ctx.registers.rax, 'my_rax') >>> # Execute instructions >>> ctx.processing(Instruction(b"\x48\x35\x34\x12\x00\x00")) # xor rax, 0x1234 >>> ctx.processing(Instruction(b"\x48\x89\xc1")) # mov rcx, rax >>> # Get the symbolic expression >>> rcx_expr = ctx.getSymbolicRegister(ctx.registers.rcx) >>> print(rcx_expr) (define-fun ref!8 () (_ BitVec 64) ref!1) ; MOV operation - 0x40006: mov rcx, rax >>> # Solve constraint >>> ctx.getModel(rcx_expr.getAst() == 0xdead) {0: my_rax:64 = 0xcc99} >>> # 0xcc99 XOR 0x1234 is indeed equal to 0xdead >>> hex(0xcc99 ^ 0x1234) '0xdead' ``` ## 使用 pip 安装 可以使用 `pip` 安装 Triton： ``` pip install triton-library ``` ## 从源码安装 Triton 依赖于以下项目： ``` * libcapstone >= 5.0.x https://github.com/capstone-engine/capstone * libboost (optional) >= 1.68 * libpython (optional) >= 3.6 * libz3 (optional) >= 4.6.0 https://github.com/Z3Prover/z3 * libbitwuzla (optional) >= 0.4.x https://github.com/bitwuzla/bitwuzla * llvm (optional) >= 12 ``` ### Linux 和 MacOS ``` $ git clone https://github.com/JonathanSalwan/Triton $ cd Triton $ mkdir build ; cd build $ cmake .. $ make -j3 $ sudo make install ``` 默认情况下，不会编译 LLVM 和 Bitwuzla。如果你想享受 Triton 的全部功能，cmake 编译命令如下： ``` $ cmake -DLLVM_INTERFACE=ON -DCMAKE_PREFIX_PATH=$(llvm-config --prefix) -DBITWUZLA_INTERFACE=ON .. ``` #### MacOS M1 注意事项： 如果你遇到如下编译错误： ``` Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS) ``` 尝试为你特定的 Python 版本指定 `PYTHON_EXECUTABLE`、`PYTHON_LIBRARIES` 和 `PYTHON_INCLUDE_DIRS`： ``` cmake -DCMAKE_INSTALL_PREFIX=/opt/homebrew/ \ -DPYTHON_EXECUTABLE=/opt/homebrew/bin/python3 \ -DPYTHON_LIBRARIES=/opt/homebrew/Cellar/python@3.10/3.10.8/Frameworks/Python.framework/Versions/3.10/lib/libpython3.10.dylib \ -DPYTHON_INCLUDE_DIRS=/opt/homebrew/opt/python@3.10/Frameworks/Python.framework/Versions/3.10/include/python3.10/ \ .. ``` 你可以通过以下代码片段获取这些信息： ``` from sysconfig import get_paths info = get_paths() print(info) ``` #### Python 自动补全 如果 Python 自动补全不起作用，请按照以下步骤操作： 1. 执行 [脚本](doc/autocomplete/generate_autocomplete.py) 2. 将生成的 triton.pyi 文件放置在你想要为其提供提示的 Triton 共享对象所在的同一目录中（例如，`/usr/lib/python3.13/`）。 你的 IDE 必须支持解析 .pyi 文件。 ### Windows 你可以使用 cmake 生成 libTriton 的 .sln 文件。 ``` > git clone https://github.com/JonathanSalwan/Triton.git > cd Triton > mkdir build > cd build > cmake -G "Visual Studio 14 2015 Win64" \ -DBOOST_ROOT="C:/Users/jonathan/Works/Tools/boost_1_61_0" \ -DPYTHON_INCLUDE_DIRS="C:/Python36/include" \ -DPYTHON_LIBRARIES="C:/Python36/libs/python36.lib" \ -DZ3_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/include" \ -DZ3_LIBRARIES="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/bin/libz3.lib" \ -DCAPSTONE_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/include" \ -DCAPSTONE_LIBRARIES="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/capstone.lib" .. ``` 不过，如果你希望直接下载预编译的库，请查看我们 AppVeyor 的 [构建产物](https://ci.appveyor.com/project/JonathanSalwan/triton/history)。 请注意，如果你使用了 AppVeyor 的构建产物，你可能需要安装适用于 Visual Studio 2012 的 [Visual C++ Redistributable](https://www.microsoft.com/en-US/download/details.aspx?id=30679) 包。 ### 从 vcpkg 安装 vcpkg 中的 Triton 端口由微软团队成员和社区贡献者保持更新。 vcpkg 的网址是：https://github.com/Microsoft/vcpkg。你可以使用 vcpkg 依赖管理器下载并安装 Triton： ``` $ git clone https://github.com/Microsoft/vcpkg.git $ cd vcpkg $ ./bootstrap-vcpkg.sh # ./bootstrap-vcpkg.bat for Windows $ ./vcpkg integrate install $ ./vcpkg install triton ``` 如果版本过期，请在 vcpkg 仓库中[创建 issue 或拉取请求](https://github.com/Microsoft/vcpkg)。 ## 他们已经在使用 Triton ### 工具 * [Exrop](https://github.com/d4em0n/exrop): 自动化 ROPChain 生成。 * [Pimp](https://github.com/kamou/pimp): 基于 Triton 的 R2 插件，用于符号执行和完全控制。 * [Ponce](https://github.com/illera88/Ponce): IDA 2016 插件大赛冠军！一键即可进行符号执行！ * [QSynthesis](https://github.com/quarkslab/qsynthesis): 用于汇编指令反混淆的灰盒合成器。 * [TritonDSE](https://github.com/quarkslab/tritondse): 基于 Triton 的 DSE 库，具有加载和探索功能。 * [Titan](https://github.com/archercreat/titan): Titan 是一个使用 Triton 的 VMProtect 反虚拟化工具。 ### 论文和会议
  • Sydr-Fuzz: Continuous Hybrid Fuzzing and Dynamic Analysis for Security Development Lifecycle
    报告地点: Ivannikov ISP RAS Open Conference, 莫斯科, 俄罗斯, 2022. [论文] [幻灯片]
    作者: Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Fedotov A.
    摘要: 如今，为了确保软件安全性并满足安全开发生命周期 (SDL) 的要求，对用于持续测试的自动化动态分析框架有着很高的需求。前沿混合模糊测试技术在查找安全漏洞方面的效率，显著优于广泛使用的覆盖率引导模糊测试。我们提出了一个增强的动态分析流水线，以提高基于混合模糊测试的自动化错误检测的生产力。我们在持续模糊测试工具集 Sydr-Fuzz 中实现了所提出的流水线，该工具集由混合模糊测试协调器驱动，集成了我们的 DSE 工具 Sydr 与 libFuzzer 和 AFL++。Sydr-Fuzz 还结合了安全谓词检查器、崩溃分类工具 Casr，以及用于语料库最小化和覆盖率收集的实用程序。我们将混合模糊测试器与替代的最先进解决方案进行了基准测试，结果表明其优于覆盖率引导的模糊测试器，同时与高级混合模糊测试器保持在同一水平。此外，我们通过在 OSS-Sydr-Fuzz 项目中发现 85 个真实世界的软件缺陷，验证了我们方法的有效性。最后，我们向社区开源了 Casr 源代码，以促进对现有崩溃的检查。

  • Strong Optimistic Solving for Dynamic Symbolic Execution
    报告地点: Ivannikov Memorial Workshop, 喀山, 俄罗斯, 2022. [论文] [幻灯片]
    作者: Parygina D., Vishnyakov A., Fedotov A.
    摘要: 动态符号执行 (DSE) 是一种用于自动化程序测试和错误检测的有效方法。它通过在混合模糊测试期间探索复杂分支来提高代码覆盖率。DSE 工具会沿着某些执行路径反转分支，并帮助模糊测试器检查以前无法访问的程序部分。DSE 经常面临过度约束和约束不足的问题。前者会导致分析显著复杂化，而后者会导致不准确的符号执行。我们提出了一种强乐观求解方法，可以消除与目标分支反转无关的路径谓词约束。我们消除了目标分支不依赖其控制的相关符号约束。此外，我们单独处理那些具有嵌套控制转移指令（将控制权传递到父分支范围之外，例如 return、goto、break 等）的符号分支。我们在动态符号执行工具 Sydr 中实现了所提出的方法。我们评估了强乐观策略、仅包含最后约束取反的乐观策略及其组合。结果表明，策略组合有助于增加代码覆盖率或提高每分钟正确反转分支的平均数量。与其他配置相比，将两种策略结合应用是最佳的。

  • Greybox Program Synthesis: A New Approach to Attack Dataflow Obfuscation
    报告地点: Blackhat USA, 拉斯维加斯, 内华达州, 2021. [幻灯片]
    作者: Robin David
    摘要: 本次演讲介绍了应用于反混淆的程序合成最新进展。旨在通过展示如何将这种分析技术应用于反混淆来揭开其神秘面纱。特别是为本次演讲发布的 Qsynthesis 实现，展示了一个完整的端到端工作流，将汇编指令反混淆回经过优化的（反混淆的）指令，并重新组装回二进制文件中。

  • From source code to crash test-case through software testing automation
    报告地点: C&ESAR, 雷恩, 法国, 2021. [论文] [幻灯片]
    作者: Robin David, Jonathan Salwan, Justin Bourroux
    摘要: 本文提出了一种从源代码到编译程序动态测试的自动化软件测试过程的方法。更具体地说，从指示源代码行警报的静态分析报告开始，它能够动态地覆盖这些代码行，并择机检查它们是否会触发崩溃。其结果是一个测试语料库，能够覆盖警报并在它们恰好为真阳性时触发它们。本文讨论了用于在编译后的二进制文件中追踪警报的方法论、测试引擎的选择过程，以及在针对嵌入式和 IoT 系统的 TCP/IP 协议栈实现上获得的结果。

  • Symbolic Security Predicates: Hunt Program Weaknesses
    报告地点: Ivannikov ISP RAS Open Conference, 莫斯科, 俄罗斯, 2021. [论文] [幻灯片]
    作者: A.Vishnyakov, V.Logunova, E.Kobrin, D.Kuts, D.Parygina, A.Fedotov
    摘要: 动态符号执行 (DSE) 是一种用于在混合模糊测试和自动错误检测期间进行路径探索的强大方法。我们提出了安全谓词来有效检测未定义行为和内存访问违规错误。最初，我们在不触发任何错误的路径上对程序进行符号执行（混合模糊测试可以探索这些路径）。然后我们构建一个符号安全谓词来验证某些错误条件。因此，我们可以改变程序数据流，导致空指针解引用、除零、越界访问或整数溢出等弱点。与静态分析不同，动态符号执行不仅报告错误，还生成新的输入数据以重现它们。此外，我们引入了针对常见 C/C++ 标准库函数的函数语义建模。我们的目标是使用单个符号公式对函数内部的控制流进行建模。这有助于错误检测，加速路径探索，并克服路径谓词中的过度约束问题。我们在动态符号执行工具 Sydr 中实现了所提出的技术。因此，我们利用了 Sydr 中的强大方法，例如消除无关约束的路径谓词切片。我们展示了 Juliet Dynamic 以测量动态错误检测工具的准确性。该测试系统还验证了生成的输入是否触发了清理器。我们评估了 Sydr 在 Juliet 测试套件中 11 个 CWE 上的准确性。Sydr 显示出 95.59% 的总体准确性。我们公开了 Sydr 评估构件，以促进结果的可重复性。

  • Towards Symbolic Pointers Reasoning in Dynamic Symbolic Execution
    报告地点: Ivannikov Memorial Workshop, 下诺夫哥罗德, 俄罗斯, 2021. [论文] [幻灯片]
    作者: Daniil Kuts
    摘要: 动态符号执行是一种广泛使用的自动化软件测试技术，专为执行路径探索和程序错误检测而设计。混合方法最近变得流行起来，其主要目标是让符号执行帮助模糊测试器提高程序覆盖率。符号执行器能反转的分支越多，它对模糊测试器就越有用。程序控制流通常取决于通过从用户输入计算地址索引而获得的内存值。然而，大多数 DSE 工具不支持这种依赖关系，因此它们会错过一些期望的程序分支。我们在动态符号执行工具 Sydr 中实现了对内存读取的符号地址推理。可能的内存访问区域是通过分析内存地址符号表达式，或使用 SMT solver 进行二分搜索来确定的。我们提出了一种增强的线性化技术来对内存访问进行建模。在程序集上比较了不同的内存建模方法。我们的评估表明，符号地址处理允许发现新的符号分支并增加程序覆盖率。

  • QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation
    报告地点: BAR, 圣地亚哥, 加利福尼亚州, 2020. [论文]
    作者: Robin David, Luigi Coniglio, Mariano Ceccato
    摘要: 我们提出了一种利用 DSE 和程序合成成功合成了经过混合布尔算术、数据编码或虚拟化混淆的程序的通用方法。所提出的合成算法是一种由自上而下广度优先搜索引导的离线枚举合成原语。我们展示了它相对于最先进的混淆器的有效性及其可扩展性，因为它超越了其他类似的基于合成的方法。我们还展示了它在复合混淆（多种技术的组合）存在时的有效性。这项正在进行的工作启发了合成在针对某些类型的混淆时的有效性，并为更健壮的算法和简化策略开辟了道路。

  • Sydr: Cutting Edge Dynamic Symbolic Execution
    报告地点: Ivannikov ISP RAS Open Conference, 莫斯科, 俄罗斯, 2020. [论文] [幻灯片] [视频]
    作者: A.Vishnyakov, A.Fedotov, D.Kuts, A.Novikov, D.Parygina, E.Kobrin, V.Logunova, P.Belecky, S.Kurmangaleev
    摘要: 动态符号执行 (DSE) 在计算机安全（模糊测试、漏洞发现、逆向工程等）领域有着巨大的应用。我们提出了几项针对动态符号执行的性能和准确性改进。跳过非符号指令可以使路径谓词的构建速度提高 1.2--3.5 倍。符号引擎在符号执行期间简化公式。路径谓词切片从求解器查询中消除了不相关的合取式。我们将每个跳转表（switch 语句）作为多个分支处理，并描述了多线程程序的符号执行方法。提出的解决方案在 Sydr 工具中得到了实现。Sydr 执行路径谓词中分支的反转。Sydr 结合了 DynamoRIO 动态二进制插桩工具和 Triton 符号引擎。

  • Symbolic Deobfuscation: From Virtualized Code Back to the Original
    报告地点: DIMVA, 巴黎-萨克雷, 法国, 2018. [论文] [幻灯片]
    作者: Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet
    摘要: 在过去十年中，软件保护占据了重要地位，以保护合法软件免受逆向工程或篡改。虚拟化被认为是对抗此类攻击的最佳防御措施之一。我们提出了一种基于符号路径探索、污点分析和重新编译的通用方法，能够从虚拟化代码中恢复出在语义上与原始代码相同且大小相近的反虚拟化代码。我们定义了标准和指标，以评估反混淆结果在正确性和精确度方面的相关性。最后，我们提出了一个开源设置，以针对几种形式的虚拟化评估所提出的方法。

  • Deobfuscation of VM based software protection
    报告地点: SSTIC, 雷恩, 法国, 2017. [法文论文] [英文幻灯片] [法文视频]
    作者: Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet
    摘要: 在本次演讲中，我们描述了一种方法，它包括自动分析基于虚拟机的软件保护，并重新编译一个没有此类保护的新版本二进制文件。这种自动化方法依赖于由污点分析和一些具体化策略引导的符号执行，然后是使用 LLVM 转换的二进制重写。

  • How Triton can help to reverse virtual machine based software protections
    报告地点: CSAW SOS, 纽约市, 纽约, 2016. [幻灯片]
    作者: Jonathan Salwan, Romain Thomas
    摘要: 演讲的第一部分将介绍 Triton 框架，展示其组件并解释它们如何协同工作。然后，第二部分将演示如何使用污点分析、符号执行、SMT 简化和 LLVM-IR 优化来逆向基于虚拟机的保护。

  • Dynamic Binary Analysis and Obfuscated Codes
    报告地点: St'Hack, 波尔多, 法国, 2016. [幻灯片]
    作者: Jonathan Salwan, Romain Thomas
    摘要: 在本次演讲中，我们将讨论 DBA (动态二进制分析) 如何帮助逆向工程师逆向混淆代码。我们将首先介绍一些基本的混淆技术，然后展示如何破解一些东西（使用我们的开源 DBA 框架 - Triton），比如检测不透明谓词、重构 CFG、寻找原始算法、隔离敏感数据等等。然后，我们将以演示和关于未来工作的几句话作为总结。

  • How Triton may help to analyse obfuscated binaries
    发表在: MISC 杂志 82, 2015. [法文文章]
    作者: Jonathan Salwan, Romain Thomas
    摘要: 二进制混淆被用于保护软件的知识产权。存在不同类型的混淆，但大致来说，它通过保留相同的语义将一个二进制结构转换为另一个二进制结构。混淆的目的是确保原始信息被“淹没”在无用的信息中，使逆向工程变得更加困难。在这篇文章中，我们将展示如何使用 Triton 框架分析混淆程序并破坏一些混淆。

  • Triton: A Concolic Execution Framework
    报告地点: SSTIC, 雷恩, 法国, 2015. [法文论文] [详细英文幻灯片]
    作者: Jonathan Salwan, Florent Saudel
    摘要: 本次演讲是关于 Triton 的发布，这是一个基于 Pin 的混合执行框架。它提供了诸如污点引擎、动态符号执行引擎、快照引擎、将 x64 指令转换为 SMT2、用于解决约束的 Z3 接口以及 Python 绑定等组件。基于这些组件，Triton 提供了构建用于漏洞研究或逆向工程辅助工具的可能性。

  • Dynamic Behavior Analysis Using Binary Instrumentation
    报告地点: St'Hack, 波尔多, 法国, 2015. [幻灯片]
    作者: Jonathan Salwan
    摘要: 本次演讲可以被视为我们在 SecurityDay 演讲的第二部分。在上一部分中，我们讨论了如何使用 DSE (动态符号执行) 方法覆盖内存中的目标函数。覆盖一个函数（或其状态）并不意味着找到所有漏洞，有些漏洞不会导致程序崩溃。这就是为什么我们必须实施特定的分析来发现特定的错误。这些分析基于二进制插桩和程序的运行时行为分析。在本次演讲中，我们将看到如何发现以下类型的错误：差一错误、栈 / 堆溢出、释放后使用、格式化字符串和 {write, read}-what-where。

  • Covering a function using a Dynamic Symbolic Execution approach
    报告地点: Security Day, 里尔, 法国, 2015. [幻灯片]
    作者: Jonathan Salwan
    摘要: 本次演讲是关于二进制分析和插桩的。我们将看到如何定位特定函数，在函数执行前对上下文内存/寄存器进行快照，将插桩转化为中间表示，基于此 IR 应用污点分析，为动态符号执行 (DSE) 构建/保留公式，生成具体值以穿过特定路径，恢复上下文内存/寄存器并生成另一个具体值以穿过另一条路径，然后重复此操作，直到目标函数被完全覆盖。
## 引用 Triton ``` @inproceedings{SSTIC2015-Saudel-Salwan, author = {Saudel, Florent and Salwan, Jonathan}, title = {Triton: A Dynamic Symbolic Execution Framework}, booktitle = {Symposium sur la s{\'{e}}curit{\'{e}} des technologies de l'information et des communications}, series = {SSTIC}, pages = {31--54}, address = {Rennes, France}, month = jun, year = {2015}, } ```
标签：AArch64, ARM32, Bash脚本, Bitwuzla, C++, CTF工具, DAST, DNS解析, LLVM, meg, odt, Python, RISC-V, SMT求解器, SMT简化, x86, Z3, 中间表示, 二进制插桩, 云资产清单, 代码仿真, 信息安全, 动态二进制分析, 动态分析框架, 开源项目, 恶意软件分析, 抽象语法树, 指令集架构, 数据擦除, 无后门, 漏洞搜索, 程序分析工具, 符号执行, 编译器, 自动化逆向, 表达式综合, 软件验证, 逆向工具, 逆向工程