DomTreSat

domtresat

DTS (Domtresat)는 소스 코드를 입력으로 취하고 생성 된 도미네이터 트리 구조에서 수집 된 경로에 대한 경로 만족도 보고서를 자동으로 생성하는 정적 분석 시스템입니다. 최소한의 인간 개입으로 최대 코드 커버리지를 얻습니다. DomTresat는 사용자 제어 변수의 지배자 트리를 생성 한 다음 만족도 솔버에게 공급 될 값에 대한 제약 조건과 작업을 출력합니다. 이는 취약성 발견을위한 프로그램에서 잠재적 인 관심 지점을 생성합니다.

주요 동기

이 도구의 주요 사용은 프로그램의 대상에 대한 제어 가능한 입력의 도달 범위 와이 입력이 무엇인지 결정하는 것입니다. 대상은 자동으로 트리의 가장 지배적 인 경로로 설정됩니다. 이를 통해 감사인은 아래 다이어그램과 같은 일련의 검사를 통해 취약한 코드의 경로를 식별하는 데 도움이됩니다. 이와 같은 프로그램에서는 사용 정의 체인을 구매하고 분석하려는 가장 지배적 인 경로입니다.

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

분석 이론

지배자 나무

이 도구는 기본적으로 가장 지배적 인 경로를 먼저 분석합니다. 이 경로는 가장 많이 작동하는 변수를 가진 경로로 설명 할 수 있습니다. 이것은 필요에 따라 변경 될 수 있으며 변경된 라이브러리를 생성하기 위해 빠른 재 컴파일 스크립트가 마련되었습니다.

정의 체인을 사용하십시오

사용-정의 체인 (use-def)은 변수를 사용하는 것으로 구성된 데이터 구조와 다른 중재 정의없이 사용하는 변수의 모든 정의입니다.

이 도구는 이러한 데이터 구조를 생성 된 지배자 트리를 통해 발견되는 가장 지배적 인 경로에서 끌어 당기는 데 의존합니다. 기본 아이디어는 대상의 사용, 즉 취약성에 도달하거나 취약성을 유발하기 위해 변수를 사용하는 경우, 모든 (재) 정의를 통해이 변수를 추적하고 a) 사용자 제어 가능 여부를 결정할 수 있다는 것입니다. b) 취약성에 사용되기 전에이 입력에 대해 수행되는 작업 (이는 제약 조건이됩니다).

건물

DOMTRESAT는 LLVM 3.7.1에서 테스트되었습니다.

1. 종속성을 설치하십시오

• OS X : brew install z3
• Linux/Windows : Z3Prover/Z3의 지침을 따르십시오

2. $./quick_setup.sh 테스트를 구축하고 실행합니다
3. $./partial_build.sh 분석 방법 변경 후 증분 재건을 수행합니다.

용법

이 섹션에서는 테스트를 실행하여 SAT 솔버에게 공급하는 방법에 대해 설명합니다.

기본 케이스 테스트

가장 지배적 인 경로를 통한 변수 (그들의 사용 사망)의 정의 추적 테스트

$./test_base_case.sh

대상 경로를 만족시키기 위해 입력을 생성하기 위해 Z3 로이 테스트를 실행하려면 :

$./complete_test_base_case.sh

추가 연산자 테스트

가장 지배적 인 경로를 통한 변수 (사용-DEF 체인)의 추적 정의에 대한 테스트는 첨가 작업이 변수에 적용된 후에도 다시 정의를 포함하는 가장 지배적 인 경로를 통한 변수 (사용-DEF 체인)를 추적합니다.

$./test_addition.sh

대상 경로를 만족시키기 위해 입력을 생성하기 위해 패스 및 Z3를 실행하려면 :

$./complete_test_addition.sh

빼기 연산자 테스트

가장 지배적 인 경로를 통한 변수 (사용-DEF 체인)의 추적 정의에 대한 테스트는 현재 Def-DEF 체인이 변수에 적용된 후 재 정의를 포함하는 가장 지배적 인 경로를 통해 정의됩니다.

$./test_subtraction.sh

대상 경로를 만족시키기 위해 입력을 생성하기 위해 패스 및 Z3를 실행하려면 :

$./complete_test_subtraction.sh

XOR 운영자 테스트

가장 지배적 인 경로를 통한 변수 (사용 -DEF 체인)의 추적 정의에 대한 테스트는 XOR 작업이 변수에 적용된 후에도 다시 정의를 포함하는 가장 지배적 인 경로를 통한 가장 지배적 인 경로를 통한 것입니다.

$./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...