ホーム>JSPソースコード>その他のカテゴリー
ダウンロード

domtreSat

Domtresat（DTS）は、ソースコードを入力として取得し、作成されたドミネーターツリー構造から収集されたパスのパス満足度レポートを自動的に生成する静的解析システムです。最小限の人間の介入で最大のコードカバレッジを取得します。 domtreSatは、ユーザー制御変数のドミネーターツリーを作成し、その値に配置された制約と操作を出力して、満足度ソルバーに供給されます。これにより、脆弱性発見のためのプログラムに関心のある潜在的なポイントが生成されます。

主な動機

このツールの主な使用は、プログラム内のターゲットへの制御可能な入力の到達可能性と、そこに到達するために必要なこの入力を決定することです。ターゲットは、ツリーの最も支配的なパスに自動的に設定されます。これにより、監査人は、以下の図のような一連のチェックを使用して、脆弱なコードへのパスを特定するのに役立ちます。このようなプログラムでは、使用法を解析したいのは、最も支配的なパスです。 

     INPUT
        
       CHECK
       /   |
     FAIL  CHECK
          /   |
        FAIL  CHECK
             /   |
           FAIL  VULNERABILITY

分析理論

ドミネーターの木

このツールは、最初に最も支配的なパスを分析するデフォルトです。これらのパスは、最も機能する変数を持つパスとして説明できます。これは、ニーズに基づいて変更でき、変更されたライブラリを生成するために迅速な再コンパイルスクリプトが用意されています。

使用決定チェーン

Use-Define Chains（Use-DEF）は、変数の使用で構成されるデータ構造であり、その変数のすべての定義は、他の介入定義なしでその使用に到達できるすべての定義です。

このツールは、作成されたドミネーターツリーを介して見られる最も支配的なパスからこれらのデータ構造を引くことに依存しています。基本的な考え方は、ターゲットを絞った使用、つまり変数を使用して脆弱性を獲得または引き起こすことを考えると、この変数を（再）定義のすべてを介して追跡し、ユーザー制御可能である場合はaを決定できるということです。

建物

DomtreSatはLLVM 3.7.1でテストされています。

  1. 依存関係をインストールします
  • OS X： brew install z3
  • Linux/Windows：Z3Prover/Z3の指示に従ってください
  1. $./quick_setup.shテストをビルドして実行します
  2. $./partial_build.sh分析方法を変更した後に増分再構築を実行する

使用法

このセクションでは、テストを実行してSATソルバーにフィードする方法について説明します。

基本ケーステスト

最も支配されたパスを介した変数（それらの使用-DEFチェーン）のトレース定義のテスト

$./test_base_case.sh

ターゲットパスを満た​​すために入力を生成するためにZ3でこのテストを実行するには：

$./complete_test_base_case.sh

追加演算子テスト

最も支配されたパスを介した変数（それらの使用-DEFチェーン）のトレース定義のテスト。使用-DEFチェーンには、追加操作が変数に適用された後に再定義が含まれるようになりました。

$./test_addition.sh

ターゲットパスを満た​​すために入力を生成するためにパスとZ3を実行するには：

$./complete_test_addition.sh

減算演算子テスト

最も支配されたパスを介した変数（それらの使用-DEFチェーン）のトレース定義のテスト。使用-DEFチェーンには、減算操作が変数に適用された後に再定義が含まれるようになりました。

$./test_subtraction.sh

ターゲットパスを満た​​すために入力を生成するためにパスとZ3を実行するには：

$./complete_test_subtraction.sh

XORオペレーターテスト

最も支配されたパスを介した変数（それらの使用-DEFチェーン）のトレース定義のテスト。XOR操作が変数に適用された後、使用-DEFチェーンには再定義が含まれるようになりました。

$./test_xor.sh

ターゲットパスを満た​​すために入力を生成するためにパスとZ3を実行するには：

$./complete_test_xor.sh

追加オペレーターの実行の予想出力

 $./complete_test_base_case.sh


...Starting LLVM to Z3 Solver...

[+] Starting Base Case Test

[ CLANG COMPILING TEST APP SOURCES ]


[ RUNNING DOMINATOR TREE PASS ]


<-- Starting analysis from main() --> 
	[+] Tracing first path of DominatorTree


[ COMPARE FOUND ]
	Comparison Operator: IS EQUAL (==)



	[+] VALUE TWO: 
				==> Found Constant Operand: Integer :: 69




	[+] VALUE ONE: 

	Reovering variable operations and starting value....
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
		.... Potential find. Store took value from :: argv

			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
[ COMPARE FOUND ]
	Comparison Operator: IS EQUAL (==)



	[+] VALUE TWO: 
				==> Found Constant Operand: Integer :: 68




	[+] VALUE ONE: 

	Reovering variable operations and starting value....
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
		.... Potential find. Store took value from :: argv

			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
[ COMPARE FOUND ]
	Comparison Operator: IS EQUAL (==)



	[+] VALUE TWO: 
				==> Found Constant Operand: Integer :: 67




	[+] VALUE ONE: 

	Reovering variable operations and starting value....
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
		.... Potential find. Store took value from :: argv

			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
[ COMPARE FOUND ]
	Comparison Operator: IS EQUAL (==)



	[+] VALUE TWO: 
				==> Found Constant Operand: Integer :: 66




	[+] VALUE ONE: 

	Reovering variable operations and starting value....
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
	[!] FOUND TERMINATING ALLOCATION

			[-] RECURSING THROUGH OPERATION
		[ TRACING BACK HISTORY OF OPERAND VALUE ]
		[+] Found StoreInst to trace
		.... Potential find. Store took value from :: argv

			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
			[-] RECURSING THROUGH OPERATION
Breaking at end of first path with # of children
[ CHECK ]: 0 == 0

<-- Successfully Traversed Dominator Tree --> 
[+] The below arguments are operated upon, then this redefinition must finally  be equal to the comparisons shown below.

argv[0];== 69
argv[1];== 68
argv[2];== 67
argv[3];== 66

[ FINISHED ]


[ LLVM Ported to Z3 ] 
['argv[0]', '== 69']
[ BUILDING EQUATION ]
x == 69
[+] Added all conditions to z3
	[+] Checking Satisfiability
	sat
argv[0]: 69

['argv[1]', '== 68']
[ BUILDING EQUATION ]
x == 68
[+] Added all conditions to z3
	[+] Checking Satisfiability
	sat
argv[1]: 68

['argv[2]', '== 67']
[ BUILDING EQUATION ]
x == 67
[+] Added all conditions to z3
	[+] Checking Satisfiability
	sat
argv[2]: 67

['argv[3]', '== 66']
[ BUILDING EQUATION ]
x == 66
[+] Added all conditions to z3
	[+] Checking Satisfiability
	sat
argv[3]: 66


[ KEY FOUND ]

EDCB


...Solver Finished...
拡大する
追加情報
関連アプリ
おすすめ
関連情報 すべて