Inicio>código fuente JSP>Otras categorias
Descargar

Domtresat

Domtresat (DTS) es un sistema de análisis estático que toma el código fuente como entrada y produce automáticamente informes de satisfacción de la ruta para las rutas recopiladas a partir de una estructura de árbol dominador creado. Obtiene una cobertura de código máxima con una intervención humana mínima. Domtresat crea un árbol dominador de variables controladas por el usuario, luego genera restricciones y operaciones colocadas en sus valores para ser alimentados a un solucionador de satisfacción. Esto genera posibles puntos de interés en el programa para el descubrimiento de vulnerabilidad.

Motivación principal

El uso principal de esta herramienta es determinar la accesibilidad de la entrada controlable a un objetivo en el programa, así como lo que esta entrada debe ser para llegar allí. El objetivo se establece automáticamente para ser la ruta más dominada del árbol. Esto ayuda a un auditor a identificar una ruta hacia el código vulnerable a través de una serie de cheques como el diagrama a continuación. En programas como estos, es la ruta más dominada por la que queremos irrumentar y analizar la cadena de defensa de uso. 

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

Teoría del análisis

Árboles dominadores

Esta herramienta predeterminada primero para analizar las rutas más dominadas primero. Estos caminos pueden describirse como aquellos con variables que se actúan más. Esto se puede cambiar en función de la necesidad y un script de recompilación rápido está en su lugar para generar bibliotecas alteradas.

Uso de las cadenas definidas

Las cadenas de uso de uso (uso de uso) son una estructura de datos que consiste en un uso de una variable, y todas las definiciones de esa variable que pueden alcanzar ese uso sin ninguna otra definición intermedia.

Esta herramienta se basa en extraer estas estructuras de datos de la ruta más dominada que se encuentra a través del árbol Dominator creado. La idea básica es que dado un uso específico, es decir, el uso de una variable para llegar o causar una vulnerabilidad, podemos rastrear esta variable a través de todas sus (re) definiciones y determinar a) si es controlable del usuario, y b) qué operaciones se realizan en esta entrada antes de que se use en la vulnerabilidad (estas se convierten en nuestras restricciones).

Edificio

Domtresat ha sido probado en LLVM 3.7.1.

  1. Instalar dependencias
  • OS X: brew install z3
  • Linux/Windows: siga las instrucciones en Z3Prover/Z3
  1. $./quick_setup.sh para construir y ejecutar pruebas
  2. $./partial_build.sh para realizar una reconstrucción incremental después de alterar los métodos de análisis

Uso

Esta sección describe cómo ejecutar pruebas y alimentarlas al solucionador SAT.

Prueba de caja base

Pruebas para rastrear definiciones de variables (sus cadenas de uso de uso) a través del camino más dominado

$./test_base_case.sh

Para ejecutar esta prueba con Z3 para generar información para satisfacer la ruta objetivo:

$./complete_test_base_case.sh

Prueba de operador adicional

Pruebas para el rastreo de definiciones de variables (sus cadenas de uso de uso) a través de la ruta más dominada, donde la cadena de uso de uso ahora contiene redefiniciones después de que las operaciones de adición se aplican a la variable.

$./test_addition.sh

Para ejecutar Pase y Z3 para generar información para satisfacer la ruta objetivo:

$./complete_test_addition.sh

Prueba del operador de sustracción

Pruebas para el rastreo de definiciones de variables (sus cadenas de uso de uso) a través de la ruta más dominada, donde la cadena de uso de uso ahora contiene redefiniciones después de que las operaciones de sustracción se aplican a la variable.

$./test_subtraction.sh

Para ejecutar Pase y Z3 para generar información para satisfacer la ruta objetivo:

$./complete_test_subtraction.sh

Prueba del operador XOR

Pruebas para el rastreo de definiciones de variables (sus cadenas de uso de uso) a través de la ruta más dominada, donde la cadena de uso de uso ahora contiene redefiniciones después de que las operaciones de XOR se aplican a la variable.

$./test_xor.sh

Para ejecutar Pase y Z3 para generar información para satisfacer la ruta objetivo:

$./complete_test_xor.sh

Salida esperada para la ejecución del operador adicional 

 $./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...
Expandir
Información adicional
Aplicaciones relacionadas
Recomendado para ti
Información relacionada Todo