DomTreSat скачать - загрузка исходного кода DomTreSat

DomTreSat

Другие категории

1.0.0

Скачать

Domtresat

Domtresat (DTS) - это система статического анализа, которая принимает исходный код в качестве входного и автоматически дает отчеты о удовлетворенности пути для путей, собранных из созданной структуры дерева доминатора. Он получает максимальное покрытие кода с минимальным вмешательством человека. Domtresat создает дерево доминатора с контролируемыми пользователями переменных, а затем выводит ограничения и операции, помещенные на их значения, которые будут подаваться на решатель удовлетворенности. Это генерирует потенциальные точки интереса к программе для обнаружения уязвимости.

Первичная мотивация

Основным использованием этого инструмента является определение достижения контролируемого ввода к цели в программе, а также то, что должен быть этот вход, чтобы попасть туда. Цель автоматически устанавливается как наиболее доминирующий путь дерева. Это помогает аудитору определить путь к уязвимому коду через серию проверок, таких как диаграмма ниже. В таких программах это самый доминирующий путь, который мы хотим купить и проанализировать цепочку с использованием использования.

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

Теория анализа

Доминирующие деревья

Этот инструмент по умолчанию по умолчанию в первую очередь анализирует наиболее доминирующие пути. Эти пути могут быть описаны как с переменными, которые действуют наиболее. Это может быть изменено в зависимости от потребностей, и существует быстрый сценарий перекомпиляции для создания измененных библиотек.

Использование цепочек

Использование цепочек (использование-def)-это структура данных, которая состоит из использования переменной, и всех определений этой переменной, которая может достичь этой использования без каких-либо других промежуточных определений.

Этот инструмент полагается на извлечение этих структур данных с наиболее доминированного пути, который находится через созданное дерево доминатора. Основная идея заключается в том, что, учитывая целевое использование, то есть использование переменной для достижения или вызвать уязвимость, мы можем проследить эту переменную через все его (повторные) определения и определить а), если она управляется пользователем, и б) какие операции выполняются при этом входе до того, как он будет использован в уязвимости (они становятся нашими ограничениями).

Здание

Domtresat был протестирован на LLVM 3.7.1.

Установить зависимости

OS X: brew install z3
Linux/Windows: следуйте инструкциям на Z3Prover/Z3

$./quick_setup.sh для создания и запуска тестов
$./partial_build.sh для выполнения постепенного восстановления после изменения методов анализа

Использование

В этом разделе описывается, как запускать тесты и подавать их до решателя SAT.

Базовый тест корпуса

Тесты для отслеживания определений переменных (их цепочки использования) через наиболее доминируемый путь

$./test_base_case.sh

Чтобы запустить этот тест с Z3 для генерации входа для удовлетворения целевого пути:

$./complete_test_base_case.sh

Тест оператора с добавлением

Тесты для отслеживания определений переменных (их цепочки использования) через наиболее доминирующий путь, где цепочка использования-дефицита теперь содержит повторные определения после применения операций добавления к переменной.

$./test_addition.sh

Запустить Pass и Z3 для генерации ввода для удовлетворения целевого пути:

$./complete_test_addition.sh

Тест оператора вычитания

Тесты для отслеживания определений переменных (их цепочки использования) через наиболее доминирующий путь, где цепочка использования-дефицита теперь содержит повторные определения после того, как операции вычитания применяются к переменной.

$./test_subtraction.sh

Запустить Pass и Z3 для генерации ввода для удовлетворения целевого пути:

$./complete_test_subtraction.sh

Тест оператора XOR

Тесты для отслеживания определений переменных (их цепочки использования) через наиболее доминирующий путь, где цепочка использования-дефицита теперь содержит повторные определения после применения операций XOR к переменной.

$./test_xor.sh

Запустить Pass и 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...

Расширять

Дополнительная информация