Defcon 23 Prequals - fuckup (writeup 분석 with z3)

• write up - https://github.com/kitctf/writeups/blob/master/defcon-quals-2015/fuckup/pwn.py
  
  
• defcon 예선 당시 fuckup 을 풀이하였는데, Well512() 의사난수 알고리즘의 state[16]를 모두 알아내면 그 다음에 나올 의사 난수를 예측할 수 있습니다. 근데 이걸 못해서 포기했었는데, 이후 Symbolic execution을 해주는 SMT solver로 z3라는 툴을 알게되어 이를 공부하기 위해 z3를 이용하여 풀이한 write up을 분석해봤습니다.
  
  
• alalrm(30) -> alarm(0)으로 패치된 바이너리

• fuckup_no_alarm

아래 사진을 보면 먼저 BitVecs()를 이용해 32비트 변수 16개를 선언해주고 있습니다.

그리고 159 라인에서 바이너리 내 well512() 의사 난수 생성함수를 파이썬 코드로 옮겨놓은 prngz3() 함수를 실행하고, 

160 라인에서는 실행 파일을 실행했을 때 나오는 메뉴 중 '3' 번을 실행하고 전달받은 현재 image_base 의 주소를 받아옵니다.

그리고 solver.add()함수에 prevstate[idx] == curr_value 라는 수식을 넣어 prevstate[idx]가 전달 받은 랜덤 값(curr_value)과 같아질 조건을 만족하기 위해 다른 값들을 자동으로 채워넣어 줍니다.

이를 16번 반복하게 됩니다. 

그리고 solver.check()를 실행하여 반환 값이 sat 인 경우 이전 조건식에서 모두 만족되는 결과가 나왔다는 뜻이므로 "State successfully recovered" 를 출력하고 다음으로 넘어가게 됩니다. 

위 과정에서 초기 state를 제대로 복구했기 때문에 170 라인에서는 solver.model()[v]를 이용하여 해당 값들을 지역변수인 state에 옮겨줍니다.

지금까지 Well512() 함수가 16번 실행되었으므로 178~180 라인에서 구해놓은 이전 state에서 16번을 더 돌려 줍니다. 

(위에서는 z3의 변수인 prevstate를 사용하였으므로 z3 에서 사용하는 전용 함수들이 사용되어 prngz3()를 사용했지만 이제는 단순 비트연산 이므로 prng()를 사용하여 계산합니다.)

그리고 180 라인에서 prng()함수를 한 번 더 돌려주고 184번에서 전달받은 랜덤 값과 같은지 최종적으로 확인하게 됩니다. 

지금까지 계산으로 state를 모두 구했고, 다음 난수를 예측할 수 있게 되었으므로 공격하기 위해 프로그램의 메뉴 중 '4'번을 실행하면 나오는 함수를 보겠습니다. read() 함수가 실행될 때 까지 Well512() 함수가 한 번 실행되고, 밑의 사진에 화살표 부분에서 100바이트를 입력하게 되면 Well512()함수는 98번 실행되게 됩니다. 또한 아래 Rand_Memory() 함수에서 추가로 한 번 더 실행되어 최종적으로 공격 페이로드가 동작할 때의 바이너리 주소는 프로그램의 메뉴 위치에서 볼 때 Well512() 함수가 100번 실행된 뒤의 값을 Image_base로 사용함을 알 수 있습니다. 

따라서, 191~192 라인에서 prng()함수를 100번 실행해주고, 해당 인덱스위치의 state 값을 image_base로 사용함을 알 수 있습니다.

이후에는 이를 이용하여 ROP페이로드를 작성하고 공격함을 알 수 있습니다.