C/Symbolic Execution/KLEE Reference

++ 2018-02-6 변경사항 ++

- docker 컨테이너 내의 파일 빼오기

- docker 컨테이너 volume의 위치를 확인

※발음 - 클레이, 클레

※ LLVM - Loew Level Virtual Machine

• clang을 사용

# 출처 : [KLEE Documentation] http://klee.github.io/docs/

# [Part : Docker] 영구적 컨테이너 설정

- docker 상에 임시적으로 띄우는 컨테이너를 영구적으로 유지시킵니다.

• docker run -ti -name=[컨테이너 이름] --ulimit='stack=-1:=1' klee/klee
• --rm 옵션을 사용하지 않으면 컨테이너가 종료될 때 컨테이너가 사라지지 않습니다.
• --volume 옵션을 통해 docker run을 통해 마운트시킨 컨테이너의 호스트 시스템 상 크기를 측정할 수 있습니다.

# [Part : KLEE ] KLEE 실행 옵션

• full command : klee --libc=uclibc --posix-runtime test.bc

# Docker로 klee를 설치하지 않았을 때

- klee 홈페이지에서 제공하는 building klee 를 참고하여 KLEE의 의존성을 해결하고 자신의 OS 시스템에 KLEE를 빌드시켜야 합니다. 저는 Docker로 klee를 사용해서 이 방법을 쓰지는 않았습니다. 

• http://klee.github.io/build-llvm34/

# Solver Chain - http://klee.github.io/docs/solver-chain/#the-solver-chain

- 커맨드라인에 관련된 solver chain 설명입니다. klee는 klee나 kleaver둘 다 공유 할 수 있는 solver chain 제어 커맨드라인 옵션을 제공합니다. 이 solver chain은 디자인 패턴 decorator를 사용하여 내부적으로 수행됩니다. solver query가 질의될 때 중첩된 solver 스택을 탐색하고 마지막에 SMT solver(핵심 solver)를 호출합니다. 

• solver chain은 constructSolverChain()함수로 생성할 수 있습니다.

# Core solver 

- solver는 -solver-backend 옵션을 통해서 선택할 수 있습니다.

• MetaSMT : -solver-backend=metasm 옵션을 사용합니다.
  http://www.informatik.uni-bremen.de/agra/eng/metasmt.php
• 추가적인 옵션 :
  -metasmt-backend=<backend>
• metasmt의 백엔드 솔버를 결정합니다.
• stp
• z3
• btor (Boolector)
• Z3 sovler는 API를 통해서 직접 사용 가능합니다.
• -use-construct-hash-metasmt
• 재사용을 위해 조건식을 캐싱합니다.

• STP : Simple Theorem Prover의 약자입니다. -solver-backend=stp로 사용합니다.
  http://stp.github.io/
• 추가적인 옵션 : 
  -debug-dump-stp-queries (기본값 : false) : 값이 True이면 STP solver가 질의를 받을 때 자신이 가지는 형식 그대로의 표준 에러를 출력합니다.
  -ignore-solver-failures (기본값 : false) : 값이 True이면 예상치 못한 sovler 실패를 무시합니다.
  -use-construct-hash (기본값 : true) : 값이 true이면 구성된 STP표현식은 재사용을 위해 캐싱합니다.

• Z3 : -solver-backend=z3 옵션으로 사용합니다.
• 추가적인 옵션 : 
  -debug-z3-dump-queries=<path> : 모든쿼리가 전달 Z3에 전달될 때마다 SMT-LIBv2 형식으로 <path>에 로그를 남깁니다.
  -debug-z3-log-api-interaction=<path> : C API 호출이 발생하면 <path>에 로그를 남깁니다. log는 -log 옵션을 사용한 Z3 binary를 이용해 다시 실행할 수 있습니다.
  - debug-z3-validate-models (기본값 : false) :  값이 True이면, Z3 모델은 만족되는 모든 쿼리를 Z3 표현식으로 대체합니다.  Z3 자신의 제약 조건 언어를 Z3가 제공한 모델이 만족하는지 체크합니다.  모델이 제약조건 제약조건을 만족하지 않는다면,  실패에 대한 표준 에러가 출력되고 abort()함수가 호출됩니다. Z3만의 제약조건 언어를 만족하도록하는 Z3 모델은 KLEE 만의 표현식 언어로 대체될 때 모델이 만족스럽다는것을 의미하지 않습니다. Z3와 KLEE 표현식 간의 의도치않은 의미적인 불일치가 있는 경우 발생합니다. KLEE 제약조건 언어를 만족하는지 검사를 위해서 -debug-assignment-validating-solver를 사용합니다.
  -debug-z3-verbosity=<N>(기본값 : true) : 값이 true 일때 구성된 Z3 표현식은 재사용을 위해 캐싱합니다.

- 공통적인 solver 옵션

• -solver-optimize-divides : MetaSMT와 STP만 영향을 받습니다. 값이 True일 때 solver에 표현식을 주기전 최적화합니다.
• -use-forked-solver(기본값 : true) : MetaSMT와 STP만 영향을 받습니다. 값이 True일 때 klee/kleaver 프로세스로 부터 분리된 프로세스를 생성합니다. false일 때 klee/kleaver 프로세스안에 solver가 생성됩니다.

