Beranda>Kode sumber JSP>Kategori lainnya
Unduh

Domtresat

Domtresat (DTS) adalah sistem analisis statis yang mengambil kode sumber sebagai input dan secara otomatis menghasilkan laporan kepuasan jalur untuk jalur yang dikumpulkan dari struktur pohon dominator yang dibuat. Ini memperoleh cakupan kode maksimal dengan intervensi manusia minimal. Domtresat menciptakan pohon dominator dari variabel yang dikendalikan pengguna, kemudian keluaran kendala dan operasi yang ditempatkan pada nilainya untuk diumpankan ke pemecah kepuasan. Ini menghasilkan titik -titik potensial yang menarik dalam program untuk penemuan kerentanan.

Motivasi utama

Penggunaan utama alat ini adalah menentukan jangkauan input yang dapat dikendalikan ke target dalam program, serta apa yang diperlukan input ini untuk sampai ke sana. Target secara otomatis diatur menjadi jalur pohon yang paling didominasi. Ini membantu auditor mengidentifikasi jalur ke kode rentan melalui serangkaian cek seperti diagram di bawah ini. Dalam program seperti ini, ini adalah jalur yang paling banyak didominasi yang ingin kami lakukan dan menganalisis rantai penggunaan-definisi. 

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

Teori Analisis

Pohon Dominator

Alat ini default untuk menganalisis jalur yang paling didominasi terlebih dahulu. Jalur ini dapat digambarkan sebagai variabel yang paling banyak ditindaklanjuti. Ini dapat diubah berdasarkan kebutuhan dan skrip kompilasi cepat ada untuk menghasilkan perpustakaan yang diubah.

Rantai Define-Define

Rantai penggunaan-define (penggunaan-def) adalah struktur data yang terdiri dari penggunaan variabel, dan semua definisi variabel yang dapat mencapai penggunaan tanpa definisi intervensi lainnya.

Alat ini bergantung pada menarik struktur data ini dari jalur yang paling didominasi yang ditemukan melalui pohon dominator yang dibuat. Gagasan dasarnya adalah bahwa mengingat penggunaan yang ditargetkan, yaitu penggunaan variabel untuk mendapatkan atau menyebabkan kerentanan, kita dapat melacak variabel ini melalui semua definisi (re-re) dan menentukan a) jika pengguna dapat dikendalikan, dan b) operasi apa yang dilakukan pada input ini sebelum digunakan dalam kerentanan (ini menjadi kendala kita).

Bangunan

Domtresat telah diuji pada LLVM 3.7.1.

  1. Instal dependensi
  • OS X: brew install z3
  • Linux/Windows: Ikuti instruksi di Z3Prover/Z3
  1. $./quick_setup.sh untuk membangun dan menjalankan tes
  2. $./partial_build.sh untuk melakukan pembangunan kembali tambahan setelah mengubah metode analisis

Penggunaan

Bagian ini menjelaskan cara menjalankan tes dan memberi makan mereka ke pemecah SAT.

Tes kasus dasar

Tes untuk melacak definisi variabel (rantai penggunaan-def) melalui jalur yang paling didominasi

$./test_base_case.sh

Untuk menjalankan tes ini dengan Z3 untuk menghasilkan input untuk memenuhi jalur target:

$./complete_test_base_case.sh

Tes Operator Tambahan

Tes untuk melacak definisi variabel (rantai penggunaan-def) melalui jalur yang paling didominasi, di mana rantai penggunaan-def sekarang berisi definisi ulang setelah operasi tambahan diterapkan pada variabel.

$./test_addition.sh

Untuk menjalankan pass dan z3 untuk menghasilkan input untuk memenuhi jalur target:

$./complete_test_addition.sh

Tes Operator Pengurangan

Tes untuk melacak definisi variabel (rantai penggunaan-def) melalui jalur yang paling didominasi, di mana rantai penggunaan-def sekarang berisi definisi ulang setelah operasi pengurangan diterapkan pada variabel.

$./test_subtraction.sh

Untuk menjalankan pass dan z3 untuk menghasilkan input untuk memenuhi jalur target:

$./complete_test_subtraction.sh

Tes Operator XOR

Tes untuk melacak definisi variabel (rantai penggunaan-def) melalui jalur yang paling didominasi, di mana rantai penggunaan-def sekarang berisi definisi ulang setelah operasi XOR diterapkan pada variabel.

$./test_xor.sh

Untuk menjalankan pass dan z3 untuk menghasilkan input untuk memenuhi jalur target:

$./complete_test_xor.sh

Output yang diharapkan untuk menjalankan operator tambahan 

 $./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...
Memperluas
Informasi Tambahan
Aplikasi Terkait
Direkomendasikan untuk Anda
Informasi Terkait Semua