KLEE 사용법

KLEE

KLEE 설치

KLEE 는 docker image 를 제공하고 있습니다. 

$ docker search klee

위 커맨드를 이용하여 docker image 를 검색하면 다음과 같이 결과를 확인할 수 있습니다.

(docker search 커맨드 중 pemission denied 에러가 발생하면 다음 페이지 참고)

 

KLEE 를 사용할 수 있는 docker image 가 검색되고, 아래 커맨드를 이용하여 KLEE 를 설치합니다.

$ docker pull klee/klee

 

KLEE Container 실행

$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee

Note the --ulimit option sets an unlimited stack size inside the container. This is to avoid stack overflow issues when running KLEE. (from https://klee.github.io/docker/)

• --rm: Docker가 자동으로 컨테이너를 정리하고 파일 시스템을 제거합니다.
• -ti: 대화형 프로세스(like a shell)의 경우, 컨테이너 프로세스에 tty를 할당하기 위해 -i -t를 함께 사용합니다.

아래와 같이 KLEE container 가 실행됨을 확인할 수 있습니다.

 

예제

이전 포스트에서 예제로 사용했던 내용을 바탕으로 코드를 작성하였습니다.

2023.09.02 - [Computer/Testing] - Symbolic Execution (심볼릭 실행)

Symbolic Execution (심볼릭 실행)

 

예제 코드

 1 #include
 2 #include
 3 #include
 4
 5 int symbolic_execution_example(int a, int b, int c) {
 6     int x = 0, y = 0, z = 0;
 7
 8     if (a) {
 9         x = -2;
10     }
11
12     if (b < 5) {
13         if (!a && c) {
14             y = 1;
15         }
16         z = 2;
17     }
18
19     assert(x + y + z != 3);
20
21     return (x + y + z);
22 }
23
24 int main(int argc, char** argv) {
25     int a, b, c;
26
27     klee_make_symbolic(&a, sizeof(a), "a");
28     klee_make_symbolic(&b, sizeof(b), "b");
29     klee_make_symbolic(&c, sizeof(c), "c");
30
31     printf("result: %d\n", symbolic_execution_example(a, b, c));
32
33     return 0;
34 }

27 ~ 29 line 은 심볼릭(symbolic) 분석을 수행할 변수를 지정합니다. 이전 포스트에서는 α, β, γ 를 사용하였지만, 예제 코드에서는 편의상 a, b, c 를 사용합니다.

 

컴파일

KLEE는 LLVM 비트코드(bitcode)에서 작동합니다. KLEE로 프로그램을 실행하려면 먼저 clang -emit-llvm을 사용하여 LLVM 비트코드로 컴파일해야 합니다.

$ clang -I ~/klee_src/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone example.c

KLEE의 --optimize 명령줄 옵션으로 활성화할 수 있는 KLEE에 대한 올바른 최적화를 직접 선택했기 때문에 KLEE에 전달되는 비트코드는 최적화되어서는 안 됩니다. 그러나 최신 LLVM 버전(> 5.0)에서는 -O0 zero flag를 사용하면 KLEE가 자체 최적화를 수행하지 못하므로 KLEE용으로 컴파일할 때 사용하지 않아야 합니다. 대신 -O0 -Xclang -disable-O0-optnone을 사용해야 하며, 자세한 내용은 이 이슈를 참조하세요. (from https://klee.github.io/docker/)

컴파일이 끝나면 LLVM 비트코드, example.bc 가 생성됩니다.

 

실행

다음 명령을 이용해 실행할 수 있습니다.

$ klee example.bc

실행하면 아래와 같은 결과를 확인할 수 있습니다.

4개의 경로에 대해 확인을 했고, 총 5개의 테스트 케이스를 생성했다고 알려줍니다. 특히 중단된(partially completed paths) 경로의 수에 대해서도 알려줍니다. KLEE 실행의 출력은 KLEE가 생성한 테스트 케이스가 포함된 디렉토리(이 경우 klee-out-0)입니다. KLEE는 출력 디렉터리의 이름을 klee-out-N으로 지정하며, 여기서 N은 사용 가능한 가장 낮은 숫자입니다(따라서 KLEE를 다시 실행하면 klee-out-1이라는 디렉터리가 생성됩니다). 또한 편의를 위해 이 디렉터리에 대한 klee-last라는 심볼릭 링크도 생성합니다:

 

테스트 케이스 분석

KLEE에서 생성된 테스트 케이스는 확장자가 .ktest인 파일로 작성됩니다. 이러한 파일은 ktest-tool 유틸리티로 읽을 수 있는 바이너리 파일입니다. 위에서 assertion 을 발생한 테스트 케이스를 보여주는 파일(test000004.ktest)을 살펴보겠습니다:

$ ktest-tool ./klee-last/test000004.ktest

위 명령어를 실행하면 아래와 같이 a, b, c 각각에 0, 0, 16843009 로 테스트 케이스가 생성된 것을 확인할 수 있습니다.

 

테스트 케이스 재생 (Replay)

KLEE가 생성한 테스트 케이스를 프로그램에서 직접 실행할 수도 있지만, KLEE는 편리한 replay 라이브러리를 제공하여 klee_make_symbolic 호출을 .ktest 파일에 저장된 값을 입력에 할당하는 함수 호출로 간단히 대체할 수 있습니다.

$ export LD_LIBRARY_PATH=~/klee_build/lib/:$LD_LIBRARY_PATH
$ gcc -I ~/klee_src/include -L ~/klee_build/lib/ example.c -lkleeRuntest

위 명령어를 사용하여 실행 파일(a.out)을 생성합니다. 실행 파일을 수행할 때 KTEST_FILE 변수에 ktest 파일의 경로를 설정합니다. 그러면 다음과 같이 ktest 에 할당되어 있는 a, b, c 값을 이용하여 함수가 수행되는 것을 확인할 수 있습니다.

 

지금까지 Symbolic Execution Engine 중 하나인 KLEE 의 사용법에 대해 알아보았습니다.

 

---

참고 사이트

• KLEE (https://klee.github.io/)
• Docker Docs (https://docs.docker.com/)