TritonのダウンロードTritonソースコードのダウンロード

Triton

その他のカテゴリー

Version 0.9

ダウンロード

Tritonは動的なバイナリ分析ライブラリです。プログラム分析ツールを構築したり、リバースエンジニアリングを自動化したり、ソフトウェア検証を実行したり、コードをエミュレートしたりできる内部コンポーネントを提供します。

動的なシンボリック実行
動的汚染分析
X86 、 X86-64 、 ARM32 、 AARCH64およびRISC-V 32/64 ISAセマンティックのAST表現
式合成
SMTの単純化が渡されます
LLVMとZ3およびバックに持ち上げる
Z3およびBitwuzlaへのSMTソルバーインターフェイス
C ++およびPython API

トリトンは一種のパートタイムプロジェクトであるため、完全に信頼できない場合でも、私たちを責めないでください。オープンな問題やプル要求は、トローリングよりも常に優れています=）。ただし、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'

インストール

トリトンは次の依存関係に依存しています。

 * 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 ..

MacOSM1注：

次のような編集エラーが発生した場合

 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 )

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のアーティファクトをご覧ください。 Appveyorのアーティファクトを使用する場合、Visual Studio 2012のVisual C ++再分配可能なパッケージをインストールする必要があることに注意してください。

VCPKGからのインストール

VCPKGのTritonポートは、Microsoftチームメンバーとコミュニティの貢献者によって最新の状態に保たれています。 VCPKGのURLはhttps://github.com/microsoft/vcpkgです。 VCPKG Dependency Managerを使用して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リポジトリで問題を作成するか、リクエストをプルしてください。

貢献者

アルベルトガルシアイレラ- クルーズオートメーション
Alexey Vishnyakov -ISP Ras
ブラックバイナリ-n/a
クリスチャンハイトマン- Quarkslab
Daniil Kuts -ISP ras
ジェシー・カンポス-N/A。
Matteo F. -n/a
Pierrick Brunet -Quarkslab
Pixelrick -n/a
ロマン・トーマス- quarkslab
そしてもっと

彼らはすでにトリトンを使用しています

ツール

Exrop：自動ロプチャイン生成。
PIMP：コンコリックの実行と総制御のためのTritonベースのR2プラグイン。
ポンセ：IDA 2016プラグインコンテストの勝者！シンボリック実行は、1つのクリックだけです！
Qsynthesis：アセンブリの指示の脱骨筋装置のためのGreyboxシンセサイザー。
Tritondse：ロードおよび探索機能を備えたTritonベースのDSEライブラリ。
Titan：Titanは、Tritonを使用したVMProtect Devirtualizerです。

論文と会議

SYDRファズ：セキュリティ開発ライフサイクルのための連続ハイブリッドファジングと動的分析
トーク：Ivannikov ISP RAS Open Conference、モスクワ、ロシア、2022。[紙] [スライド]
著者：Vishnyakov A.、Kuts D.、Logunova V.、Parygina D.、Kobrin E.、Savidov G.、Fedotov A.
要約：最近では、継続的なテスト用の自動化された動的分析フレームワークは、ソフトウェアの安全性を確保し、セキュリティ開発ライフサイクル（SDL）要件を満たすために高い需要があります。最先端のハイブリッドファジングテクニックのセキュリティバグハンティング効率は、カバレッジ誘導ファジングを広く利用していることを上回ります。ハイブリッドファジングに基づいた自動バグ検出の生産性を活用するために、強化された動的分析パイプラインを提案します。提案されたパイプラインは、ハイブリッドファジングオーケストレーターによって駆動される連続ファジングツールセットSYDRファズに実装し、DSEツールSYDRをLibfuzzerおよびAFL ++と統合します。 SYDRファズには、セキュリティ述語チェッカー、クラッシュトリアングツールCASR、およびコーパスの最小化とカバレッジの収集のためのユーティリティも組み込まれています。代替の最先端のソリューションに対するハイブリッドファッツァーのベンチマークは、高度なハイブリッドファッツァーと同じレベルにとどまりながら、カバレッジ誘導ファッツァーに対するその優位性を示しています。さらに、OSS-SYDR-Fuzzプロジェクト内で85の新しい現実世界のソフトウェアの欠陥を発見することにより、アプローチの関連性を承認します。最後に、CASRソースコードをコミュニティに開き、既存のクラッシュの調査を容易にします。

動的な象徴的な実行のための強力な楽観的解決
トーク：Ivannikov Memorial Workshop、カザン、ロシア、2022。[紙] [スライド]
著者：Parygina D.、Vishnyakov A.、Fedotov A.
要約：動的シンボリック実行（DSE）は、自動化されたプログラムテストとバグ検出のための効果的な方法です。ハイブリッドファジング中の複雑な分岐探査によるコードカバレッジが増加しています。 DSEツールは、いくつかの実行パスに沿ってブランチを反転させ、Fuzzerが以前に利用できなかったプログラムパーツを調べるのを支援します。 DSEは、しばしば過剰な制約の問題に直面しています。最初のものは重要な分析の合併症につながり、2番目のものは不正確な象徴的な実行を引き起こします。ターゲットブランチの反転の無関係な経路述語制約を排除する強力な楽観的解決方法を提案します。ターゲットブランチが制御されないような象徴的な制約を排除します。さらに、親ブランチの範囲を超えて制御を渡す制御転送命令をネストしたシンボリックブランチなどを個別に処理します。強力な楽観的戦略、最後の制約否定のみを含む楽観的戦略、およびそれらの組み合わせを評価します。結果は、戦略の組み合わせが、コードカバレッジまたは1分あたり正しく反転した枝の平均数のいずれかを増やすのに役立つことを示しています。他の構成とは対照的に、両方の戦略を一緒に適用することが最適です。

Greyboxプログラムの統合：データフローの難読化を攻撃するための新しいアプローチ
トーク：ブラックハットUSA、ラスベガス、ネバダ州、2021年。[スライド]
著者：ロビン・デイビッド
要約：この講演では、脱骨筋が適用されるプログラム統合の最新の進歩を示しています。これは、難読化にどのように実行できるかを示すことにより、この分析手法を分析することを目的としています。特に、この講演のためにリリースされた実装QSynthesisは、バイナリで再構築された最適化（脱状）命令に戻ってアセンブリ命令を除去するための完全なエンドツーエンドのワークフローを示しています。

ソースコードからクラッシュテストケースまで、ソフトウェアテストの自動化を通じて
トーク：C＆ESAR、レンヌ、フランス、2021。[紙] [スライド]
著者：ロビン・デイヴィッド、ジョナサン・サルワン、ジャスティン・ブルルー
要約：このペーパーでは、ソースコードからコンパイルされたプログラムの動的テストまで、ソフトウェアテストプロセスを自動化するアプローチを示します。より具体的には、ソースラインのアラートを示す静的分析レポートから、テストがこれらのラインを動的にカバーすることを可能にし、クラッシュをトリガーできるかどうかを日和見的にチェックします。その結果、アラートをカバーし、それらがたまたま真のポジティブである場合にそれらをトリガーすることができるテストコーパスができます。このペーパーでは、コンパイルされたバイナリでアラートを追跡するために採用された方法論、テストエンジンの選択プロセス、および組み込みおよびIoTシステムのTCP/IPスタック実装で得られた結果について説明します。

シンボリックセキュリティの述語：ハントプログラムの弱点
トーク：Ivannikov ISP RAS Open Conference、モスクワ、ロシア、2021。[Paper] [Slide]
著者：A.Vishnyakov、V.Logunova、E.Kobrin、D.Kuts、D.Parygina、A.Fedotov
要約：動的シンボリック実行（DSE）は、ハイブリッドファジングおよび自動バグ検出中のパス探索の強力な方法です。未定義の動作とメモリアクセス違反エラーを効果的に検出するためのセキュリティの前兆を提案します。最初に、エラーをトリガーしないパスでプログラムを象徴的に実行します（ハイブリッドファジングはこれらのパスを探索する場合があります）。次に、いくつかのエラー条件を確認するために、シンボリックセキュリティ述語を構築します。したがって、プログラムのデータフローを変更して、ゼロによる分割、バウンドアウトアクセス、または整数のオーバーフローの弱点を伴う場合があります。静的分析とは異なり、動的なシンボリック実行は、エラーを報告するだけでなく、それらを再現するための新しい入力データを生成します。さらに、一般的なC/C ++標準ライブラリ関数の関数セマンティクスモデリングを導入します。単一のシンボリック式で関数内の制御フローをモデル化することを目指しています。これにより、バグの検出が役立ち、パスの探索をスピードアップし、パス述語の過剰制約を克服します。ダイナミックシンボリック実行ツールSYDRに提案された手法を実装します。したがって、無関係な制約を排除するPATH述語スライスなど、SYDRから強力な方法を利用します。 Juliet Dynamicを提示して、動的なバグ検出ツールの精度を測定します。テストシステムは、入力が生成されたトリガー消毒剤を生成することも検証します。 Juliet Test Suiteの11 CWEのSYDR精度を評価します。 SYDRは、全体的な精度95.59％を示しています。 SYDR評価アーティファクトを公開して、結果の再現性を促進します。

