심볼릭 동적 실행

Tracer [동적 바이너리 구성 프로그램]

• 개요 : DBI (동적 바이너리 구성) 프로그램
• 기간 : 2017년 3월 ~ 2017년 5월
• 인원 : 1명
• 프로젝트 내용 : 
   Pintool을 활용하여 비밀번호 해킹
   함수 후킹으로 메모장 내용 해킹
• Github Link : https://github.com/HwangSangDu/Tracer

심볼릭 동적 실행이란?

Symbolic 기호
Dynamic 동적인
Execution 실행

원하는 코드 블록에 도달하기 위하여 input값을 symbolic으로 대체합니다.

x,y,z 등의 기호로 된 수식을 풀어내 답을 풀기 위한 대표적인 라이브러리가 Z3, angr 입니다.

ex) f(x,y) = z 를 만족하는 (x,y,z) 를 구하기 위한 tool로서 Z3가 사용되며 컨테이너로는 angr가 사용됩니다.
원하는 경로를 위한 해(solve)를 구하는 도구로 보면 됩니다.

Z3는 pintool과 결부하여 사용하기 좋은 라이브러리입니다.
angr 대신 triton이 쓰이기도 하지만 호환성 문제로  윈도우에서 작동하지 않아 angr을 사용하게 되었습니다.

pintool의 경우 속도가 매우 느리다는 점이 가장 큰 단점입니다.
이를 보완하기 위해서 SMT_Solver와 함께 쓰이기도 한다.
실제 해킹대회에서 상당히 유행했고 관련문제가 많이 나왔습니다.

동적 심볼릭 수행과 심볼릭 수행의 차이점(?)

동적 심볼릭 수행은 (심볼릭 수행 + 콘크리트 수행) 이라고 보면 됩니다.
실제 값(콘크리트 값)과 심볼릭 기호(x,y,z와 같은 기호)를 적절히 섞어 코드 커버리지와 속도를 둘 다 잡기 위한 시도라고 볼 수 있습니다.

Taint 분석은 오염분석으로 입력값이 어느 메모리 영역까지 영향을 미치는지 연구하는 것이라고 보면 됩니다.
특권 계층의 메모리까지 영향을 미친다면 이는 취약성 가능성이 있다고 볼 수 있습니다.

관련 자료

발표자료 : Tracer.pdf

정리자료 : Taint 및 Angr.pptx

Z3 Github : https://github.com/Z3Prover/z3 (빌드 버전도 있습니다)

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

C나 C++은 외부라이버리를 참조해야만 사용가능합니다. Python 사용을 추천드립니다.

Z3 Tutorial : http://rise4fun.com/z3/tutorial

Angr : http://revers3r.tistory.com/424 

Triton : https://triton.quarkslab.com 

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