[Defcon CTF 2016] baby-re write up

defcon ctf는 언제나 어려웠는데, 이번에도 어렵게 느껴졌다.

그렇게 꼬아놓지도 않았는데, 엄청 고생한 거 같다.

baby-re는 최근에 애용하고 있는 z3를 잘 이용하면 풀 수 있는 문제이다.

풀고나서 보면 정말 간단한 문제이다.

총 13번의 입력을 받는다.

그리고 결과 값으로 wrong 또는 키값을 출력하는데,

키값을 출력하는 조건을 확인하는 CheckSolution함수가 IDA로 디 컴파일이 안 된다.

오류 메시지는 function frame is wrong이라고 뜬다.

그래서 graph view 모드로 확인해보니까 뭔가 엄청 길다...

그런데 핸드레이 못할 만큼 긴 것은 아닌 거 같아서

핸드레이로 풀려고 했는데.

중간에 쓰레기 값때문인 것으로 추측하고 해서 제거를 시도했다.

아래 처럼 쓰레기 값있는 부분을 hexeditor로 00으로 변경했다

운 좋게도 바로 디컴파일러가 되서 해당 소스를 살펴보니 13차 연립방정식이다.

연립방정식 같은 수식을 계산하는 파이썬 모듈이 있는데

마이크로소프트사에서 개발한 Z3라는 모듈이 있다.

해당 모듈로 돌리면 답을 얻을 수 있다.

from z3 import *
 
a1 = [Int("a1_%d"%(i)) for i in range(0,13)]
s = Solver()
 
s.add ( 39342 * a1[11]+ 21090 * a1[10]+ 14626 * a1[9]+ 57693 * a1[8]+ 16388 * a1[7]+ 29554 * a1[6]+ 43166 * a1[5]+ 50633 * a1[4]+ 37485 * a1[0]- 21621 * a1[1]- 1874 * a1[2]- 46273 * a1[3]+ 54757 * a1[12] == 21399379 )
 
s.add ( 22599 * a1[5]+ 14794 * a1[4]+ 38962 * a1[3]+ 50936 * a1[0]+ 4809 * a1[1]- 6019 * a1[2]- 837 * a1[6]- 36727 * a1[7]- 50592 * a1[8]- 11829 * a1[9]- 20046 * a1[10]- 9256 * a1[11]+ 53228 * a1[12] == 1453872 )
 
s.add ( 5371 * a1[11]+ 42654 * a1[10]+ 17702 * a1[8]+ 26907 * a1[3]+ -38730 * a1[0]+ 52943 * a1[1]- 16882 * a1[2]- 44446 * a1[4]- 18601 * a1[5]- 65221 * a1[6]- 47543 * a1[7]- 33910 * a1[9]+ 11469 * a1[12] == -5074020 )
 
s.add ( 8621 * a1[10]+ 34805 * a1[7]+ 10649 * a1[6]+ 54317 * a1[4]+ 57747 * a1[0]- 23889 * a1[1]- 26016 * a1[2]- 25170 * a1[3]- 32337 * a1[5]- 9171 * a1[8]- 22855 * a1[9]- 634 * a1[11]- 11864 * a1[12] == -5467933 )
 
s.add ( 15578 * a1[11]+ 43186 * a1[9]+ 28134 * a1[8]+ 54889 * a1[4]+ 34670 * a1[3]+ 43964 * a1[2]+ -14005 * a1[0]+ 16323 * a1[1]- 6141 * a1[5]- 35427 * a1[6]- 61977 * a1[7]- 59676 * a1[10]+ 50082 * a1[12] == 7787144 )
 
s.add ( 10305 * a1[11]+ 29341 * a1[10]+ 13602 * a1[7]+ 39603 * a1[6]+ 13608 * a1[2]+ -40760 * a1[0]- 22014 * a1[1]- 4946 * a1[3]- 26750 * a1[4]- 31708 * a1[5]- 59055 * a1[8]- 32738 * a1[9]- 15650 * a1[12] == -8863847 )
 
s.add ( 16047 * a1[9]+ 55241 * a1[7]+ 13477 * a1[2]+ -47499 * a1[0]+ 57856 * a1[1]- 10219 * a1[3]- 5032 * a1[4]- 21039 * a1[5]- 29607 * a1[6]- 6065 * a1[8]- 4554 * a1[10]- 2262 * a1[11]+ 18903 * a1[12] == -747805 )
 
s.add ( 41178 * a1[11]+ 47909 * a1[7]+ 53309 * a1[6]+ -65419 * a1[0]+ 17175 * a1[1]- 9410 * a1[2]- 22514 * a1[3]- 52377 * a1[4]- 9235 * a1[5]- 59111 * a1[8]- 41289 * a1[9]- 24422 * a1[10]- 23447 * a1[12] == -11379056 )
 
s.add ( 15699 * a1[10]+ 58551 * a1[5]+ 46767 * a1[4]+ 33381 * a1[3]+ 1805 * a1[0]+ 4135 * a1[1]- 16900 * a1[2]- 34118 * a1[6]- 44920 * a1[7]- 11933 * a1[8]- 20530 * a1[9]- 36597 * a1[11]+ 18231 * a1[12] == -166140 )
 
s.add ( 10788 * a1[10]+ 18975 * a1[9]+ 15033 * a1[8]+ 42363 * a1[7]+ 47052 * a1[6]+ 41284 * a1[3]+ -42941 * a1[0]+ 61056 * a1[1]- 45169 * a1[2]- 1722 * a1[4]- 26423 * a1[5]- 33319 * a1[11]+ 63680 * a1[12] == 9010363 )
 
s.add ( 30753 * a1[10]+ 22613 * a1[9]+ 58786 * a1[7]+ 12587 * a1[6]+ 12746 * a1[5]+ -37085 * a1[0]- 51590 * a1[1]- 17798 * a1[2]- 10127 * a1[3]- 52388 * a1[4]- 8269 * a1[8]- 20853 * a1[11]+ 32216 * a1[12] == -4169825 )
 
s.add ( 57612 * a1[11]+ 47348 * a1[9]+ 48719 * a1[8]+ 9228 * a1[5]+ 65196 * a1[4]+ 36650 * a1[0]+ 47566 * a1[1]- 33282 * a1[2]- 59180 * a1[3]- 59599 * a1[6]- 62888 * a1[7]- 37592 * a1[10]+ 40510 * a1[12] == 4081505 )
 
s.add ( 25633 * a1[11]+ 25252 * a1[9]+ 28153 * a1[8]+ 26517 * a1[7]+ 59511 * a1[4]+ 4102 * a1[3]+ 51735 * a1[0]+ 35879 * a1[1]- 63890 * a1[2]- 21386 * a1[5]- 20769 * a1[6]- 43789 * a1[10]+ 7314 * a1[12] == 1788229 )
 
print s.check()
m = s.model()
 
for d in m.decls():
  print "%s = %s" %(d.name(),m[d])
 

PS.

이렇게 푸는 방법도 있지만,

요즘 유행하는 angr를 이용하면 코딩만으로 쉽게 풀 수 있습니다.

해당 방법은 geame가 포스팅 할 거라 믿고 이번 포스팅에는 포함 안 합니다.