Página Inicial>Código fonte JSP>Outras categorias
Baixar

Domtresat

O Domtresat (DTS) é um sistema de análise estática que toma o código -fonte como entrada e produz automaticamente relatórios de satisfação do caminho para os caminhos coletados de uma estrutura de árvore de dominador criada. Ele obtém cobertura máxima de código com o mínimo de intervenção humana. O Domtresat cria uma árvore dominadora de variáveis ​​controladas pelo usuário, em seguida, produz restrições e operações colocadas em seus valores a serem alimentadas a um solucionador de satisfação. Isso gera possíveis pontos de interesse no programa para descoberta de vulnerabilidades.

Motivação primária

O uso principal desta ferramenta é determinar a acessibilidade da entrada controlável de um destino no programa, bem como o que essa entrada precisa ser para chegar lá. O alvo é automaticamente definido como o caminho mais dominado da árvore. Isso ajuda um auditor a identificar um caminho para o código vulnerável através de uma série de verificações como o diagrama abaixo. Em programas como esses, é o caminho mais dominado para o qual queremos comprar e analisar a cadeia de uso de uso. 

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

Teoria da análise

Árvores dominadoras

Essa ferramenta indica os padrões mais dominados primeiro. Esses caminhos podem ser descritos como aqueles com variáveis ​​que mais são atuadas. Isso pode ser alterado com base na necessidade e um script de recompilação rápida está no lugar para gerar bibliotecas alteradas.

Correntes de uso de uso

As cadeias de uso de uso (Use-DeF) são uma estrutura de dados que consiste no uso de uma variável e todas as definições dessa variável que podem alcançar esse uso sem nenhuma outra definição intermediária.

Essa ferramenta depende da extração dessas estruturas de dados do caminho mais dominado, encontrado através da árvore do Dominator criada. A idéia básica é que, dado um uso direcionado, ou seja, o uso de uma variável para chegar ou causar uma vulnerabilidade, podemos rastrear essa variável em todas as suas (re-) definições e determinar a) se for controlável pelo usuário e b) quais operações são feitas nessa entrada antes de ser usada na vulnerabilidade (essas se tornarem nossas restrições).

Prédio

O Domtresat foi testado no LLVM 3.7.1.

  1. Instalar dependências
  • OS X: brew install z3
  • Linux/Windows: Siga as instruções no Z3Prover/Z3
  1. $./quick_setup.sh para construir e executar testes
  2. $./partial_build.sh para realizar uma reconstrução incremental após a alteração de métodos de análise

Uso

Esta seção descreve como executar testes e alimentá -los para o solucionador de SAT.

Teste de caso base

Testes para definições de rastreamento de variáveis ​​(suas cadeias de uso-Def) através do caminho mais dominado

$./test_base_case.sh

Para executar este teste com Z3 para gerar entrada para satisfazer o caminho de destino:

$./complete_test_base_case.sh

Teste do operador de adição

Testes para definições de rastreamento de variáveis ​​(suas cadeias de uso de uso) através do caminho mais dominado, onde a cadeia de uso de uso agora contém redefinições após as operações de adição são aplicadas à variável.

$./test_addition.sh

Para executar o passe e o Z3 para gerar entrada para satisfazer o caminho do alvo:

$./complete_test_addition.sh

Teste do operador de subtração

Testes para rastrear definições de variáveis ​​(suas cadeias de uso de uso) através do caminho mais dominado, onde a cadeia de uso de uso agora contém redefinições após as operações de subtração são aplicadas à variável.

$./test_subtraction.sh

Para executar o passe e o Z3 para gerar entrada para satisfazer o caminho do alvo:

$./complete_test_subtraction.sh

Teste do operador XOR

Testes para definições de rastreamento de variáveis ​​(suas cadeias de uso de uso) através do caminho mais dominado, onde a cadeia de uso de uso agora contém redefinições após as operações do XOR são aplicadas à variável.

$./test_xor.sh

Para executar o passe e o Z3 para gerar entrada para satisfazer o caminho do alvo:

$./complete_test_xor.sh

Saída esperada para a execução do operador de adição 

 $./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
Informações adicionais
Aplicativos Relacionados
Recomendado para você
Informações Relacionadas Todos