Page tree
Skip to end of metadata
Go to start of metadata

Excuse the ads! We need some help to keep our site up.

List


Concrete execution

  • Concrete execution은 프로그램 실행시 구체적인 값을 바탕으로 프로그램을 분석하는 방식입니다.

Example

  • 다음 코드를 이용해 Concrete execution을 확인 할 수 있습니다.
    • 해당 코드는 아주 간단합니다.
    • 해당 프로그램은 1이라는 고정 값에 의해 "Nice" 라는 문구를 출력합니다.
    • 해당 프로그램을 몇번을 실행해도 실행되는 경로와 결과가 동일합니다.
ConcreteExec.c
#include <stdio.h>

void main(){
	if(1){
		printf("Nice!\n");
	}else{
		printf("Wrong!\n");
	}
}

Symbolic execution

  • Symbolic execution은 프로그램 실행시 구체적인 값이 아닌 미지수가 사용된다면, 해당 값을 기호 값을 가정하여 프로그램을 분석하는 방식입니다.

Example

  • 다음 코드를 이용해 Symbolic execution을 확인 할 수 있습니다.
    • 해당 프로그램은 사용자로 부터 입력 받은 값으로 인해 3가지의 실행 경로를 확인 할 수 있습니다.
    • x, y는 미지수 이며, 해당 값을 기호 값으로 선언합니다.
      • y = λ
      • x = χ
    • 아래와 같은 실행 경로와 식을 확인할 수 있습니다.
      • z의 값이 1000이 아닐 경우((χ * 2) ≠ 1000)
      • z의 값이 1000이고 y의 값이 z보다 작거나 같을 경우(((χ * 2) = 1000) && λ ≤ (χ * 2))
      • z의 값이 1000이고 y의 값이 z보다 클 경우(((χ * 2) = 1000) && λ > (χ * 2))
SymbolicExe.c
#include <stdio.h>

void main(){
	int x,y,z;

	scanf("%d",&x);
	scanf("%d",&y);

	z = x * 2;

	if(z == 1000){
		if(y > z){
			printf("Nice!\n");
		}else{
			printf("Wrong!\n");
		}
	}
}

Limitations

Path Explosion

  • Symbolic execution을 이용해 대형 프로그램의 모든 실행 가능한 경로를 확인하는 것은 적합하지 않습니다.
  • 프로그램의 크기에 따라 실행 가능한 경로의 수는 기하 급수적으로 증가하며, 무한 반복문이 있는 경우 무한으로 실행될 수 있습니다.
  • 해당 문제를 해결하기 위해 다음과 같은 방안이 있습니다.
    • 일반적인 경로 탐색을 위해 휴리스틱을 사용해 코드 적용 범위를 늘립니다.
    • 독립적인 경로를 병렬 처리하여 실행 시간을 단축합니다.
    • 유사한 경로를 병합합니다.

Program-Dependent Efficacy

  • Symbolic execution은 다른 테스팅 패러다임들이 사용하는 입력별 프로그램 분석(추론)보다 이점이 있는 경로별 프로그램 분석(추론)에 사용됩니다.

    • 하지만 만약 적은 입력이 프로그램의 같은 경로를 사용한다면, 각각의 입력별로 테스트하는 것이 비용을 절약 할 수 있습니다.

Environment Interactions

  • 프로그램은 시스템 호출, 신호 수신 등을 수행하여 환경과 상호 작용합니다.
  • symbolic execution이 제어 할 수 없는 구성 요소에 도달 할 때 일관성 문제가 발생할 수 있습니다.

Tool

NamearchitectureUrl
Tritonx86 and x86-64http://triton.quarkslab.com
angrlibVEX based (supporting x86, x86-64, ARM, AARCH64, MIPS, MIPS64, PPC, and PPC64)http://angr.io/

Related site