White Box Testing

SW testing & Fuzzing camp lab3
Dynamic Symbolic Execution

cd lab3-crest/
cd cil
./configure

make

lib/z3/bin의 path export해주기

export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$(pwd)

src폴더에서 make하기

path export하기

export PATH=$PATH:$(pwd)

실행시켜보기

vi triangle.c

vi triangle.crest.c 

z3에서 Symbolic Execution을 계산하여 나온 값을 넣어준다. (CREST_int을 사용하여 받음)

컴파일 시키기.

crestc triangle.crest.c 

최대 100번의 cycle을 돈다.

run_crest ./triangle.crest 100 -pdfs 

다음과 같이 모든 branch를 실행시키는 test case들을 눈으로 확인 할 수 있다.

더 많은 정보는 아래에
https://github.com/ARISE-Handong/crest