z3_and_angr_binary_analysis_workshop
1.0.0
원래 Sail Brown이 Steelcon and Hack.lu 2018에서 제공 한이 건물은 3 시간 동안의 이진 분석을 위해 Z3 및 AngR을 사용하는 참석자들을 소개하는 3 시간의 워크샵이었습니다. 워크숍은 SMT 솔버, Z3 SMT 솔버 및 파이썬 라이브러리 및 ANGR BINAGE 분석 프레임 워크에 대한 소개를 제공했습니다.
보안 연구원들이 역 엔지니어링 및 취약성 연구를 수행하는 데 도움이되는 기술의 잠재적 응용 프로그램을 입증하기위한 워크샵 연습이 제공되었습니다.
슬라이드는 내용에 대한 대략적인 안내서와 연습을 시도 할 주문을 제공합니다.
| 이름 | 유형 | 설명 |
|---|---|---|
| 퀸즈 | 예 | '퀸즈는 어떻게 NXN 체스 보드에 배치하여 두 사람이 서로를 공격 할 수 없습니까?' Z3을 사용하여 N * N Chessboard 용 솔루션을 생성합니다. |
| Hackvent 15 | 예 | 솔루션 및 Z3로 Hackvent 15 CTF 챌린지를 해결하기 위해 걸어갑니다. |
| 스도쿠 | 운동 | Z3을 사용하여 스도쿠를 해결하십시오 |
| rng | 운동 | 선택적 연습 - Z3을 사용하여 비 암호화 적으로 안전한 임의 번호 생성기 종자 값을 찾습니다. |
| x86 | 50/50 | 절반 예제, 반 DIY- Z3를 사용하여 X86 지침의 Simiplifified 버전 구현 |
| 불투명 한 곤경 | 운동 | 이전에 구현 된 지침을 사용하여 소규모 조립 지침에서 불투명 한 사전 진치사를 식별하십시오. |
| 동등성 점검 | 예 | 이전에 구현 된 지침을 사용하여 동등한 지침 시퀀스를 식별합니다. |
| 이름 | 유형 | 설명 |
|---|---|---|
| opaque_predicates | 예 | ANGR을 사용하여 불투명 한 작업이 훨씬 적은 일을 식별합니다. :) |
| ioctls | 예 | ANGR을 사용하여 Windows 드라이버 IOCTL 코드를 식별하십시오 |
| 안녕하세요 세계 | 50/50 | ANGR을 사용하여 간단한 '라이센스 키 검증기'에 대한 유효한 인수를 생성하는 데 대한 연습 및 연습 |
| 폭탄 실험실 | 운동 | '폭탄 실험실'을 해결하기 위해 angr을 사용한 DIY 운동 |
모든 코드는 Python3에 있으며 ANGR BINAGE 분석 프레임 워크 만 설치하면됩니다.
mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr
