[DreamHack] verify 문제 풀이_reversing_nabi

 

main 함수

sub_160A의 반환값이 1이 되는 조건을 찾아야 합니다.

 

sub_160A 함수

sub_1395, sub_11D6, sub_14B6 함수의 반환값이 모두 1이 되는 조건을 찾아야 합니다.

 

sub_1395 함수

사용자 입력값의 길이가 43 입니다.

 

sub_11D6 함수

위 로직을 통해 input 값의 형태가 DH{00000000-0000000000-0000000000-00000000} 이라는 것을 알 수 있습니다.

 

sub_14B6 함수

calculate_string 함수를 통해 input 값에 대한 연산을 진행하고 반환값을 v4, v3, v2, v1 변수에 할당합니다.

 

calculate_string 함수

각 문자에 대해 ASCII를 16진수로 변환해주는 연산을 수행하고 그 값을 v5 변수에 더하여 반환합니다.

 

위 함수들의 연산을 통해 calculate_string 함수의 반환값인 v1, v2, v3, v4의 값을 방정식으로 구할 수 있습니다. 위 조건들을 방정식으로 만들면 아래와 같습니다.

---

v3 + v4 == 697224306874

v2 + v3 == 842444828387

v2 + v1 == 148247777351

v4 + v1 == 3027255838

(v1 ^ v2 ^ v3) == 565079939463

---

z3를 이용해 위 방정식을 풀겠습니다.

from z3 import *

solver = Solver()

v1, v2, v3, v4 = BitVecs('v1 v2 v3 v4', 64)

solver.add(v3 + v4 == 697224306874)
solver.add(v2 + v3 == 842444828387)
solver.add(v2 + v1 == 148247777351)
solver.add(v4 + v1 == 3027255838)
solver.add(v1 ^ v2 ^ v3 == 565079939463)

if solver.check() == sat:
    model = solver.model()
    print("Solution found:")
    print("v1 =", model[v1])
    print("v2 =", model[v2])
    print("v3 =", model[v3])
    print("v4 =", model[v4])
else:
    print("No solution found.")

알게된 v1, v2, v3, v4의 값을 바탕으로 문자열을 구하겠습니다. 처음에는 str → hex 연산으로 단순 구현하였는데 정상적으로 실행되지 않아 조건을 하나 하나 정해주면 힘들게 풀었습니다.. 허허

처음에 구현하였던 코드가 남아있지 않아서 왜 이상한 값이 나왔는지는 기억이 나지 않지만 중간에 int로 변환해주는 과정이 없어서 그랬던거 같습니다. 풀고 나서 다른 분들 풀이를 보니까 아주 간결하고 깔끔한 코드들이더군요…ㅎㅎ

 

저는 아래처럼 무식하게(?) 풀었습니다..

from z3 import *

solver = Solver()

variable_list = [Int('x{}'.format(i)) for i in range(10)]

for i in range(10):
    solver.add(Or(And(variable_list[i] >= 48, variable_list[i] <= 57), And(variable_list[i] >= 97, variable_list[i] <= 102)))

v5 = Int('v5')

v5 = 0
for i in range(10):
    v5 = If(And(variable_list[i] >= 48, variable_list[i] <= 57), 16 * v5 + variable_list[i] - 48, 16 * v5 + variable_list[i] - 87)

solver.add(v5 == 146880461027) #v3 = 146880461027, v2 = 695564367360

if solver.check() == sat:
    model = solver.model()
    ascii_str = ''.join(chr(model[variable_list[i]].as_long()) for i in range(10))
    print(ascii_str)
else:
    print("No solution found.")

from z3 import *

solver = Solver()

variable_list = [Int('x{}'.format(i)) for i in range(8)]

for i in range(8):
    solver.add(Or(And(variable_list[i] >= 48, variable_list[i] <= 57), And(variable_list[i] >= 97, variable_list[i] <= 102)))
v5 = Int('v5')

v5 = 0
for i in range(8):
    v5 = If(And(variable_list[i] >= 48, variable_list[i] <= 57), 16 * v5 + variable_list[i] - 48, 16 * v5 + variable_list[i] - 87)

solver.add(v5 == 1367316324) #v3 = 1367316324, v4 = 1659939514

if solver.check() == sat:
    model = solver.model()
    ascii_str = ''.join(chr(model[variable_list[i]].as_long()) for i in range(8))
    print(ascii_str)
else:
    print("No solution found.")

위 식에 이전 함수 분석을 통해 알게 되었던 조건들을 넣어주었습니다.

---

1. 모든 문자는 48<=0~9<=57 || 97<=a~f<=102 의 값이다.
2. v1 = 1367316324 (8byte)
   v2 = 146880461027 (10byte)
   v3 = 695564367360 (10byte)
   v4 = 1659939514 (8byte)

---

z3가 익숙하지 않아서 무식한 코드를 짜게 되었는데… 점점 문제 풀면서 늘겠죠…?ㅎㅎ

아무튼 위 값을 바탕으로 플래그를 조합하였습니다. 참고로 저는 플래그를 거꾸로 넣어서 왜 안되나 계속 그러고 있었습니다 허허

 

DH{decrypt(v4)-decrypt(v3)-decrypt(v2)-decrypt(v1)}

위 코드를 바탕으로 복호화된 값을 순서대로 넣어주면 플래그가 완성됩니다.