C/Symbolic Execution/KLEE Tutorials 1-2 Anaylsis

# 대상 파일 : ~/klee_src/examples/get_sign/get_sign.c

기호실행을 할 수 있게 해주는 가상 엔진입니다.

소스코드와 함께 헤더파일이 전처리되어 소스를 감싼 후 

기호 실행할 변수를 지정하는 klee_make_symbolic() 함수를 이용해 기호실행을 합니다.

klee_make_symbolic()은 소스 내의 지정할 변수의 주소값, 기호로 다룰 크기, 그 변수를 부를 이름 이렇게 3가지를 인자값으로 사용합니다. 

-  Bllvm 바이너리 생성하는 방법

• clang -I [전처리할 헤더 위치] -emit-llvm -c -g [소스 위치]
• -I는 컴파일러가 klee/klee.h 파일을 찾을 수 있게 하는 옵션이고,
• -g는 디버그 정보를 바이트 코드에 포함시키는 옵셥입니다.
• 최적화를 시키려면 --optimize 옵션을 추가하면 내부적으로 최적화합니다.

- Gcc 바이너리 생성

• clang -I [전처리할 헤더 위치] -emit-gcc -c -g [소스 위치]

- 클레이 실행

• 실행은 아래 명령으로 할 수 있습니다.
• STP 솔버가 backend에서 돌아가, 전체 인스트럭션 수와 발견한 경로 생성한 test케이스를 결과로 내보입니다.
• 결과 파일 : klee-out-x
• 가장 최근 결과는 klee-last에 링크되어 최근 결과를 확인 할 수 있습니다.

- 결과를 분석해보겠습니다.

# 표준 결과 파일

- 제일 처음 assembly.ll은, file 명령으로 확인해본 결과 C 소스 파일이고 컴퓨터가 보기에는 C 소스 파일이지만 어떤 의미를 가지는지 모르므로 내용을 확인해보면,

-  네.. 저도 모르겠습니다. 파싱할 수 있는 데이터들이 있는데 맨 위부터 순서대로 막연한 의미 추론을 해보면 정의(difine, declear), 실행(vector: 방향) 이라는 키워드로 정의하는 부분과 어떤방향으로 실행하는 부분으로 나눠져 있구나를 알 수 있습니다. 정확한 의미를 찾기위해 공식홈페이지 docs(http://klee.github.io/docs/files/)를 찾아보면 assembly.ll파일은 klee가 실행한 llvm 코드를 사람이 읽을 수 있게 해논 파일이라고 합니다. 그렇다면 c 소스가아닌 llvm 코드라는 말이고 llvm 구조를 이해하면 읽을 수 있다는 말입니다. 이걸 읽어서 뭐하냐고 하시겠지만, 직접 읽을려고 하는 건 아니고 파싱할 때 구조 이해가 필요해서 공부 해야할 것 같습니다.

• 사람이 읽을 수 없는 .bc의 llvm 코드를 첨부합니다. 위에서 읽을 수 있다는 의미는 이걸 읽을 수 있게 ASCII로 나타냈다는 말이라고 생각합니다.
• cat get_sign.bc
• 

- .bc로 컴파일을 할때, 디버깅 정보를 포함했기 때문에, 읽을 수 있게 변환해 준것 같습니다.

- warings.txt :  파일 이름 그대로 KLEE말한 경고를 포함하는 파일입니다.

- messages.txt : Klee가 실행을 하면서 내보낸 메시지를 포함한 파일입니다. 열어보면 실행할 때 STP가 백엔드에서 돌아가고 있다고 알려준 라인이 기록되있음을 볼 수 있습니다.

- run.stats : 통계적 정보입니다. klee-stats  tool을 통해 수동 감사가 가능하다고 합니다.  get_sign.bc에 대한 경고는 없어서 기록된 내용이 없습니다.

- runistats : 프로그램의 각 코드라인에 대한 전역 통계 바이너리 파일입니다.

- info : klee가 실행 했을때, 실행에 관련된정보를 포함합니다. 전체적인 실행 시간도 또한 포함합니다.

• 

- 프로세스 ID 115, 시작시간은 2018-01-08 11:45:26 종료시간은 2018-01-8 11:45:26으로 1초도 안되서 실행이 끝났습니다. 사용한 검색 방법은 RandomPathSearcher와 WightedRandomSearcher::CoveringNew 두가지를 사용한 것으로 보입니다. (*klee에 아무 옵션도 주지않고 실행한 결과입니다.) 

• 탐색 경로 = 3
• 평균 구성된 쿼리 = 14 (하나의 기호 실행당 만들어진 쿼리 양을 말하는 것 같습니다.)
• 전체 쿼리 = 3
• 유효 쿼리 = 0
• 무효 쿼리 = 3
• 쿼리 CEX = 3
• 전체 명령어 수  =  31
• 완료된 경로 = 3
• 생성된 테스트 케이스  = 3

- ktest-tool 로 ktest 읽기. 

• --write-ints 는 4bytes의 크기 시퀀스를 정수로 변환하는 옵션입니다.
• ktest-tool --write-ints [.ktest파일]
• 

- 각각의 테스트 마다 어떤 이름의 변수에, 크기가 몇인 무슨 데이터가 들어갔는지 알 수 있습니다.

 위 테스트 3개에선 각각 0, 16843009, -2147483648의 값이 들어 갔습니다. 

- 기호 실행을 하고나서 결과에 경로마다 생성되는 파일들이 있습니다. Per-path files이라 하며, 5가지 정도가 있습니다. 첫번째로는 test<n>.ktest로 경로에 대한 테스트 케이스 파일 입니다. --no-output 옵션으로 테스트파일을 생성하지 않을 수 있습니다. 두번째 파일은 에러 파일입니다. test<n>.<error-type>.err의 형식이며, klee가 찾은 에러를 파일로 떨궈줍니다. 세번째는 test<N>.kquery 파일입니다. KQuery 포맷이며, 주어진 경로에 관련된 제약조건을 포함합니다. 생성을 원한다면 --write-kqueries 옵션을 써서 생성할 수 있습니다. 네번째 파일은 test<N>.cvc 파일입니다.  CVC 포맷으로 주kquery와 동일하게 주어진 경로에 관련된 제약조건을 포함합니다. --write-cvcs 옵션으로 파일을 생성할 수 있습니다. 마지막 5번째 test<N>.smt2 파일입니다. 위 두가지 파일과 동이하게 주어진 경로에 관련된 제약조건을 포함하고 SMT-LIBv2 형식(현재는 버전2) 입니다. --write-smt2s 명령을 통해 생성할 수 있고 거의 .kqeury와 일치하는 정보를 보여줍니다.

• test<N>.ktest : 테스트 케이스 파일
• test<N>.<error-type>err : 에러 파일
• test<N>.kquery : kquery 형식의 경로 제약조건
• test<N>.cvc : cvc 형식의 경로 제약조건
• test<N>.smt2 : smt2 형식의 경로 제약조건

- 이제 경로에 대한 파일을 언급했고 에러의 종류에 대해 말할 수 있을 것 같습니다. test<N>.<error-type>.err 파일로 떨어지는 에러 파일의 에러 종류는 총 7가지가 있습니다. 모든에러가 이범주에 속하는지는 아직까지 모르겠지만 일단 공식 홈페이지(http://klee.gihub.io/tutorials/testing-regex : KLEE error reports )에서 말하는 에러 종류는 7가지가 됩니다.

- ptr 에러는 유효하지않은 메모리 위치가 저장되거나 불러와질 때 발생합니다. 예를 들면 아래서 다룰 함수의 버퍼 포인터가 문자열의 범위를 넘어갔을 때 발생하는 bound of pointer 오류가 여기에 해당한다고 말할 수 있습니다.

- free 에러는 유효하지않은 자원이 해제되거나 두번 해제 됬을때 발생합니다. 동적 할당한 배열의 메모리가 아닌곳을 해제하거나 이를 두번 해제 했을 때 발생한다고 볼 수 있습니다.

- abort 에러는 프로그램이 abort()를 불렀을 때 발생합니다.

- assert : 프로그램에서 assertion이란 말을 잘 모르고 있어 나무 위키의 "표명"이라는 사전을 참고했습니다. (https://ko.wikipedia.org/wiki/%ED%91%9C%EB%AA%85) 한글로 어서션은 프로그램에서 추가하는 참 거짓을 미리 가정하는 문이라고 합니다. 가정을 읽어보면 현재 다루는 프로그램은 klee이고 klee가 미리 참 거짓을 가정하는 문이 가정에 실패했을 떄 발생하는 에러라고 볼 수 있습니다. 또하나의 가정을 둔다면 기호 실행중인 프로그램 안에서 발생하는 assertion failure로 볼 수도 있습니다. 저는 전자를 가정에 두고 에러를 정의하고자 합니다. klee는 klee_assume() 내장 함수를 통해서 기호 변수를  가정할 수 있습니다. 에러고치기(1)에 klee_assume(re[SIZE - 1] == '\0');를 정의하는 것을 예로 들 수 있습니다.

- div 에러는 0으로 나눌 때 발생하는 에러입니다.

- user 에러는 사용자가 klee를 사용할때 문제가 발생한 에러입니다.

- exec 에러는 예로 정의되지않은 명령어, 유효하지않은 함수 포인터로 부터의 호출이나

인라인 어셈블리와 같은 실행중인 프로그램으로 부터 Klee이 멈추는 문제입니다.

- model 에러는 Klee가 프로그램 공간을 탐색하는데 정확성을 유지할 수 없을 때 발생합니다.

예로 동적할당한 기호 크기는 현재 지원되지 않는 경우 Klee는 인자를 구체화 합니다.

- 에러 고치기 (1)

• 

- 오류 파일은 klee폴더 내에 examples/regexp/Regexp.bc를 기호 실행한 결과로 떨어진 파일입니다. 파일이름은 test000010.ptr.err와 test000011.ptr.err입니다. cat 명령으로 내용을 출력했을때 re의 주소값에서 1만큼 떨어진 곳에 오류가 발생했음을 알 수 있습니다.

• 문자열 끝을 '\0'으로 인식하는 함수를 만났을 때, klee의 기호 입력값의 끝에 '\0'이 없어 문자열 포인터 범위를 벗어나는 문제.
• klee_assume 함수를 이용해 고침.
• 단일 인자(unsigned int)를 가져갑니다. (현재 경로를 가정하는것)
• 문제가되는 소스

1 2 3 4 5 6 7 8 9 10 11 12 13

int main() {   // The input regular expression.   char re[SIZE];     // Make the input symbolic.   klee_make_symbolic(re, sizeof re, "re");     // Try to match against a constant string "hello".   match(re, "hello");     return 0; } Colored by Color Scripter

cs

- 출처는 klee.github.io/tutorials/testing-regex/이며, re 문자 배열에 사이즈를 가정하면 해결할 수 있습니다. 

간단하게 klee_assume(re[SIZE - 1] == '\0');를 추가하여 끝을 의미하는

SIZE -1 번호의 배열 값은 항상 '\0'이다 라고 가정해줍니다.