# Caching Solvers

- 중복을 피하기위해서 이전 쿼리 또는 그 쿼리에 반대되는 반례를 캐싱합니다. 쿼리는 적중률을 높이기위해 정규화됩니다.

• -use-cex-cache 옵션을 통해 사용됩니다.

# Independence solver

- 질의를 독립적인 제약조건으로 나누고 독립적으로 각각의 solver를 호출합니다.

• -use-independent-solver 옵션을 통해 사용합니다.

# Debugging solvers

- Assginment 검증 solver :  표현식으로 대체된 쿼리가 결과에 적당한지 체크합니다. 이것은 KLEE의 제약조건 언어와 핵심 sovler의 일관성을 검사할 때 유용합니다. 이 옵션은 -debug-assignment-validating-solver를 통해 사용합니다.

- 디버그 검증 sovler :  이 솔버는 디버깅을 위한 것이며, 현재 빌드가 assertion이 가능하다면 유용합니다. -debug-validate-solver 옵션을 통해 사용합니다. 

- 쿼리 로깅 sovler :

# KLEE 옵션

- klee를 실행할 때 옵션으로 줄 수 있는 인자들에 대해서 설명합니다. 

• 기호 실행 환경 옵션
• -sym-arg <N> - 길이 N의 인자로 대체합니다.
• -sym-args <MIN> <MAX> <N> - 각각 최대 길이 N으로 최소 길이 N과 최대 길이 N을 정의합니다.
• -sym-files <NUM> <N> - (표준 입력을 제외한) 각각 N 크기의 기호 파일('A','B','C' 등)을 생성합니다.
• -sym-stdin <N> - N 크기의 표준입력 기호를 생성합니다.
• -sym-stdout - 표준 출력 기호를 생성합니다.
• -save-all-writes - (기본값=on) 파일 크기를 초과할지라도 명령이 예상대로 실행되도록 쓰기를 허용합니다.
• -max-fail <N> - 최대 N회의 삽입된 실패를 허용합니다.
• -fd-fail - -max-fail 1 에 대한 단축키를 지정합니다. (?)
• 탐색 방법
• Depth-First Search (DFS): 분기 수가 깊어질 수록 우선 탐색을 합니다.
• Random State Search: 탐색 상태를 랜덤으로 선택합니다.
• Random Path Selection: 다소 복잡한 프로그램에서 사용되는 높은 커버리지 테스트를 위한 탐색 방법 입니다.
• http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf
• Non Uniform Random Search (NURS): 주어진 구분점에 따라 랜덤으로 상태를 선택합니다. 밝혀진 명령어의 최소 거리(minimum distance to an uncovered instruction : MD2U)를 기준으로 합니다.
• 옵션 : --search=[인자]
• 인자값
• dfs
• random-state
• random-path
• nurs 탐색은 Non Uniform Random Search을 의미합니다.
• nurs:covnew 
• nurs:md2u
• nurs:depth
• nurs:icnt
• nurs:cpicnt
• nurs:qc
• 탐색은 라운드 로빈을 통해서 돌아가면서 쓰여질 수 있습니다. 중복적으로 사용하기위해 --search 옵션을 사용하는 복수 탐색 만큼 사용하면됩니다.
• ex)
  klee --search=random-state --search=nurs:md2u demo.o
