Software Vulnerability 문서 원본 보기

Symbolic Execution[14]

  심볼릭 실행은 실제 값 대신 Symbolic을 추적하는 프로그램의 분석을 나타낸다. 예를 들면, 이 그림과 같은 코드가 있을 때 read() 함수의 리턴 값을 symbolic variable로 정하고 s 라고 한다.  (여기서 s와 y는 동일하다.) 심볼릭 실행을 통해, y=2*y를 거치면 y=2*s 가된다. 다음 조건문에서 if(y==12)를 통과하는 데 조건문의 결과가 TRUE면 2s=12가 된다. 이와 같은 방식으로 symbolic variable s를 실행과정에서 추적하면서 프로그램을 분석을 한다. STP는 테스트 케이스를 생성하는 것에 도움을 주는 툴로 비트벡터(Boolean 시퀀스 변수)의 산술에 대한 결정 절차(decision procedure)이다. 심볼릭 실행을 바탕으로 구성이 되어 있고 조건식을 쿼리를 전달받아 테스트 케이스를 생성하는데 도움을 준다. 심볼릭 실행은 최근 프로그래밍 언어 학자들에 의해 개발된 방법이며, 특히 프로그램 테스팅 시 다양한 경로와 조건을 실행할 수 있는 입력 값 및 초기 값 생성을 가능케 한다.

(1) 동적 심볼릭 수행 도구(KLEE) [18]
  KLEE 는 LLVM bytecode 의 해석기를 기반으로, LLVM bytecode 로 컴파일 된 프로그램을 입력으로 받아서 명령어를 수행하고 심볼릭하게 표현된 프로그램의 상태 변경을 기록한다. 프로그램 수행 가운데 분기를 만나게 되면 현재 프로그램의 심볼릭 상태에 따라 분기할 수 있는 경우를 계산하고 가능한 실행 경로를 따라 계속해서 프로그램을 실행한다. 현재 프로그램의 심볼릭 상태가 특정 분기를 실행할 수 있는지 검사하기 위해 KLEE 는 bit-level 정확도를 갖는 조건식을 생성하고 bit-vector 로직을 지원하는 SMT solver 를 사용해서 조건식을 풀어낸다.

(가) KLEE 수행 예

int my_islower(int x) {
  if (x >= 'a' && x <= 'z')
    return 1;
  else return 0;
}


KLEE를 이용하여 위와 같은 함수를 테스팅을 하기 위해서는 symbolic input으로 실행을 하여야한다. 따라서 klee_make_symbolicdmf 이용하여 값에 symbolic 마킹을 하고 이를 사용한다.

int main() {
      char c;
      klee_make_symbolic(&c, sizeof(c), "input"); 
      return my_islower(c);
  } 


위와 같은 코드를 LLVM bitcode로 컴파일 파일을 한다. 

$ llvm-gcc --emit-llvm -c -g demo.c



$ klee demo.o 
KLEE: output directory = "klee-out-0"
KLEE: done: total instructions = 69  
KLEE: done: completed paths = 3      
KLEE: done: generated tests = 3
컴파일을 통해 나온 결과를 다음과 같이 실행을 한다.

이와 같이 3가지의 testcase를 생성한 것을 볼 수 있다. 3가지의 testcase 내용은 다음과 같다. 

$ ktest-tool klee-last/test000001.ktest 
  ktest file : 'klee-last/test000001.ktest'
  args       : ['demo.o']
  num objects: 1
  object    0: name: 'input'
  object    0: size: 1
  object    0: data: 'b'

$ ktest-tool klee-last/test000002.ktest 
  ...
  object    0: data: '~'

$ ktest-tool klee-last/test000003.ktest 
  ..
  object    0: data: '\x00'


이와 같이 3가지의 testcase를 이용하여 프로그램을 실행하여보면 다음과 같은 결과를 얻을 수 있다.

$ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
$ KTEST_FILE=klee-last/test000001.ktest ./a.out 
$ echo $?
  1
$ KTEST_FILE=klee-last/test000002.ktest ./a.out 
$ echo $?
  0
$ KTEST_FILE=klee-last/test000003.ktest ./a.out
$ echo $?
  0 


  위의 결과를 보면 KLEE는 if (x >= 'a' && x <= 'z') 조건에 대하여 x를 symbolic value로 정하고 이에 대한 값 \x00, ‘b’, ‘~’를 만들어 낸 것을 확인 할 수 있다. 이는 'a'보다 작은 케이스, x >= 'a' && x <= 'z' 조건에 부합하는 케이스, ‘z’보다 큰 케이스를 생성하였다고 확인 할 수 있다.