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

List

Concrete execution

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

Example

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

#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))

#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

Related site

• https://en.wikipedia.org/wiki/Symbolic_execution