Z3 은 Microsoft에서 개발한 수식 해석 도구로 방정식과 같은 수학적인 요소들의 해결을 가능하게 해준다. Binary Analysis에 대한 부분도 Z3이 많이 사용 되는데 Pin과 함깨 Concolic Execution이 가능하게 해준다거나 Valgrind의 output을 Z3으로 처리를 해주는 등의 작업을 해줄수 있다.
설치과정은 아래 링크를 참조하면 쉽게 할 수 있으니 생략하고..
https://github.com/Z3Prover/z3
간단한 예제들을 봐보자.
z3의 Int라는 함수를 이용해 변수 x와 y를 만들어 주고 solve라는 함수에 조건을 줘서 방정식을 해결해준 모습이다.
>>> from z3 import * >>> x = Int('x') >>> y = Int('y') >>> solve(x>2, y<10, x+2*y==7) [y = 0, x = 7] |
아래처럼 expression 들에 대한 traversing도 가능하다
>>> n = x+y>=3 >>> n.num_args() 2 >>> n.children() [x + y, 3] >>> n.arg(0) x + y >>> n.decl() >= |
아래는 실수 집합에 대한 수를 정의한후 set_option()이라는 함수를 이용해 추가적인 조건을 줘 값을 출력하는 예제이다 precision에 30을 설정함으로써 소수점 30째자리까지 결과값이 출력이 되도록 해주었다.
>>> x = Real('x') >>> y = Real('y') >>> solve(x**2+y**2==3, x**3==2) [x = 1.2599210498?, y = -1.1885280594?] >>> set_option(precision=30) >>> solve(x**2+y**2==3, x**3==2) [x = 1.259921049894873164767210607278?, y = -1.188528059421316533710369365015?] |
이제 Z3의 핵심이자 Binary Analysis에서 가장 많이 쓰이는 Solver에 관해서 알아 볼탠데 위의 예제에서 사용했던 solve()함수는 이 Solver을 이용한 함수이다. Z3은 다양한 Solver를 제공하는데 다음 예를 봐보자.
>>> x = Int('x') >>> y = Int('y') >>> s = Solver() >>> s [] >>> s.add(x>10, y==x+2) >>> s [x > 10, y == x + 2] >>> s.check() sat >>> s.push() >>> s.add(y<11) >>> s [x > 10, y == x + 2, y < 11] >>> s.check() unsat >>> s.pop() >>> s [x > 10, y == x + 2] >>> s.check() sat |
Solver()로 기본 solver를 생성하고 add()를 통해 수식들을 추가해 줄 수 있다. 그 뒤 check()라는 함수를 통해 solution이 발견되었을 경우 sat(satisfiable)라는 출력 값을, solution이 발견되지 않았을경우 unsat(unsatisfiable)라는 출력 값을 내뱉는다. push()나 pop()을 이용해서는 solver에 수식을 추가로 더해주거나 뺄수 있다.
아래 예제와 같이 다양한 메소드를 활용해 가독성을 넓힐 수 도 있다.
>>> x, y, z = Reals('x y z') >>> s = Solver() >>> s.add(x>1, y>1, x+y>3, z-x<10) >>> s.check() sat >>> m = s.model() >>> for d in m.decls(): ... print "%s = %s" %(d.name(), m[d]) ... z = 0 y = 2 x = 2 |
Z3에서는 비트 단위를 이용하여 데이터를 표현하는 방식인 비트백터도 사용을 할 수 가 있다. 바로 예제를 살펴보자.
>>> x = BitVec('x', 16) >>> y = BitVec('y', 16) >>> simplify(x+y-1) 65535 + x + y >>> a = BitVecVal(-1, 16) >>> b = BitVecVal(65535, 16) >>> simplify(a==b) True |
BitVec()을 통해 16bit크기의 변수를 선언해줬다. 3번째 줄의 simplify를 수행했을때 16bit에서 -1은 65535임을 알 수 있다.
지금까지 알아본 내용들을 이용하여 Olympic CTF 2014 Welcome To Forensics 문제의 일부를 풀어보자.
eval('FUNCTION FUNCTI0N($PARAMETER) { /* ' OMFG A FUNCTION !!! */ IF (STRLEN($PARAMETER) <> 16): RETURN FALSE; ENDIF; DIM; $ARRAY = ARRAY(); FOR ($I = 1; $I <= STRLEN($PARAMETER); $I++): $ARRAY[$I] = ORD(SUBSTR($PARAMETER, $I - 1, 1)); ENDFOR; IF ((($ARRAY[3] * $ARRAY[6]) ^ ($ARRAY[2] * $ARRAY[2])) - 7320): RETURN FALSE; ENDIF; IF ((($ARRAY[11] * $ARRAY[14]) ^ ($ARRAY[9] * $ARRAY[11])) - 15882): RETURN FALSE; ENDIF; IF ((($ARRAY[14] * $ARRAY[15]) ^ ($ARRAY[11] * $ARRAY[4])) - 11789): RETURN FALSE; ENDIF; IF ((($ARRAY[1] * $ARRAY[9]) ^ ($ARRAY[8] * $ARRAY[9])) - 7184): RETURN FALSE; ENDIF; IF ((($ARRAY[13] * $ARRAY[16]) ^ ($ARRAY[7] * $ARRAY[11])) - 10366): RETURN FALSE; ENDIF; IF ((($ARRAY[9] * $ARRAY[4]) ^ ($ARRAY[4] * $ARRAY[2])) - 6902): RETURN FALSE; ENDIF; IF ((($ARRAY[13] * $ARRAY[15]) ^ ($ARRAY[11] * $ARRAY[16]))): RETURN FALSE; ENDIF; IF ((($ARRAY[14] * $ARRAY[6]) ^ ($ARRAY[6] * $ARRAY[1])) - 2277): RETURN FALSE; ENDIF; IF ((($ARRAY[10] * $ARRAY[9]) ^ ($ARRAY[16] * $ARRAY[15])) - 4385): RETURN FALSE; ENDIF; IF ((($ARRAY[2] * $ARRAY[7]) ^ ($ARRAY[1] * $ARRAY[10])) - 15468): RETURN FALSE; ENDIF; IF ((($ARRAY[3] * $ARRAY[14]) ^ ($ARRAY[6] * $ARRAY[15])) - 8075): RETURN FALSE; ENDIF; IF ((($ARRAY[6] * $ARRAY[3]) ^ ($ARRAY[5] * $ARRAY[10])) - 11550): RETURN FALSE; ENDIF; IF ((($ARRAY[5] * $ARRAY[3]) ^ ($ARRAY[9] * $ARRAY[8])) - 7668): RETURN FALSE; ENDIF; IF ((($ARRAY[13] * $ARRAY[12]) ^ ($ARRAY[12] * $ARRAY[1])) - 3032): RETURN FALSE; ENDIF; IF ((($ARRAY[7] * $ARRAY[4]) ^ ($ARRAY[8] * $ARRAY[13])) - 14067): RETURN FALSE; ENDIF; IF ((($ARRAY[6] * $ARRAY[3]) ^ ($ARRAY[7] * $ARRAY[7])) - 11997): RETURN FALSE; ENDIF; IF ((($ARRAY[12] * $ARRAY[11]) ^ ($ARRAY[5] * $ARRAY[8])) - 13208): RETURN FALSE; ENDIF; IF ((($ARRAY[5] * $ARRAY[16]) ^ ($ARRAY[7] * $ARRAY[13])) - 11282): RETURN FALSE; ENDIF; IF ((($ARRAY[2] * $ARRAY[12]) ^ ($ARRAY[13] * $ARRAY[2])) - 1126): RETURN FALSE; ENDIF; IF ((($ARRAY[8] * $ARRAY[15]) ^ ($ARRAY[9] * $ARRAY[2])) - 326): RETURN FALSE; ENDIF; IF ((($ARRAY[5] * $ARRAY[11]) ^ ($ARRAY[15] * $ARRAY[12])) - 5115): RETURN FALSE; ENDIF; IF ((($ARRAY[16] * $ARRAY[2]) ^ ($ARRAY[15] * $ARRAY[7])) - 1213): RETURN FALSE; ENDIF; IF ((($ARRAY[13] * $ARRAY[12]) ^ ($ARRAY[1] * $ARRAY[16])) - 9471): RETURN FALSE; ENDIF; IF ((($ARRAY[6] * $ARRAY[16]) ^ ($ARRAY[1] * $ARRAY[3])) - 6359): RETURN FALSE; ENDIF; IF ((($ARRAY[16] * $ARRAY[5]) ^ ($ARRAY[14] * $ARRAY[9])) - 7177): RETURN FALSE; ENDIF; IF ((($ARRAY[14] * $ARRAY[10]) ^ ($ARRAY[10] * $ARRAY[1])) - 5846): RETURN FALSE; ENDIF; IF ((($ARRAY[4] * $ARRAY[3]) ^ ($ARRAY[13] * $ARRAY[12])) - 15954): RETURN FALSE; ENDIF; IF ((($ARRAY[8] * $ARRAY[8]) ^ ($ARRAY[1] * $ARRAY[14])) - 3254): RETURN FALSE; ENDIF; IF ((($ARRAY[4] * $ARRAY[15]) ^ ($ARRAY[7] * $ARRAY[8])) - 12137): RETURN FALSE; ENDIF; IF ((($ARRAY[3] * $ARRAY[10]) ^ ($ARRAY[5] * $ARRAY[4])) - 131): RETURN FALSE; ENDIF; IF ((($ARRAY[5] * $ARRAY[4]) ^ ($ARRAY[6] * $ARRAY[10])) - 2685): RETURN FALSE; ENDIF; IF ((($ARRAY[11] * $ARRAY[12]) ^ ($ARRAY[10] * $ARRAY[14])) - 7242): RETURN FALSE; ENDIF; RETURN "YES, $PARAMETER"; } RETURN TRUE;') |
이 무수히 많은 조건들을 일일이 통과할수는 없고 다른 방법이 필요한데 z3을 써주면 아주 간단히 문제를 풀 수 있다.
#!/usr/bin/python from z3 import * array = [ BitVec('a%i'%i,8) for i in range(0,17)] s = Solver() s.add(((array[3] * array[6]) ^ (array[2] * array[2])) == 7320) s.add(((array[11] * array[14]) ^ (array[9] * array[11])) == 15882) s.add(((array[14] * array[15]) ^ (array[11] * array[4])) == 11789) s.add(((array[1] * array[9]) ^ (array[8] * array[9])) == 7184) s.add(((array[13] * array[16]) ^ (array[7] * array[11])) == 10366) s.add(((array[9] * array[4]) ^ (array[4] * array[2])) == 6902) s.add(((array[13] * array[15]) ^ (array[11] * array[16])) == 0) s.add(((array[14] * array[6]) ^ (array[6] * array[1])) == 2277) s.add(((array[10] * array[9]) ^ (array[16] * array[15])) == 4385) s.add(((array[2] * array[7]) ^ (array[1] * array[10])) == 15468) s.add(((array[3] * array[14]) ^ (array[6] * array[15])) == 8075) s.add(((array[6] * array[3]) ^ (array[5] * array[10])) == 11550) s.add(((array[5] * array[3]) ^ (array[9] * array[8])) == 7668) s.add(((array[13] * array[12]) ^ (array[12] * array[1])) == 3032) s.add(((array[7] * array[4]) ^ (array[8] * array[13])) == 14067) s.add(((array[6] * array[3]) ^ (array[7] * array[7])) == 11997) s.add(((array[12] * array[11]) ^ (array[5] * array[8])) == 13208) s.add(((array[5] * array[16]) ^ (array[7] * array[13])) == 11282) s.add(((array[2] * array[12]) ^ (array[13] * array[2])) == 1126) s.add(((array[8] * array[15]) ^ (array[9] * array[2])) == 326) s.add(((array[5] * array[11]) ^ (array[15] * array[12])) == 5115) s.add(((array[16] * array[2]) ^ (array[15] * array[7])) == 1213) s.add(((array[13] * array[12]) ^ (array[1] * array[16])) == 9471) s.add(((array[6] * array[16]) ^ (array[1] * array[3])) == 6359) s.add(((array[16] * array[5]) ^ (array[14] * array[9])) == 7177) s.add(((array[14] * array[10]) ^ (array[10] * array[1])) == 5846) s.add(((array[4] * array[3]) ^ (array[13] * array[12])) == 15954) s.add(((array[8] * array[8]) ^ (array[1] * array[14])) == 3254) s.add(((array[4] * array[15]) ^ (array[7] * array[8])) == 12137) s.add(((array[3] * array[10]) ^ (array[5] * array[4])) == 131) s.add(((array[5] * array[4]) ^ (array[6] * array[10])) == 2685) s.add(((array[11] * array[12]) ^ (array[10] * array[14])) == 7242) for i in range(1,17): s.add(array[i] >= 32 and array[i] <= 126) print s.check() print s.model() |
Z3을 다루는데에 이론적인 부분은 많이 필요 없다고 생각하여 예제중심으로 포스팅을 하였읍니다~
Reference
http://blog.dragonsector.pl/2014/02/olympic-ctf-2014-welcome-to-forensics.html
http://z3prover.github.io/api/html/namespacez3py.html
http://cpl0.net/~argp/papers/z3py-guide.pdf
'Programming' 카테고리의 다른 글
| crc 정리 (0) | 2015.04.26 |
|---|---|
| android php server gcm & multipart (0) | 2014.10.09 |
| Python Assembly Emulator (0) | 2014.07.30 |
| DimiManager 개발 후기 (0) | 2014.07.11 |
| 심심해서 만든거.. (0) | 2014.04.11 |
Wireshark로 패킷 분석하기.pdf