• 진입점 지정
• -entry-point=함수명 : 해당 함수명이 실행의 시작점으로 사용됩니다.
• klee-assume 옵션
• 기본적으로 KLEE는 가정된 조건이 실행이 불가능할 경우 오류 보고를 합니다. -silent-klee-assume 옵션으로 현재 경로 탐색의 자동 종료를 지정할  수 있습니다.
• 통계
• 기본적으로 KLEE는 코드 탐색에 관련한 통계를 포함하는 두개의 파일을 생성합니다.
• run.stats : KLEE에서 산출한 다양한 통계를 포함하는 이 텍스트 파일은 수동으로 klee-stats를 통해서 수동으로 감사할 수 있습니다.
• run.istats : 프로그램의 각 코드 행에 대해 KLEE가 산출한 전역 통계를 포함한 Callgrind 형식의 텍스트 파일입니다. 파일은 읽을 수 있어 프론트 엔드에서 감사를 할 수 있습니다.
• -stats - 통계를 사용합니다. (기본값:on)
• -output-stats - 실행중인 통계 추적파일 작성 (기본값:on)
• -output-istats - callgrind 형식의 명령어 레벨 통계를 작성 (기본값:on)
• -stats-write-interval=TIME - stat 기록의 대략적인 간격을 설정합니다. (기본값:1초)
• -istats-write-interval=TIME -istat 기록에 대략적인 간격을 설정합니다. (기본값=10초)
• -stats-write-after-instructions=N - 각각 N개의 명령어 후에 stat를 기록합니다. 0은 비활성화 입니다. (기본값:0)
• -istats-write-after-instructions=N - 각각 N개의 명령어 후에 istat를 기록합니다. 0은 비활성화 입니다. (기본값:0)
• 디버깅
• -debug-print-instructions=FORMAT - KLEE에 의해서 실행된 LLVM 명령어를 로깅합니다. (기본값:off)
• (src) : 소스코드 파일, 라인
• (inst_id) : KLEE에 의해 할당된 명령어 식별자
• (llvm_inst) : 디버깅 정보를 가진 LLVM 명령어
• =all:stderr - [src, inst_id, llvm_inst] 형식으로 모든 명령어를 표준 에러에 기록
• =src:stderr - [src, inst_id] 형식으로 모든 명령어를 표준 에러에 기록
• =compact:stderr - [inst_id] 형식으로 모든 에러를 표준 에러에 기록
• =all:file -  [src, instd_id, llvm_inst] 형식으로 모든 명령어를 instruction.txt에 기록
• =src:file -  [src, inst_id] 형식으로 모든 명령어를 instruction.txt에 기록
• =compact:file - [inst_id] 형식으로 모든 명령어를 instruction.txt에 기록
• -debug-compress-instructions - instructions.txt를 압축합니다. (기본값:off)
• 메모리 관리
• KLEE는 명시적으로 메모리 관리 호출(like malloc() and free())을 차단하고 존재하는 메모리 할당자에게 보냅니다. 이러한 행동을 바꾸기위해 아래 옵션을 사용합니다.
• --allocate-determ - 실행된 응용프로그램에 대해 메모리를 결정적으로 할당하도록 지원합니다. (기본값:off)
• --allocate-determ-size - 할당 결정을 위해 특정 크기의 버퍼는 미리 MB 안에 할 당됩니다. (기본값:100)
• --allocate-determ-start-addres - 미리 할당된 메모리의 요구되는 시작주소를 제어합니다. 이 주소는 페이지 할당이 될 수 있습니다. null이 제공된다면, 메모리는 임의의 주소로 매핑됩니다.
• --return-null-on-zero-malloc - 크기 인자가 0인 경우 NULL 포인터를 반환해야하는지 제어합니다. (기본값:off)
• --red-zone-space - 인접한 두 공간에 사용되지 않은 공간을 바이트 단위로 제어합니다. (기본값=10)
• 종료 이벤트 생성
• KLEE는 기본적으로 분석하는 응용프로그램에서 버그를 찾는다해도 종료하지 않습니다. 반면에 KLEE는 암시적으로 일부 실패를 종료합니다. 
• -exit-on-error : 임의의 첫 에러에 종료합니다.
• -exit-on-error-type=[Type]
• =Abort - 크래시 났을 때
• =Assert - Assertion을 만났을 때
• =Exec - 예상하지 못한 명령어를 실행하려 시도할 때
• =External - 외부 객체를 참조했을 때
• =Free - 유효하지않은 메모리를 해제했을 때
• =Model - 메모리 모델 제한점을 만났을 때
• =Overflow - 오버플로우가 발생했을 때
• =Ptr - 포인터 에러
• =ReadOnly - 읽기 전용에 쓰기 했을 때
• =ReportError - klee_report_error함수가 불러와졌을 때
• =User - 잘못된 klee 함수가 쓰여졌을때 (klee_*)
• =Unhandled - 다루지않는 함수를 만났을 때
• -ignore-solver-failures - solver 실패에도 종료되지 못하게 합니다.
• 외부 라이브러리 링크
• 주어진 파일에 정의되지 않은 함수를 -link-llvm-lib 옵션을 사용해 정의합니다.
• 입력 파일안에 몇가지 함수가 외부 LLVM IR 파일에 정의되어 있다면, LLVM IR 파일의 .a 또는 LLVM IR 코드와 공유된 객체, 외부 파일은 -link-llvm-lib=LIB_FiLENAME을 사용해 링크될 수 있습니다.

# Instrinsic 정리 (내장 함수)

- 내장함수는 include/klee/klee.h 에 선언되어 있습니다. 

• klee_assume(condition) : 기호 변수가 취할 수 있는 값을 제한하는데 사용합니다. 개념적으로 if(condition) { } 문과 동일합니다.  기술적으로 klee_assume(condition)은 현재 경로에 제약조건을 추가합니다.
• klee_prefer_cex(object, condition) : 이 함수는 결과로 testcase를 생성할 때 특정 값을 선호하겠다고 제시합니다. KLEE 상태는 다양하고 가능한 테스트 케이스에 해당할 수 있습니다.
• 테스트케이스를 생성할 때 테스트 케이스 안에 기호 데이터는 임의로 생성되어 입력됩니다. 이때 임의로 생성되는 제약 조건을 설정할 수 있습니다.
• klee_make_symbolic 함수 이후 klee_prefer_cex를 사용합니다.
• ex)

1 2

for (int i = 0; i < 4; i++)   klee_prefer_cex(input, 32 <= input[i] && input[i] <= 126); // assume ASCII

cs

# docker 컨테이너 안의 파일 빼오기

- docker cp <컨테이너ID>:/파일/디렉토리/경로 /호스트/디렉토리/경로

# docker 컨테이너 volume의 위치를 확인

- sudo docker inspect [컨테이너 이름] 으로 확인할 수 있습니다.