Z3

pintool과 결부하여 사용하기 좋은 라이브러리이다.

Z3란 게 SMTsolver로서 사용된다고 한다.

원하는 경로를 위한 해(solve)를 구해주는 툴이라고 보면된다.

핀툴의 경우 속도가 매우 느린데 이 툴을 사용하여 원하는 경로만 볼 수 있다면 분석시간을 많이 단축 시킬 수 있을 것이다.

https://github.com/Z3Prover/z3 

github를 참조하자!

빌드된 버전도 있으니 사용하자!

-->  z3-4.3.2-x64-win.zip

z3실행파일이 생성되며 주요언어를 모두 지원한다.

파이썬을 통해서 하는 게 가장 편할것이다.

인터프리터 언어이기 떄문이다.

C언어나 C++로 하기 위해서는 외부라이버리를 참조해야만 사용가능하다.

angr과 triton은 같이 사용하는 프레임워크이다.

http://rise4fun.com/z3/tutorial

http://xer0s.tistory.com/97

http://revers3r.tistory.com/424 - angr

https://triton.quarkslab.com - triton

http://shell-storm.org/blog/Stack-and-heap-overflow-detection-at-runtime-via-behavior-analysis-and-PIN/

파싱이란? - 가공되지 않은 데이터에서 원하는 특정한 문자열을 빼내는 작업

makefile형식으로 이루어져 있다.