หน้าแรก>ซอร์สโค้ด JSP>หมวดหมู่อื่นๆ
ดาวน์โหลด

Domtresat

Domtresat (DTS) เป็นระบบการวิเคราะห์แบบคงที่ที่ใช้ซอร์สโค้ดเป็นอินพุตและสร้างรายงานความพึงพอใจของเส้นทางโดยอัตโนมัติสำหรับเส้นทางที่รวบรวมจากโครงสร้างต้นไม้ Dominator ที่สร้างขึ้นโดยอัตโนมัติ ได้รับการครอบคลุมรหัสสูงสุดพร้อมการแทรกแซงของมนุษย์น้อยที่สุด Domtresat สร้างแผนผัง Dominator ของตัวแปรที่ผู้ใช้ควบคุมจากนั้นเอาต์พุตข้อ จำกัด และการดำเนินการที่วางไว้บนค่าของพวกเขาที่จะป้อนให้กับตัวแก้ความน่าพอใจ สิ่งนี้สร้างจุดที่น่าสนใจที่เป็นไปได้ในโปรแกรมสำหรับการค้นพบช่องโหว่

แรงจูงใจหลัก

การใช้งานหลักของเครื่องมือนี้คือการกำหนดความสามารถในการเข้าถึงอินพุตที่ควบคุมได้ไปยังเป้าหมายในโปรแกรมรวมถึงสิ่งที่อินพุตนี้ต้องไปถึงที่นั่น เป้าหมายถูกตั้งค่าให้เป็นเส้นทางที่โดดเด่นที่สุดของต้นไม้โดยอัตโนมัติ สิ่งนี้ช่วยให้ผู้สอบบัญชีระบุเส้นทางไปยังรหัสที่มีช่องโหว่ผ่านชุดของการตรวจสอบเช่นแผนภาพด้านล่าง ในโปรแกรมเช่นนี้มันเป็นเส้นทางที่โดดเด่นที่สุดที่เราต้องการสร้างและวิเคราะห์ห่วงโซ่การใช้งาน 

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

ทฤษฎีการวิเคราะห์

ต้นไม้ครอบงำ

เครื่องมือนี้เริ่มต้นในการวิเคราะห์เส้นทางที่โดดเด่นที่สุดก่อน เส้นทางเหล่านี้สามารถอธิบายได้ว่าเป็นตัวแปรที่ทำหน้าที่มากที่สุด สิ่งนี้สามารถเปลี่ยนแปลงได้ตามความต้องการและสคริปต์การรวมใหม่อย่างรวดเร็วอยู่ในสถานที่เพื่อสร้างไลบรารีที่เปลี่ยนแปลง

โซ่นิยามใช้

โซ่-นิยามใช้ (ใช้-เดนย่า) เป็นโครงสร้างข้อมูลที่ประกอบด้วยการใช้ตัวแปรและคำจำกัดความทั้งหมดของตัวแปรนั้นที่สามารถเข้าถึงการใช้งานนั้นได้โดยไม่ต้องมีคำจำกัดความอื่น ๆ

เครื่องมือนี้อาศัยการดึงโครงสร้างข้อมูลเหล่านี้จากเส้นทางที่โดดเด่นที่สุดซึ่งพบได้ผ่านต้นไม้ Dominator ที่สร้างขึ้น แนวคิดพื้นฐานคือการใช้งานเป้าหมายเช่นการใช้ตัวแปรเพื่อไปที่หรือก่อให้เกิดช่องโหว่เราสามารถติดตามตัวแปรนี้ผ่านคำจำกัดความทั้งหมด (อีกครั้ง) และกำหนด 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 Solver

การทดสอบกรณีฐาน

การทดสอบคำจำกัดความการติดตามของตัวแปร (โซ่การใช้งาน) ผ่านเส้นทางที่โดดเด่นที่สุด

$./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...
ขยาย
ข้อมูลเพิ่มเติม
แอปที่เกี่ยวข้อง
แนะนำสำหรับคุณ
ข้อมูลที่เกี่ยวข้อง ทั้งหมด