z3에 적응하기 위해 RedVelvet을 풀어보자.

오늘은 z3에 적응하기 위해서 2018 Codegate 예선전 문제로 나온 Redvelvet을 풀어보겠습니다.

일단 DIE에 던져줍시다.

우분투 x64 환경에서 한 번 돌려봅시다.

프로그램이.. 죽어버렸네요.

IDA로 살펴보면 27의 길이의 문자열을 입력받은 후 15개의 함수를 거쳐서 값을 검증한 후 

SHA256 해시 함수로 암호화하여 바이너리에 하드코딩되어 있는 긴 문자열과 비교하고 있습니다.

---

이름을 지어주자.

이대로 계속 작업을 하다간 멘탈폭사를 겪을 수 있습니다. 네이밍을 해줍시다.

혹시 모르는 함수가 있다면 제가 참조글 링크를 해놨으니 한 번 보시는 것을 추천드립니다.

OpenSSL 라이브러리 홈페이지에서 설명한 SHA*_* 함수

ptrace 함수 설명

흐름이 이제 보이는 것 같습니다. 

NULL을 제외한 26글자를 받아서 func1~func15까지 검증 루틴을 거쳐서 하드코딩된 해시값과 비교합니다.

해시값과 입력한 글자의 해시한 값이 맞으면 플래그인 것이고 아니면 플래그가 아닌 것이군요.

func1에서 func15까지의 검증 루틴을 살펴볼까요?

func1

func2

func3

func4

그만봅시다. C로 게싱할 생각이였는데 잘못하면 날밤 새겠네요. z3를 씁시다.

---

z3

z3은 Microsoft에서 개발한 수식 해석 도구입니다. 수학적인 요소들을 해결하는데 도움을 준다고 하네요.

z3에 관련한 문서와 포스트는.. Z3-a tutorial과 해적왕님 포스트 추천해드립니다.

일단 코드를 짭시다.

검증 루틴 코드 붙여넣는데 && 연산자가 안 먹어서 봤더니 Python에서는 and라는 예약어가 따로 있더라구요.

(근데 and를 썼는데 에러가 걸려서 And()를 쓰게 되었습니다.)

아래처럼 검증 루틴이 하는 행위를 반대로 해서 따라하면 될 듯 싶습니다.

글자 수가 26개인데... 일일히 BitVec 함수에 이름 넣어주다간 손가락이 나가겠군요;;  잔머리를 굴립시다.

크으... 함수를 구현한 값어치를 여기에서 써먹습니다. 수식을 구현을 이리 편하게~

출력하게 만들어주고! 한번 돌려봅시다!

What_You_Wanna_Be?:)_l'_la가 떠서 넣어봤는데 정답이라고 뜨지 않는군요...

---

조금 생각을 해봤습니다. z3에서 구해진 플래그가 과연 하나만 있을 수 있을까?

이차방정식도 삼차방정식도 답이 여러 개가 있을 수 있는데 나는 주어진 힌트를 다 활용하지 않은 것이 아닐까?

주어진 힌트를 다 활용하기 위해서 손님 한 분 모셔왔습니다! hashlib 라이브러리입니다!

우리가 입력한 플래그를 해시 함수에 돌려서 하드코딩된 해시값과 같은지 확인해봅시다.

수식을 통과한 플래그가 여러 개라는 가정이 사실이라고 생각해봤을 때 코드를 좀 바꿔야겠네요.

계속 플래그를 구하도록 무한 루프를 돌리고 같은 플래그를 구하지 않도록 수식을 추가시키는 겁니다.

플래그를 구했으면 빠져나가 주도록 break 문도 걸어줍니다.

돌려보면 답이 나오겠죠?

첫 날에는 Z3 공부하면서 설치하느라 애먹고 둘쨋날에는 Python 숙련도 때문에 어려웠습니다.

새로운 언어에 익숙해진다는게 참... 힘드네요.