Concolic Testing(Concrete + Symbolic : https://en.wikipedia.org/wiki/Concolic_testing)를 지원하는 오픈소스 프로젝트를 찾다 klee란 프로그램을 찾았다. (CREST란 것도 있다.) LLVM(http://llvm.org/)을 사용하여, 좀 더 정확한 분석을 수행하며, 홈페이지에서 제공하는 튜토리얼(https://klee.github.io/)을 진행해보았다.
1. klee 설치
리눅스 머신에 klee를 직접 설치하는 방법도 있지만, 얼마 전에 docker(https://www.docker.com/)를 설치하였기에 해당 이미지가 있는지 검색해 보았다. Linux가 아니라, Mac 또는 Windows를 사용하고 있다면, Docker Toolbox(https://www.docker.com/products/docker-toolbox)를 사용할 수 있다.(현재 Windows 10을 사용하고 있다.)
docker search klee
klee를 사용할 수 있는 docker 이미지들이 있었으며, 이 중 klee/klee 를 설치하였다.
docker pull klee/klee
klee/klee 이미지를 다 받았다면, container를 하나 실행해 보자. 이름은 klee_test 라고 지었으며, stack=-1:-1 옵션을 주어 container에서 stack 크기를 무제한으로 설정하였다.
docker run -i -t --name klee_test --ulimit='stack=-1:-1' klee/klee /bin/bash
container가 실행되었다. 간단한 명령을 주어 container가 실행됨을 확인한다.
설치된, klee 와 llvm의 버전을 확인해 보자.
klee --version
clang --version
2. 예제 구동
2.1. 예제 파일
아래의 예제(divbyzero.c)를 사용한다. 일부러 0으로 나누기 연산을 하도록 만들었다.
#include#include int divide(int a, int b) { if ( b > 0 ) return a % b; else return a % b * -1; } int main(int argn, char *argv[]) { int a; int b; int c; klee_make_symbolic(&a, sizeof(a), "a"); klee_make_symbolic(&b, sizeof(b), "b"); c = divide(a, b); return c; }
18 ~ 19 Line : Symbolic 분석을 수행할 변수를 지정해준다.
klee_make_symbolic
* 첫 번째 인자 : 대상 변수
* 두 번째 인자 : 대상 변수 크기
* 세 번째 인자 : Symbol의 이름
2.2. 컴파일
clang -I ~/klee_src/include/ -emit-llvm -c -g divbyzero.c
컴파일이 끝나면 llvm 상에서 동작할 수 있는 divbyzero.bc 파일이 생성된다.
2.3. 분석
klee 명령어로 분석을 수행한다.
klee --libc=uclibc --posix-runtime divbyzero.bc
--libc 명령이 없이 libc 함수를 사용하면 제대로 인식을 못할 때가 있다.
KLEE: ERROR: /home/klee/work/divbyzero/divbyzero.c:7: divide by zero
0으로 나누기 오류가 발생하였음을 알 수가 있다.
2.4. 테스트 케이스 분석
klee로 분석이 완료되면, 분석 횟수에 따라 하부에 klee-out-N 의 폴더가 생긴다. N에 수행한 횟수만큼 숫자가 증가한다. 가장 최신에 수행한 결과는 klee-last로 접근할 수 있다. 해당 폴더에는 아래와 같은 파일들이 있다.
일단 test로 시작하고, 확장자가 ktest 파일들은 테스트 케이스 파일들이다. 만약 뒤에 err로 끝나는 파일이 있다면, 해당 테스트 케이스를 수행하다 오류가 발생했다는 것을 알 수 있다. 0으로 나누기 오류가 발생한 테스트 케이스가 1번임을 알 수 있다.
테스트 케이스의 상세정보를 확인하려면, ktest-tool 명령어를 사용한다.
ktest_tool klee-last/test000001.ktest
Symbol b의 값이 0으로 설정된 테스트 케이스임을 알 수 있다.
다른 테스트 케이스의 내용도 확인해보자.