動的な象徴的な実行における象徴的なポインターの推論に向けて
トーク：Ivannikov Memorial Workshop、Nizhny Novgorod、Russia、2021。[Paper] [Slide]
著者：Daniil Kuts
要約：動的シンボリック実行は、自動化されたソフトウェアテストのために広く使用されている手法であり、実行パスの探索とプログラムエラーの検出用に設計されています。象徴的な実行の主な目標が、ファザーがプログラムのカバレッジを増やすのに役立つことが、最近、ハイブリッドアプローチが広く普及しています。より多くの支店のシンボリックエグゼキューターが反転できるほど、ファッツァーにとってより有用になります。プログラム制御フローは、多くの場合、メモリ値に依存します。これは、ユーザー入力からアドレスインデックスを計算することによって取得されます。ただし、ほとんどのDSEツールはそのような依存関係をサポートしていないため、望ましいプログラムブランチを見逃しています。動的なシンボリック実行ツールsydrにメモリ読み取りに記載の推論を実装します。考えられるメモリアクセス領域は、メモリアドレスのシンボリック式を分析するか、SMT-Solverを使用したバイナリ検索によって決定されます。メモリアクセスをモデル化するための強化された線形化手法を提案します。さまざまなメモリモデリング方法が、プログラムのセットで比較されます。私たちの評価は、シンボリックアドレスの取り扱いにより、新しいシンボリックブランチを発見し、プログラムのカバレッジを増やすことができることを示しています。

Qsynth：バイナリコードの脱骨のためのプログラム統合ベースのアプローチ
トーク：バー、カリフォルニア州サンディエゴ、2020年。[紙]
著者：ロビン・デイヴィッド、ルイージ・コニリオ、マリアーノ・セッカト
要約： DSEとプログラムの両方の合成を活用する一般的なアプローチを提示して、混合ブール - アリスメティック、データエンコード、または仮想化で難読化されたプログラムを正常に合成します。提案されている合成アルゴリズムは、トップダウンブレスファースト検索によって誘導されたオフライン列挙合成プリミティブです。合成に基づいて他の同様のアプローチに取って代わるため、最先端の難読因子に対する有効性とそのスケーラビリティを示しています。また、複合難読化（さまざまな技術の組み合わせ）の存在においてその有効性を示します。この継続的な作業は、特定の種類の難読化をターゲットにして合成の有効性を啓発し、より堅牢なアルゴリズムと簡素化戦略への道を開きます。

SYDR：最先端の動的なシンボリック実行
トーク：Ivannikov ISP RAS Open Conference、モスクワ、ロシア、2020。[Paper] [Slide] [Video]
著者：A.Vishnyakov、A.Fedotov、D.Kuts、A.Novikov、D.Parygina、E.Kobrin、V.Logunova、P.Belecky、S.Kurmangaleeev
要約：動的シンボリック実行（DSE）には、コンピューターセキュリティ（ファジング、脆弱性の発見、リバースエンジニアリングなど）に膨大な量のアプリケーションがあります。動的なシンボリック実行のためのいくつかのパフォーマンスと精度の改善を提案します。非共同指示をスキップすることで、パスの述語を1.2〜3.5倍速く構築できます。シンボリックエンジンは、シンボリック実行中に式を簡素化します。パス述語スライシングは、ソルバークエリから無関係な接続詞を排除します。各ジャンプテーブル（スイッチステートメント）を複数のブランチとして処理し、マルチスレッドプログラムの象徴的な実行方法を説明します。提案されたソリューションは、SYDRツールに実装されました。 SYDRは、PATH PRESTICEで枝の反転を実行します。 SYDRは、Dynamorio Dynamic Binary Instrumentation ToolとTriton Symbolic Engineを組み合わせています。

Symbolic Deobfuscation：仮想化コードからオリジナルに戻ります
トーク：Dimva、Paris-Saclay、France、2018。[紙] [スライド]
著者：Jonathan Salwan、SébastienBardin、Marie-Laure Potet
要約：ソフトウェア保護は、リバースエンジニアリングまたは改ざんから合法的なソフトウェアを保護するために、過去10年間に重要な位置を占めてきました。仮想化は、そのような攻撃に対する最高の防御の1つと考えられています。象徴的な経路探索、汚染、および再コンパイルに基づいた一般的なアプローチを提示し、仮想化コードから、元のコードと同じように同一の偏見コードとサイズが近いことを回復できます。正確さと精度の観点から、脱骨筋摂取結果の関連性を評価するための基準とメトリックを定義します。最後に、いくつかの形式の仮想化に対する提案されたアプローチを評価できるオープンソースのセットアップを提案します。

