Software Vulnerability 문서 원본 보기

'''Symbolic Execution'''

심볼릭 실행은 실제 값 대신 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)이다. 심볼릭 실행을 바탕으로 구성이 되어 있고 조건식을 쿼리를 전달받아 테스트 케이스를 생성하는데 도움을 준다. 심볼릭 실행은 최근 프로그래밍 언어 학자들에 의해 개발된 방법이며, 특히 프로그램 테스팅 시 다양한 경로와 조건을 실행할 수 있는 입력 값 및 초기 값 생성을 가능케 한다.

'''동적 심볼릭 수행 도구(KLEE)''' 

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

'''(1) 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’보다 큰 케이스를 생성하였다고 확인 할 수 있다.



'''(2) KLEE 수행 예 - Maze'''

다음은 KLEE를 사용하여 토이 프로그램인 maze를 자동으로 해결하는 예제이다. 토이 프로그램 maze의 소스코드는 http://pastebin.com/6wG5stht 에서 구할 수 있다. 

먼저 maze예제를 KLEE를 사용하지 않고 수동으로 해결하여 본다. 

 gcc maze.c –o maze

 ( a : Left, d : Right, w : Up, s : Down )
 Player pos: 1x4
 Iteration no. 2. Action: s.
 +-+---+---+
 |X|     |#|
 |X| --+ | |
 |X|   | | |
 |X+-- | | |
 |     |   |
 +-----+---+

[http://feliam.files.wordpress.com/2010/10/maze3.gif]

'#' 까지 도달하기 위한 결과 값이다. 
 ssssddddwwaawwddddssssddwwww

KLEE를 사용하여 자동으로 해결하여 본다. 먼저 KLEE를 사용하기 위해서는 LLVM-gcc를 이용하여 LLVM bitcode를 생성하고 이를 KLEE로 실행하여야 한다. 일반적으로는 다음과 같이 LLVM bitcode는 LLVM bitcode interpreter를 이용하여 수행이 된다. 

 llvm-gcc -c –emit-llvm maze.c -o maze.bc
 lli maze.bc

하지만 KLEE를 이용하여 Symbolic execution을 수행하여야 하기 때문에 LLVM bitcode interpreter 대신 KLEE를 사용한다. Symbolic execution을 위해서는 maze의 입력 값에 marking을 하여야 한다. 따라서 소스코드를 다음과 같이 수정하여야 한다. 

 read(0,program,ITERS); 

소스코드에서 위와 같은 코드를 아래와 같이 변경한다. 

 klee_make_symbolic(program,ITERS,"program");

또한 해더파일의 추가도 필요하다. 

 #include <klee/klee.h>

다음과 같이 컴파일을 한 후 실행하면 

 llvm-gcc -c -Ipath/to/klee –emit-llvm maze_klee.c -o maze_klee.bc
 klee maze.bc

다음과 같은 결과를 얻을 수 있다. KLEE는 321개의 다른 경로를 탐색하였다. 

 KLEE: done: total instructions = 112773
 KLEE: done: completed paths = 321
 KLEE: done: generated tests = 318

그리고 해당 케이스에 대하여 테스트 케이스를 생성한다. 

 $ls klee-last/
 assembly.ll test000078.ktest test000158.ktest
 info test000079.ktest test000159.ktest
 messages.txt test000080.ktest test000160.ktest
 run.istats test000081.ktest test000161.ktest
 run.stats test000082.ktest test000162.ktest
 test000001.ktest test000083.ktest test000163.ktest
 test000075.ktest test000155.ktest warnings.txt

각 케이스는 ktest-tool을 이용하여 확인 할 수 있다. 위의 결과는 문제를 해결하기 위한 테스트 케이스가 아닌 모든 경로에 대한 테스트 케이스이다. 따라서 문제를 해결하는 테스트 케이스를 얻기 위해 소스코드를 수정을 한다. 다음과 같이 “You win!”이라는 메시지를 띄우는 코드 이후에 klee_assert()를 삽입을 한다. klee_assert는 C언어의 assert함수와 동일하다.   ( assert는 주어진 조건이 거짓이면 오류 메시지 출력과 함께 코어 덤프를 출력하고 프로그램을 종료한다. )

 printf ("You win!\n");
 klee_assert(0);  //Signal The solution!!

위와 같이 소스코드를 수정하고 컴파일 후 실행하여 보면 다음과 같이 오류 메시지 및 코어덤프를 생성하는 테스트 케이스를 확인 할 수 있다. 

 $ls -1 klee-last/ |grep -A2 -B2 err
 test000096.ktest
 test000097.ktest
 test000098.assert.err
 test000098.ktest
 test000098.pc

해당 테스트 케이스의 내용을 확인하여 보면 다음과 같다. 

 $ktest-tool klee-last/test000098.ktest
 ktest file : ‘klee-last/test000098.ktest’
 args : ['maze_klee.o']
 num objects: 1
 object 0: name: ‘program’
 object 0: size: 29
 object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00

해당 결과를 통해 maze를 실행하여 보면 다음과 같이 미로의 벽에 문제가 있음을 확인 할 수 있다. 이와 같이 프로그램의 오류 및 버그 등을 찾는데에도 도움이 될 수 있다. 최종적으로 다음과 같이 4가지의 테스트 케이스를 얻을 수 있다. 

 $ktest-tool klee-last/test000097.ktest
 ktest file : ‘klee-last/test000097.ktest’
 args : ['maze_klee.o']
 num objects: 1
 object 0: name: ‘program’
 object 0: size: 29
 object 0: data: ‘sddwddddsddw\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′

 $ktest-tool klee-last/test000136.ktest
 ktest file : ‘klee-last/test000136.ktest’
 args : ['maze_klee.o']
 num objects: 1
 object 0: name: ‘program’
 object 0: size: 29
 object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′

 $ktest-tool klee-last/test000239.ktest
 ktest file : ‘klee-last/test000239.ktest’
 args : ['maze_klee.o']
 num objects: 1
 object 0: name: ‘program’
 object 0: size: 29
 object 0: data: ‘ssssddddwwaawwddddsddw\x00\x00\x00\x00\x00\x00\x00′

 $ktest-tool klee-last/test000268.ktest
 ktest file : ‘klee-last/test000268.ktest’
 args : ['maze_klee.o']
 num objects: 1
 object 0: name: ‘program’
 object 0: size: 29
 object 0: data: ‘ssssddddwwaawwddddssssddwwww\x00′

최초 수동으로 찾은 결과 이외에도 버그를 통해 maze를 해결하는 3가지의 케이스를 더 찾을 수 있다.

 * sddwddddsddw
 * sddwddddssssddwwww
 * ssssddddwwaawwddddsddw
 * ssssddddwwaawwddddssssddwwww

<출처 : http://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ >