الصفحة الرئيسية>كود المصدر JSP>فئات أخرى
تنزيل

Domtresat

DOMTRESAT (DTS) هو نظام تحليل ثابت يأخذ الكود المصدر كمدخلات وينتج تلقائيًا تقارير إرضاء المسار للمسارات التي تم جمعها من بنية شجرة dominator التي تم إنشاؤها. يحصل على تغطية كود أقصى مع الحد الأدنى من التدخل البشري. تقوم Domtresat بإنشاء شجرة dominator من المتغيرات التي يسيطر عليها المستخدم ، ثم يخرج القيود والعمليات الموضوعة على قيمها ليتم تغذيتها لحل الرضا. هذا يولد نقاط الاهتمام المحتملة في البرنامج لاكتشاف الضعف.

الدافع الأساسي

الاستخدام الرئيسي لهذه الأداة هو تحديد إمكانية الوصول إلى المدخلات التي يمكن التحكم فيها إلى هدف في البرنامج ، وكذلك ما يجب أن يكون هذا المدخلات للوصول إلى هناك. يتم تعيين الهدف تلقائيًا ليكون المسار الأكثر هيمنة على الشجرة. يساعد هذا المدقق في تحديد طريق إلى الكود الضعيف من خلال سلسلة من عمليات الفحص مثل الرسم البياني أدناه. في مثل هذه البرامج ، هذا هو المسار الأكثر تهيمن عليها الذي نريد أن ننشئه وتحليل سلسلة الاستخدام. 

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

نظرية التحليل

الأشجار المهيمنة

هذه الأداة تتخلف عن تحليل المسارات الأكثر هيمنة أولاً. يمكن وصف هذه المسارات على أنها تلك التي لديها متغيرات يتم تصرفها أكثر من غيرها. يمكن تغيير هذا بناءً على الحاجة ، ويقع برنامج إعادة تجميع سريع لإنشاء مكتبات تم تغييرها.

استخدام السلاسل المعرفة

سلاسل الاستخدام المعرفة (USE-DEF) هي بنية بيانات تتكون من استخدام متغير ، وجميع تعريفات هذا المتغير التي يمكن أن تصل إلى الاستخدام دون أي تعريفات متداخلة أخرى.

تعتمد هذه الأداة على سحب هياكل البيانات هذه من المسار الأكثر هيمنة التي تم العثور عليها من خلال شجرة Dominator التي تم إنشاؤها. الفكرة الأساسية هي أنه بالنظر إلى الاستخدام المستهدف ، أي استخدام متغير إما للوصول إلى أو التسبب في ثغرة أمنية ، يمكننا تتبع هذا المتغير من خلال جميع تعريفاته (إعادة) وتحديد أ) إذا كان قابلاً للتحكم في المستخدم ، و ب) ما هي العمليات التي يتم في هذا الإدخال قبل استخدامه في الضعف (تصبح هذه القيود).

مبنى

تم اختبار 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

اختبار مشغل الإضافة

اختبارات تتبع تعريفات المتغيرات (سلاسل استخدامها) من خلال المسار الأكثر هيمنة ، حيث تحتوي سلسلة الاستخدام DEF الآن على إعادة تعريف بعد عمليات الإضافة على المتغير.

$./test_addition.sh

لتشغيل PASS و Z3 لتوليد الإدخال لتلبية المسار المستهدف:

$./complete_test_addition.sh

اختبار مشغل الطرح

اختبارات تتبع تعريفات المتغيرات (سلاسل استخدامها) من خلال المسار الأكثر هيمنة ، حيث تحتوي سلسلة الاستخدام DEF الآن على إعادة تعريف بعد عمليات الطرح على المتغير.

$./test_subtraction.sh

لتشغيل PASS و Z3 لتوليد الإدخال لتلبية المسار المستهدف:

$./complete_test_subtraction.sh

اختبار المشغل XOR

اختبارات تتبع تعريفات المتغيرات (سلاسل استخدامها) من خلال المسار الأكثر هيمنة ، حيث تحتوي سلسلة الاستخدام DEF الآن على إعادة تعريف بعد تطبيقات 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...
يوسع
معلومات إضافية
تطبيقات ذات صلة
نوصي لك
أخبار ذات صلة الكل