D1N0's hacking blog
HackCTF - Keygen 본문
z3 solver를 써볼 문제를 찾다가 이걸 선택하게 되었다
굳이 z3 solver를 안 써도 풀 수 있을 것 같기는 한데 그래도 이왕 배운 거 써먹어보고 싶었다
문제 풀이
분석
일단 주어진 파일의 hex값을 보면 elf파일임을 알 수 있다
실행을 해보면 입력을 받는다
그리고 바로 끝나는데 키가 맞으면 뭔가 일어날 것 같다
IDA로 까보면 입력을 받고 check_key를 실행하여 1이면 flag 파일을 열어 출력해주는 것을 알 수 있다
check_key 함수는 입력받은 문자열을 encoding 함수에 넣고 OO]oUU2U<sU2UsUsK와 비교해서 같으면 1을, 아니면 0을 반환하는 구조이다
그러면 encoding 함수가 가장 중요하다고 볼 수 있다
encoding은 조금 복잡한데, 먼저 v5에 인코딩한 문자열을 저장할 공간을 할당하고, v4에 입력값의 길이를 넣고, v2에는 72를 넣는다
그리고 v4만큼 반복문을 돌리는데, ((a1[i] + 12) * v2 + 17) % 70 + 48를 v5[i]에 넣고 그 값이 새로운 v2가 되는 구조이다
코드 작성
먼저 z3 solver를 import 해준다
from z3 import *우리가 원하는 것은 v5와 비교하는 문자열이 같은 것이므로 v5를 OO]oUU2U<sU2UsUsK로 먼저 정하고, 입력값인 a1를 미지수로 두었다
v4는 v5의 길이이고, v2는 72이므로 이것들도 넣어준다
v5 = "OO]oUU2U<sU2UsUsK"
v2 = 72
v4 = len(v5)solver 객체를 만들고, a1의 각 자리를 미지수로 하는 a1 배열을 만들었다
s = Solver()
a1 = [Int('x'+str(i)) for i in range(v4)]encoding 함수의 for문에 맞도록 식을 더해준다
for j in range(v4):
s.add(ord(v5[j])==((a1[j]+12)*v2+17)%70+48)
v2 = ord(v5[j])답이 있는지 확인하고 출력해보았다
print(s.check())
print(s.model())결과
sat
[x0 = -40,
x7 = 1,
x9 = -3,
x13 = 10,
x16 = 10,
x8 = -17,
x14 = -10,
x2 = -40,
x10 = 4,
x1 = -26,
x6 = 1,
x3 = -80,
x12 = 1,
x15 = -4,
x4 = -32,
x5 = -6,
x11 = -13]답은 구해졌지만 음수가 나왔다
음수는 문자로 출력할 수가 없으니 출력 가능한 범위의 수가 나오도록 조건을 설정해준다
for k in range(len(a1)):
s.add(a1[k]>=32)
s.add(a1[k]<=126)결과
sat
[x0 = 100,
x7 = 120,
x9 = 123,
x13 = 38,
x16 = 38,
x8 = 123,
x14 = 32,
x2 = 100,
x10 = 32,
x1 = 114,
x6 = 113,
x3 = 60,
x12 = 36,
x15 = 122,
x4 = 38,
x5 = 120,
x11 = 43]잘 나오는 것을 볼 수 있다
이제 이 수들에 맞는 문자를 출력해준다
for l in range(len(a1)):
print(chr(s.model()[a1[l]].as_long()), end="")결과
drd<&xqx{{ +$& z&문제 서버에 이 문자열을 넣어줬다
근데 플래그가 안나온다
이 부분에서 삽질을 조금 했는데, 찾아보니 이 프로그램에서 입력을 받을 때 쓰는 fgets는 개행 문자까지 입력 문자열에 넣는다고 한다
플래그가 안 나온 이유는 내가 입력한 문자열 + 개행문자까지 들어가서 결과가 달라졌던 것이다
이걸 해결할 방법은 여러 가지가 있는데, 입력 뒤에 NULL을 넣어주거나, 아니면 아예 마지막 글자가 개행 문자인 키를 찾는 방법도 있다
NULL 넣어주기
간단히 pwntool을 써서 널 바이트를 넘겨줄 수 있다
from pwn import *
p = remote("ctf.j0n9hyun.xyz", 9004)
p.recvline()
p.recvline()
p.send("drd<&xqx{{ +$& z&" + "\x00")
p.interactive()
또는 간단하게 파이썬 스크립트로 인자를 넘겨줘도 된다
(python -c 'print "drd<&xqx{{ +$& z&\x00"') | nc ctf.j0n9hyun.xyz 9004
마지막 문자가 개행인 문자열 찾기
코드를 다음과 같이 수정한다
for k in range(len(a1)-1):
s.add(a1[k]>=32)
s.add(a1[k]<=126)
s.add(a1[16]==10)결과
A,d<&$q${ t+$&tz
사실 생각해보니까 마지막 글자의 조건인 ((x16 + 12)*115 + 17)%70 + 48 == 75를 10이 만족하니까
그냥 첫 번째 코드로 나온 문자열의 마지막 글자를 지우고 그냥 입력해도 플래그가 나온다
전체 코드
from z3 import *
v5 = "OO]oUU2U<sU2UsUsK"
v2 = 72
v4 = len(v5)
s = Solver()
a1 = [Int('x'+str(i)) for i in range(v4)]
for j in range(v4):
s.add(ord(v5[j])==((a1[j]+12)*v2+17)%70+48)
v2 = ord(v5[j])
for k in range(len(a1)): #18번째 줄을 사용하려면 len(a1)-1로 넣기
s.add(a1[k]>=32)
s.add(a1[k]<=126)
# s.add(a1[16]==10) # 마지막에 개행 들어가는 조건
# print(s)
print(s.check())
# print(s.model())
for l in range(len(a1)):
print(chr(s.model()[a1[l]].as_long()), end="")답 여러 개 구하기
쭉 보면 알겠지만 이 문제는 답이 한 개가 아니다
다양한 값이 궁금하면 키 출력 부분을 아래 코드로 바꾸자
while s.check() == sat:
print(''.join([chr(int(str(s.model()[x[i]]))) for i in range(len(x))]))
s.add(Or([x[i] != s.model()[x[i]] for i in range(len(x))]))