Z3로 공부하는 SMT Solver, 그리고 CTF

목차 0. 소개 CTF SMT Solver Z3 CTF PROB QnA

소개 Name : 정윤서 NickName : Hanel Age : 18 School : 한국디지털미디어고등학교 Intersts : Reversing, Pwnable Blog : www.han3l.tistory.com Team : …

주의 이 발표는 간단하게 설명합니다. 자신이 SMT Solver의 구현에 관심이 있다면 NP (Non-deterministic Polynomial time) NP-C(Non-deterministic Polynomal time – Complete) Decidable Theory SAT Solver ETC..

CTF CTF ? Capture the flag의 약자 ‘깃발을 잡아라’라는 뜻으로 바이너리 분석이나 취약점 익스를 통해 플래그를 얻을 수 있다. 각 팀마다 서버가 주어질 경우, 상대 팀을 공격하여 플래그를 얻을 수도 있다. CTF 일정은 www.ctftime.org

CTF 요즘 문제 동향 : 웹 < 리버싱 < 포너블 그러면 리버싱에서는 어떤 형태의 문제가 나올까?

CTF 리버싱 악성 프로그램 문제 수학 형태의 분기문이 있는 문제 프로그래밍 능력을 요구하는 문제 Simbolic Excution을 활용하게 끔 하는 문제 ETC..

CTF 이건 사람이 풀 수 있는 수학 문제인가..? 나는 수학을 못하는데.. 심지어 이거 너무 길어.. 아 이걸 어떻게 풀지? : SMT Solver

SMT Solver SAT Solver ? boolean SATistfiability problem 의 약어 수식을 만족하는 값이 존재하는지 찾음 ‘True’ or ‘False’ 임

SMT Solver SMT Solver ? Satisfiability Modulo Theories 의 약자 수식을 만족하는 값이 존재하는지 찾음. 수식을 만족하는 값이 존재할 경우 그 값을 구함. ‘True’ or ‘False’ + 방정식, 부등식 해 구하기 컴퓨터 과학과 수학 분야에서 사용됨.

SMT Solver 는 SAT Solver 가 더욱 발전한 것

지원하는 이론 및 데이터 구조 정수론 실수론 배열 리스트 비트 벡터 Etc.. SMT Solver 지원하는 이론 및 데이터 구조 정수론 실수론 배열 리스트 비트 벡터 Etc.. 종류에 따라서는 문자열 등도 있다.

SMT Solver 식의 표현 x – y > c x + y = c 여기서 x와 y는 미지수, c는 정해져 있는 상수 부등식 또는 방정식, 함수 형태로 표현

SMT Solver SMT Solver 종류 ABSOLVER OPENSMT SMTINTERPOL SMT-RAT SONOLAR YICES Z3 ETC..

Z3 Z3로 하는 이유..? 무언가 익숙한 문법 찾기 쉬운 튜토리얼 문서들 운영체제의 제한성이 없음 4. MIT license ETC..

Z3 미지수 선언 – 정수 Int() Ex) from z3 import * x = Int('x') y = Int('y') solve(x + y > 10, x * y == 20)

Z3 미지수 선언 – 실수 Real() Ex) from z3 import * x = Real('x') y = Real('y') solve(x**2 + y**2 == 5, x**4 == 4 )

Z3 미지수 선언 – 실수 Real() 만약, 내가 소수 5자리 까지만 출력하고 싶다면 set_option(precision=5)

Z3 미지수 선언 – 비트 벡터 BitVec() Ex) from z3 import * x = BitVec(‘x’, 8) y = BitVec(‘y’, 8) solve(x + y*3 == 5, x*7 == 14 )

Z3 그럼 값을 구해달라고 하는 함수는 뭔가요..?

Z3 1. solve() 함수 2. Solver 사용

결국 solve 함수도 내부적으로 Solver를 사용 또한 코드가 길어질 수록 가독성 면에서도 Solver가 훨씬 좋음 Z3 결국 solve 함수도 내부적으로 Solver를 사용 또한 코드가 길어질 수록 가독성 면에서도 Solver가 훨씬 좋음

Z3 Solver Solver() : Solver 객체 생성 함수 add() : 수식을 추가하는 함수 check() : 값이 존재하는지 확인하는 함수 값이 존재하지 않으면 unsat, 값이 존해만 sat 를 반환함 알 수 없을 경우 unknown을 반환. model() : 값이 존재할 경우 값을 구하는 함수 unsat, unknown일 경우 에러를 반환함

Z3 Solver – unknown일 경우 언노운이 뜨는 경우 설명

Z3 Solver – unsat 일 경우

Z3 Solver – sat 일 경우

Z3 Z3 그 외의 함수들 append(), assert_exprs(), insert() : 수식을 추가하는 함수 assertions() : 추가된 수식을 반환하는 함수 push(), pop() : 수식을 넣고 빼고 할 수 있음 reason_unknown() : check() 함수의 반환값이 unknown인 이유를 설 명함 reset() : 추가한 수식을 초기화시키는 함수 Etc..

CTF PROB DEFCON CTF 2016 BABY-RE

CTF PROB Anti Hex-ray patch + Z3 Simbolic Excution

CTF PROB Var[0]부터 var[12]까지 13개의 입력을 받음

CTF PROB CheckSolution 함수에서 숫자를 확인하는 것으로 보임.

CTF PROB CheckSolution 함수에서 숫자를 확인하는 것으로 보임. 하지만 디컴파일 에러가 뜸.

CTF PROB 아이다 매뉴얼을 보면 잘 뜨지 않는 오류라고 함 간간히 보이는 쓰레기 코드 때문에 그런거 같았음.

CTF PROB 그래서 함수 전체를 Undefine 한 후 다시 Code로 변경한 후 함수를 다시 만듬

CTF PROB 디컴파일이 됨. CheckSolution 함수를 보아하니 Z3 참 잘 쓸 자신이 생김

CTF PROB 끝 !

CTF PROB 근데 이거보다 쉬운 방법 없나요?

CTF PROB 2번 방법

CTF PROB angr – symbolic execution Python 모듈임 Shellphish 팀이 제작함 Install : pip install angr

QnA ????

Reference http://argosarch.tistory.com/45 http://xer0s.tistory.com/97 https://z3prover.github.io/api/html/classz3py_1_1_solver.html https://github.com/Z3Prover/z3 https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://kldp.org/node/106972