2022 05 21

2022-05-21¶

Basics of VIM¶

:set number : 줄 번호 보여주기
dd : 커맨드 모드에서 한 줄 지우기
u : undo
ctrl + r : redo
/search-string : 해당 파일에서 search-string에 해당하는 첫 위치 보여줌
:%s/from-string/to-string : from-string을 to-string으로 첫 위치에 있는거 바꿔주세요
:%s/from-string/to-string/g : from-string을 to-string으로 모두 싹 다 바꿔주세요

KLEE¶

참고: https://klee.github.io/tutorials/testing-function/
참고: https://klee.github.io/tutorials/testing-regex/
Input을 Symbolic으로 바꾸기
- KLEE로 함수를 테스트하기 위해서는 symbolic input으로 돌려야 해
- 변수를 symbolic하게 만들기 위해선 klee_make_symbolic() 함수를 사용해야해
  - 세가지 변수를 받음
    1. 변수의 주소
    2. 변수의 사이즈
    3. 변수의 이름
- 아래 예시와 같이 a를 symbolic으로 만들어 get_sign() 에서 symbolic input으로 사용하도록 할 수 있음
```
int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}
```

Compiling to LLVM bitcode
- KLEE는 LLVM bitcode에서 수행됨
- clang -emit-llvm을 활용하여 LLVM bitcode를 만들자
- clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c
  - -I : 컴파일러가 klee/klee.h를 찾을 수 있게
  - -g : 비트코드 파일 디버그 가능토록
  - --optimize : 최적화 가능하도록
- 그냥 디버그랑 최적화 신경 안쓴다면 clang -emit-llvm -c get_sign.c로도 충분

Running KLEE
- bitcode 파일을 KLEE에서 돌리는 법...
  - 커맨드 : klee get_sign.bc
  - 결과물
```
KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3
```
    - KLEE가 3개의 path를 다녀오셨음 (해당 예시는 3개면 다 한거)
      - 프로그램 크다면, 각 path 시간상, 메모리상 다 돌진 못했을 수도
      - 이렇다면 인터럽트가 몇개의 path에서 발생했는지 기록해둠
    - 이번엔 "klee-out-0"이라는 결과물 디렉토리를 봅시다
      - 해당 디렉토리에 KLEE가 만들어낸 테스트 케이스를 보여줌

Executing the code with KLEE
- klee --only-output-states-covering-new Regexp.bc
- 중간 중간 중요한 이벤트가 발생한다면, 상태를 출력해줌.
  - 가령 invalid memory access
- --only-output-states-covering-new 옵션을 통해서 테스트를 돌리면 새롭게 커버되는 코드에 대한 테스트만 써줌
  - 이 옵션이 없다면 모든 path에 대한 테스트는 아니라도 많은 path에 대한 테스트 만들어줌
    - 전부다가 아닌 이유는, 에러 하나 발견하면 그 path에 대한 실패테스트 케이스는 한개만 놔둠
    - --emit-all-errors 옵션으로 모두 다 케이스 돌릴 수 있긴 함

KLEE-generated test cases

KLEE가 생성한 Test Case는 .ktest 확장자 가짐

ktest-tool을 통해 테스트 볼 수 있음

$ ktest-tool klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

KLEE error reports
- KLEE가 detect하는 에러는 다음과 같음
  - ptr : Invalid memory 주소에 대해 store/load
  - free : double free/invalid free
  - abort : 프로그램이 abort() 실행
  - assert : assertion 실패
  - div : 0으로 나눔
  - user : 유저 인풋이 파토남
  - exec : unknown instruction
  - model : full precision 못지킴

Changing the test harness

KLEE가 Regex 라이브러리에 대해 많은 에러를 찾은 이유는,
- regex function에 버그가 있어서가 아닌, 테스트 드라이버가 문제 있어서
- regex buffer를 symbolic하게 만들고 있지만, match function은 null로 끝나는 string이길 바람

해결책은 다음과 같이 \0을 그냥 char array에 박아버리는 방법과

int main() {
    // The input regular expression.
    char re[SIZE];

    // Make the input symbolic.
    klee_make_symbolic(re, sizeof re, "re");
    re[SIZE - 1] = '\0';

    // Try to match against a constant string "hello".
    match(re, "hello");

    return 0;
}

klee_assume을 활용하는 것

assertion을 하나 더해서 match 함수 넘어가지 않게

int main() {
    // The input regular expression.
    char re[SIZE];

    // Make the input symbolic.
    klee_make_symbolic(re, sizeof re, "re");
    klee_assume(re[SIZE - 1] == '\0');

    // Try to match against a constant string "hello".
    match(re, "hello");

    return 0;
}