[z3 solver, WinDbg, IDA] 여러 조건문을 만족시키는 flag 찾기 & 디버깅 [@ KUICS]

IT/역공학

[z3 solver, WinDbg, IDA] 여러 조건문을 만족시키는 flag 찾기 & 디버깅 [@ KUICS]

kykyky 2024. 3. 10. 22:53

아래 내용은 고려대학교 정보보호 동아리 KUICS의 수업 내용을 바탕으로 작성한 것입니다.

1. IDA를 통해 실행파일 디컴파일하여 flag 조건 확인

✅ line 11~14:

while문을 통해, v3의 값이 v7의 요소 개수와 같아집니다.

✅ line 37~40:

v4 == True여야만 v5가 congratulations!가 됨을 알 수 있습니다.

✅ line 15~36:

if ~ ~, else ~ 구조입니다.

else가 실행될 경우 v4 = 0 즉 False가 되므로,

v4 = True가 될 수 있도록 if가 실행되어야 함을 알 수 있습니다.

따라서 line 15~27이 모두 만족되어야 합니다.

(물론 이것이 만족되어도 v4는 아직 0입니다.)

✅ line 30~31:

line 30을 만족하면 line 31이 수행되고,

line 31에서는 LOBYTE(v4)에 True 혹은 False가 대입됨을 알 수 있습니다.

우리는 v4 == True를 만들어야 하므로,

우선 line 30을 만족시켜 if문 안으로 들어가야 하고,

LOBYTE(v4)에 True를 대입하기 위해 (v7[5] ^ v7[15]) == 21가 참이어야겠군요.

2. 조건을 모두 만족하는 flag를 찾기 by z3 solver @ python

from z3 import *

s = Solver() # solver 클래스 객체

buf = [BitVec(f"buf_{i}", 8) for i in range(16)] # buf_0, buf_1, ..., buf_15라는 이름의 8bit 크기의 bit-vector 변수들이 buf에 담김
flag = [0] * 16

# solver 객체에 조건식들을 모두 add하기
s.add(buf[0] == ord('F'))
s.add(buf[1] == ord('L'))
s.add(buf[2] == ord('A'))
s.add(buf[3] == ord('G'))
s.add(buf[0]^buf[3] == 1)
s.add(buf[1]^buf[11] == 35)
s.add(buf[1]^buf[2]^buf[14] == 105)
s.add(buf[3]^buf[14]^buf[8] == 79)
s.add(buf[12]^buf[4]^buf[13] == 101)
s.add(buf[5]^buf[9] == 7)
s.add(buf[13]^buf[6] == 9)
s.add(buf[2]^(buf[7]^buf[15]) == 80)
s.add(buf[1]^buf[8] == 32)
s.add(buf[2]^(buf[12]^buf[9]) == 92)
s.add(buf[3]^(buf[14]^buf[10]) == 84)
s.add(buf[11]^buf[5] == 7)
s.add(buf[14]^(buf[13]^buf[10]) == 127)
s.add(buf[5]^buf[15] == 21)

if s.check() != sat: # satisfiable한지 확인
    exit("Not satisfiable")

m = s.model()
for i in range(16):
    flag[i] = m[buf[i]].as_long() # model 객체를 이용해 flag 각 바이트의 정답 맞추기

print("".join(map(chr, flag))) # flag의 integer들을 ASCII character로 전환한 뒤 하나의 string으로 합침