Triton是动态二进制分析库。它提供了内部组件,使您能够构建程序分析工具,自动化反向工程,执行软件验证或仿真代码。
- 动态符号执行
- 动态污染分析
- X86 , X86-64 , ARM32 , AARCH64和RISC-V 32/64 ISA语义的AST表示
- 表达合成
- SMT简化通过
- 提起到LLVM以及Z3和后背
- SMT求解器接口到Z3和Bitwuzla
- C ++和Python API
由于Triton是一个兼职项目,请不要怪我们,如果它不完全可靠。开放问题或拉动请求总是比拖钓=)更好。但是,您可以在Twitter @QB_Triton上关注开发。
快速开始
- 安装
- Python API
- C ++ API
- python示例
- 他们已经使用了特里顿
入门
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' 安装
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。如果您想享受特里顿的全部力量,则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/[email protected]/3.10.8/Frameworks/Python.framework/Versions/3.10/lib/libpython3.10.dylib
-DPYTHON_INCLUDE_DIRS=/opt/homebrew/opt/[email protected]/Frameworks/Python.framework/Versions/3.10/include/python3.10/
..您可以从此片段中获取此信息:
from sysconfig import get_paths
info = get_paths ()
print ( info )
视窗
您可以使用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文物。请注意,如果您使用Appveyor的工件,则可能必须为Visual Studio 2012安装Visual C ++重新分布软件包。
从VCPKG安装
Microsoft团队成员和社区贡献者保持了VCPKG的Triton港口的最新状态。 VCPKG的URL为: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存储库上创建问题或拉出请求。
贡献者
- Alberto Garcia Illera -Cruise Automation
- Alexey Vishnyakov -ISP RAS
- 黑色二进制-N/A
- 克里斯蒂安·海特曼(Christian Heitman) - 夸克斯拉布(Quarkslab)
- Daniil Kuts -ISP RAS
- 杰西·坎波斯(Jessy Campos)-N/A
- Matteo F. -N/A
- Pierrick Brunet -Quarkslab
- Pixelrick -n/a
- 罗曼·托马斯(Romain Thomas)-Quarkslab
- 还有更多
他们已经使用了特里顿
工具
- EXROP:自动链链生成。
- PIMP:基于Triton的R2插件,用于共同执行和总控制。
- Ponce:IDA 2016插件竞赛冠军!象征性执行只有一键!
- QSYNESIS:灰盒合成器,适用于装配说明的去量。
- Tritondse:具有加载和勘探功能的基于Triton的DSE库。
- Titan:Titan是使用Triton的VMPROTECT DEVIRTUALIZER。
论文和会议
- SYDR-FUZZ:用于安全开发生命周期的连续混合模糊和动态分析
在:2022年莫斯科,伊万尼科夫ISP RAS公开会议上谈话。[纸] [幻灯片]
作者:Vishnyakov A.,Kuts D.,Logunova V.,Parygina D.,Kobrin E.,Savidov G.,Fedotov A.
摘要:如今,用于连续测试的自动化动态分析框架需求很高,以确保软件安全并满足安全开发生命周期(SDL)要求。尖端混合模糊技术的安全错误狩猎效率优于广泛使用的覆盖范围引导的模糊。我们提出了一条增强的动态分析管道,以利用基于混合模糊的自动化错误检测的生产率。我们在连续模糊的工具集Sydr-Fuzz中实现了拟议的管道,该管道由混合模糊编排器提供动力,将我们的DSE工具SYDR与libfuzzer和AFL ++集成在一起。 Sydr-Fuzz还结合了安全性谓词检查器,CALRS TRIAGING TOAL CASR以及用于最小化和覆盖范围收集的实用程序。我们的混合模糊器对替代性最先进的解决方案的基准测试表明,它优于覆盖范围引导的模糊器,同时与先进的混合动力爆炸剂保持在相同的水平上。此外,我们通过在OSS-Sydr-Fuzz项目中发现85个新的现实世界软件缺陷来批准我们的方法的相关性。最后,我们向社区开放CASR源代码,以促进对现有崩溃的检查。
- 强烈的乐观解决,以动态符号执行
在:2022年喀山伊万尼科夫纪念研讨会上谈话。[纸] [幻灯片]
作者:Parygina D.,Vishnyakov A.,Fedotov A.
摘要:动态符号执行(DSE)是自动化程序测试和错误检测的有效方法。在混合模糊过程中,复杂的分支探索增加了代码覆盖范围。 DSE工具沿着某些执行路径颠倒分支,并帮助Fuzzer检查以前不可用的程序零件。 DSE经常面临过度和欠缺问题。第一个导致重大分析并发症,而第二个则导致不准确的符号执行。我们提出了强大的乐观解决方法,以消除目标分支反演的无关路径谓词约束。我们消除了这种符号约束,即目标分支不能控制。此外,我们分别处理具有嵌套控制传输指令的符号分支,这些分支将控制传递到父分支范围,例如返回,goto,break等。我们在动态符号执行工具sydr中实现了所提出的方法。我们评估强大的乐观策略,即仅包含最后一个约束否定及其组合的乐观策略。结果表明,策略组合有助于增加代码覆盖范围或每分钟正确倒立分支的平均数量。与其他配置相比,将这两种策略一起应用在一起是最佳的。
- Greybox程序综合:一种攻击数据流混淆的新方法
在内华达州拉斯维加斯,黑人美国聊天:2021年。[幻灯片]
作者:罗宾·戴维(Robin David)
摘要:此演讲介绍了用于去滥用的程序合成的最新进展。它旨在通过展示如何对混淆作用来揭开该分析技术的神秘面纱。尤其是为本演讲发布的实现qsynsis,显示了一个完整的端到端工作流程,以重新填充(DeObfuscated)指令重新组装回二进制中,以解除汇编的汇编指令。
- 从源代码到崩溃测试案例,通过软件测试自动化
在:法国雷恩斯,C&Esar,2021年。[纸] [幻灯片]
作者:罗宾·戴维(Robin David),乔纳森·萨尔万(Jonathan Salwan),贾斯汀·布鲁克斯(Justin Bourroux)
摘要:本文提出了一种方法,将软件测试过程从源代码到编译程序的动态测试进行自动化。更具体地说,从静态分析报告中指示源线上的警报,它使测试能够动态和机会性地检查它们是否可以触发崩溃。结果是测试语料库允许涵盖警报并触发它们,如果它们恰好是真正的阳性。本文讨论了用于跟踪编译二进制中的警报,测试引擎选择过程中所采用的方法,以及在用于嵌入式和物联网系统的TCP/IP堆栈实现上获得的结果。
- 符号安全谓词:狩猎计划弱点
在:2021年莫斯科,伊万尼科夫ISP RAS公开会议上谈话。[纸] [幻灯片]
作者:A.Vishnyakov,V.Logunova,E.Kobrin,D.Kuts,D.Parygina,A.Fedotov
摘要:动态符号执行(DSE)是在混合模糊和自动错误检测过程中进行路径探索的强大方法。我们建议安全性谓词有效检测未定义的行为和内存访问违规错误。最初,我们在没有触发任何错误的路径上象征性地执行程序(混合模糊可能会探索这些路径)。然后,我们构建一个符号安全性谓词以验证某些错误条件。因此,我们可能会将程序数据流更改为“零指针”取消,除以零,距离访问或整数溢出弱点。与静态分析不同,动态符号执行不仅报告错误,而且还会生成新的输入数据来复制它们。此外,我们为常见的C ++标准库功能引入功能语义建模。我们旨在用单个符号公式对函数内部的控制流进行建模。这有助于错误检测,加快路径探索并克服路径谓词中的过度构造。我们在动态符号执行工具SYDR中实现了所提出的技术。因此,我们利用SYDR的强大方法,例如消除无关约束的路径谓词切片。我们提出朱丽叶动态,以测量动态错误检测工具的精度。测试系统还验证生成输入的触发消毒剂。我们从朱丽叶测试套件中评估了11个CWES的SYDR准确性。 SYDR的总体准确性为95.59%。我们使SYDR评估工件公开可用,以促进结果可重复性。
- 在动态符号执行中迈向符号指针推理
在:俄罗斯尼兹·诺夫哥罗德(Nizhny Novgorod),2021年。[纸] [slide]
作者:Daniil Kuts
摘要:动态符号执行是一种用于自动化软件测试的广泛使用的技术,旨在执行路径探索和程序错误检测。最近,当象征性执行的主要目标是帮助Fuzzer提高程序覆盖范围时,混合动力的方法已变得广泛。符号执行人可以反转的分支越多,对fuzzer的有用越有用。程序控制流通常取决于内存值,这是通过从用户输入中计算地址索引获得的。但是,大多数DSE工具不支持此类依赖项,因此他们错过了一些所需的程序分支。我们在动态符号执行工具SYDR中实现了内存读取的符号地址。可能的内存访问区域是通过分析内存地址符号表达式来确定的,或使用SMT溶剂搜索二进制搜索。我们提出了一种增强的线性化技术来建模内存访问。在程序集上比较了不同的内存建模方法。我们的评估表明,符号地址处理可以发现新的符号分支并增加程序覆盖范围。
- QSYNTH:基于程序综合的二进制代码DEOBFUSCATION的方法
在:2020年,加利福尼亚州圣地亚哥的BAR上交谈。[纸]
作者:罗宾·戴维(Robin David),路易吉·科尼格里奥(Luigi Coniglio),马里亚诺·塞卡托
摘要:我们提出了一种通用方法,利用DSE和程序合成,以成功地合成与混合树状算术,数据编码或虚拟化混淆的程序。提出的综合算法是列举综合原始呼吸搜索以引导的一个离线综合原始搜索。我们显示了它针对最先进的混淆器的有效性及其可扩展性,因为它基于合成,取代了其他类似的方法。我们还显示了其在复合混淆的存在(各种技术的组合)中的有效性。这项正在进行的工作启发了综合目标的有效性,以针对某些类型的混淆,并为更强大的算法和简化策略打开了道路。
- SYDR:尖端动态符号执行
在:2020年莫斯科,伊万尼科夫ISP RAS公开会议上谈话。[纸] [幻灯片] [视频]
作者: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符号发动机结合在一起。
- 象征性去量:从虚拟化代码回到原始代码
在:法国巴黎 - 萨克莱,2018年DIMVA上交谈。[纸] [幻灯片]
作者:Jonathan Salwan,SébastienBardin,Marie-Laure Potet
摘要:在过去的十年中,软件保护是一个重要的位置,以保护合法软件免受反向工程或篡改。虚拟化被认为是针对此类攻击的最佳防御能力之一。我们提出了一种基于符号路径探索,污点和重新编译的通用方法,可以从虚拟化代码中恢复与原始大小相同并接近大小相同的Devirtalized代码。我们定义标准和指标,以根据正确性和精确度来评估Deobfuscusted结果的相关性。最后,我们提出了一个开源设置,允许评估针对几种虚拟化的建议方法。
- 基于VM的软件保护的去掺杂
在:法国雷恩斯的SSTIC,2017年。[法国论文] [英语幻灯片] [法语视频]
作者:Jonathan Salwan,SébastienBardin,Marie-Laure Potet
摘要:在本演示文稿中,我们描述了一种方法,该方法包括自动分析基于虚拟机的软件保护措施,并在没有这种保护的情况下重新编译新版本的二进制版本。这种自动化方法依赖于通过污点分析和某些具体政策的符号执行指南,然后使用LLVM过渡的二进制重写。
- Triton如何帮助逆转基于虚拟机的软件保护
在:2016年纽约市纽约市CSAW SOS上交谈。[幻灯片]
作者:乔纳森·萨尔万(Jonathan Salwan),罗曼·托马斯(Romain Thomas)
摘要:演讲的第一部分将成为Triton框架的介绍,以揭示其组成部分并解释它们如何共同工作。然后,第二部分将包括有关如何使用污点分析,符号执行,SMT简化和LLVM-IR优化逆转虚拟机的保护的演示。
- 动态二进制分析和混淆代码
2016年,法国波尔多的St'Hack,St'Hack 。[幻灯片]
作者:乔纳森·萨尔万(Jonathan Salwan),罗曼·托马斯(Romain Thomas)
摘要:在本演讲中,我们将讨论DBA(动态二进制分析)如何帮助反向工程师逆转混淆的代码。我们将首先介绍一些基本的混淆技术,然后揭示如何打破某些东西(使用我们的开源DBA框架 - Triton),例如检测不透明的谓词,重建CFG,找到原始算法,找到原始的算法,孤立的敏感数据等等...然后,我们将与我们的演示和几个有关未来的言论结束。
- Triton如何帮助分析混淆的二进制文件
出版物:MISC杂志82,2015。[法国文章]
作者:乔纳森·萨尔万(Jonathan Salwan),罗曼·托马斯(Romain Thomas)
摘要:二进制混淆用于保护软件的知识产权。存在不同种类的混淆,但粗略地,它通过保留相同的语义将二进制结构转化为另一种二元结构。混淆的目的是确保原始信息在无用的信息中被“淹没”,这将使反向工程变得更加困难。在本文中,我们将展示如何使用Triton框架分析一个无局部的程序并打破一些混淆。
- Triton:一个共同的执行框架
在:法国雷恩斯,雷恩斯,2015年。[法国论文] [详细的英语幻灯片]
作者:乔纳森·萨尔万(Jonathan Salwan),佛罗伦萨·索德尔
摘要:此谈话是关于Triton的发布,Triton是基于PIN的一致执行框架。它提供了诸如污点引擎,动态符号执行引擎,快照引擎的组件,将x64指令转换为SMT2,Z3接口,以求解约束和Python绑定。基于这些组件,Triton提供了为脆弱性研究或反向工程辅助构建工具的可能性。
- 使用二元仪器的动态行为分析
2015年,法国波尔多的St'Hack,St'Hack 。[幻灯片]
作者:乔纳森·萨尔万
摘要:这次演讲可以像我们在SecurityDay上谈话的第2部分一样将其视为。在上一部分中,我们讨论了如何使用DSE(动态符号执行)方法在内存中覆盖目标功能。覆盖功能(或其状态)并不意味着找到所有漏洞,某些漏洞不会崩溃该程序。这就是为什么我们必须实施特定分析才能找到特定的错误。这些分析基于二进制仪器和程序的运行时行为分析。在本演讲中,我们将看到如何找到以下类型的错误:隔离,堆栈 /堆溢出,无效,格式字符串和{write,read} -what-what-where-where。
- 使用动态符号执行方法覆盖功能
在:法国里尔的安全日,2015年。[幻灯片]
作者:乔纳森·萨尔万
摘要:此谈话是关于二进制分析和仪器的。 We will see how it's possible to target a specific function, snapshot the context memory/registers before the function, translate the instrumentation into an intermediate representation,apply a taint analysis based on this IR, build/keep formulas for a Dynamic Symbolic Execution (DSE), generate a concrete value to go through a specific path, restore the context memory/register and generate another concrete value to go through another path then repeat this operation until the target function is covered.
引用特里顿
@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},
}