Triton

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},
}