VMベースのソフトウェア保護の脱ブスケーション
トーク：SSTIC、レンヌ、フランス、2017年。[フレンチペーパー] [英語スライド] [フレンチビデオ]
著者：Jonathan Salwan、SébastienBardin、Marie-Laure Potet
要約：このプレゼンテーションでは、仮想マシンベースのソフトウェア保護を自動的に分析し、そのような保護なしに新しいバージョンのバイナリを再コンパイルするためのアプローチについて説明します。この自動化されたアプローチは、汚染分析といくつかの具体化ポリシーによるシンボリック実行ガイド、次にLLVM遷移を使用したバイナリ書き換えに依存しています。

Tritonが仮想マシンベースのソフトウェア保護を逆転させるのにどのように役立つか
トーク：CSAW SOS、NYC、ニューヨーク、2016年。[スライド]
著者：ジョナサン・サルワン、ロマン・トーマス
要約：講演の最初の部分は、コンポーネントを公開し、それらがどのように連携するかを説明するためのTritonフレームワークの紹介となるでしょう。次に、2番目の部分には、汚染分析、シンボリック実行、SMT単純化、LLVM-IRの最適化を使用して、仮想マシンベースの保護をどのように逆転させることができるかについてのデモが含まれます。

動的バイナリ分析と難読化コード
トーク：St'hack、Bordeaux、France、2016。[スライド]
著者：ジョナサン・サルワン、ロマン・トーマス
要約：このプレゼンテーションでは、DBA（動的バイナリ分析）がリバースエンジニアが難読化コードを逆転させる方法について説明します。最初にいくつかの基本的な難読化技術を導入し、不透明な述語を検出し、CFGを再構築し、元のアルゴリズムを見つけ、賢明なデータを見つけ、その他多くのものなど、いくつかのもの（オープンソースDBAフレームワーク - トリトンを使用して）をどのように壊すことができるかを公開します。

Tritonが難読化されたバイナリの分析にどのように役立つか
出版物：Misc Magazine 82、2015。[フランスの記事]
著者：ジョナサン・サルワン、ロマン・トーマス
要約：バイナリの難読化は、ソフトウェアの知的財産を保護するために使用されます。さまざまな種類の難読化が存在しますが、大まかに、同じセマンティックを保存することにより、バイナリ構造を別のバイナリ構造に変換します。難読化の目的は、元の情報が、リバースエンジニアリングをより困難にする役に立たない情報で「drれ」ていることを保証することです。この記事では、繁殖したプログラムを分析し、Tritonフレームワークを使用していくつかの難読化を破る方法を示します。

トリトン：コンコリック実行フレームワーク
トーク：SSTIC、レンヌ、フランス、2015年。[フランスの論文] [詳細な英語のスライド]
著者：ジョナサン・サルワン、フローレント・サウデル
要約：この講演は、PINに基づくコンコリック実行フレームワークであるTritonのリリースに関するものです。 Taintエンジン、動的なシンボリック実行エンジン、スナップショットエンジン、X64命令のSMT2への翻訳、Z3インターフェイス、制約とPythonバインディングを解決するなどのコンポーネントを提供します。これらのコンポーネントに基づいて、Tritonは、脆弱性の研究またはリバースエンジニアリング支援のためのツールを構築する可能性を提供します。

バイナリ計装を使用した動的な動作分析
トーク：St'hack、Bordeaux、France、2015。[スライド]
著者：ジョナサン・サルワン
要約：この講演は、SecurityDayでの講演のパート2のように考えることができます。前のパートでは、DSE（動的シンボリック実行）アプローチを使用して、メモリ内のターゲット関数をどのようにカバーできるかについて話しました。関数（またはその状態）をカバーすることは、すべての脆弱性を見つけることを意味するものではなく、一部の脆弱性はプログラムをクラッシュさせません。そのため、特定のバグを見つけるために特定の分析を実装する必要があります。これらの分析は、プログラムのバイナリインストルメンテーションとランタイム行動分析に基づいています。この講演では、オフワン、スタック /ヒープオーバーフロー、無用、フォーマット文字列、{write、read} - what-whereなど、次のようなバグを見つけることができる方法を確認します。

動的なシンボリック実行アプローチを使用して関数をカバーします
トーク：セキュリティデイ、リール、フランス、2015年。[スライド]
著者：ジョナサン・サルワン
要約：この講演は、バイナリ分析と計装に関するものです。特定の関数をターゲットにし、関数の前にコンテキストメモリ/レジスタをスナップショットし、インストゥルメンテーションを中間表現に変換し、このIRに基づいて汚染分析を適用し、動的なシンボリック実行（DSE）のためにフォーミュラを構築/保持する方法を確認し、特定のパスを通過するために具体的な価値を回復するためにコンクリート値を生成します。

トリトンを引用します

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

拡大する

追加情報