Page d'accueil>Code source JSP>Autres catégories
Télécharger

Domtresat

Domtresat (DTS) est un système d'analyse statique qui prend le code source en entrée et produit automatiquement des rapports de satisfabilité des chemins pour les chemins recueillis à partir d'une structure d'arbre dominatrice créée. Il obtient une couverture de code maximale avec une intervention humaine minimale. DomtResat crée un arbre dominateur de variables contrôlées par l'utilisateur, puis produit des contraintes et des opérations placées sur leurs valeurs à transmettre à un solveur de satisfaction. Cela génère des points potentiels d'intérêt dans le programme de découverte de vulnérabilité.

Motivation principale

L'utilisation principale de cet outil est de déterminer la contraabilité de l'entrée contrôlable dans une cible dans le programme, ainsi que ce que cette entrée doit être pour y arriver. La cible est automatiquement définie pour être le chemin le plus dominé de l'arbre. Cela aide un auditeur à identifier un chemin vers le code vulnérable à travers une série de vérifications comme le diagramme ci-dessous. Dans des programmes comme ceux-ci, c'est le chemin le plus dominé que nous voulons construire et analyser la chaîne définie par l'utilisation. 

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

Théorie de l'analyse

Arbres dominateurs

Cet outil analyse par défaut les chemins les plus dominés en premier. Ces chemins peuvent être décrits comme ceux avec des variables qui sont les plus agités. Cela peut être modifié en fonction des besoins et un script de recompilation rapide est en place pour générer des bibliothèques modifiées.

Chaînes définies par l'utilisation

Les chaînes de définition de l'utilisation (USE-DEF) sont une structure de données qui consiste en une utilisation d'une variable, et toutes les définitions de cette variable qui peuvent atteindre cette utilisation sans aucune autre définition intermédiaire.

Cet outil repose sur le tir de ces structures de données du chemin le plus dominé que l'on trouve à travers l'arbre Dominator créé. L'idée de base est que, étant donné une utilisation ciblée, c'est-à-dire l'utilisation d'une variable pour accéder ou provoquer une vulnérabilité, nous pouvons retracer cette variable à travers toutes ses (ré) définitions et déterminer a) si elle est contrôlable par l'utilisateur, et b) quelles opérations sont effectuées sur cette entrée avant son utilisation dans la vulnérabilité (celles-ci deviennent nos contraintes).

Bâtiment

Domtresat a été testé sur LLVM 3.7.1.

  1. Installer des dépendances
  • OS X: brew install z3
  • Linux / Windows: Suivez les instructions sur Z3Prover / Z3
  1. $./quick_setup.sh pour construire et exécuter des tests
  2. $./partial_build.sh pour effectuer une reconstruction incrémentielle après avoir modifié les méthodes d'analyse

Usage

Cette section décrit comment exécuter des tests et les alimenter au solveur SAT.

Test de cas de base

Tests pour le traçage des définitions des variables (leurs chaînes d'utilisation-def) par le chemin le plus dominé

$./test_base_case.sh

Pour exécuter ce test avec Z3 pour générer des entrées pour satisfaire le chemin cible:

$./complete_test_base_case.sh

Test de l'opérateur d'addition

Tests pour les définitions de traçage des variables (leurs chaînes d'utilisation-def) par le chemin le plus dominé, où la chaîne d'utilisation-def contient désormais des redéfinitions après les opérations d'addition appliquées à la variable.

$./test_addition.sh

Pour exécuter Pass et Z3 pour générer des entrées pour satisfaire le chemin cible:

$./complete_test_addition.sh

Test de l'opérateur de soustraction

Tests pour les définitions de traçage des variables (leurs chaînes d'utilisation-def) par le chemin le plus dominé, où la chaîne d'utilisation-DEF contient désormais des redéfinitions après des opérations de soustraction appliquées à la variable.

$./test_subtraction.sh

Pour exécuter Pass et Z3 pour générer des entrées pour satisfaire le chemin cible:

$./complete_test_subtraction.sh

Test de l'opérateur XOR

Tests pour le traçage des définitions des variables (leurs chaînes d'utilisation-def) à travers le chemin le plus dominé, où la chaîne d'utilisation-def contient désormais des redéfinitions après les opérations XOR appliquées à la variable.

$./test_xor.sh

Pour exécuter Pass et Z3 pour générer des entrées pour satisfaire le chemin cible:

$./complete_test_xor.sh

Sortie attendue pour l'opérateur d'addition 

 $./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...
Développer
Informations supplémentaires
Applications connexes
Recommandé pour vous
Actualités connexes Tout