[DiceCTF] babymix - 리버싱 / IDA / Python

 

쉬운것 같으면서도 쉽지 않은 리버싱 문제

 

python z3 를 알고있다면 금방 풀수있다.

 

반응형

 

 

babymix 라는 이름의 바이너리 파일이 하나 주어진다.

 

 

한번 실행시켜봤다.

 

admin 비밀번호를 입력하라고 요구하고,

 

비밀번호가 틀리면 Incorrect 메세지가 출력되면서 종료된다.

 

 

바로 IDA 를 이용해 디컴파일 해보았다.

 

main 함수를 보면

 

사용자의 입력값을 s에 담아 check815546 함수로 집어넣는다.

 

그 검증결과가 참일경우 Correct 라는 메세지가 출력된다.

 

 

check815546 함수를 살펴봤다.

 

사용자가 입력한 값의 각 자리를 계산해서 특정한 조건을 만족시키는지 검증한다.

 

그런데 한번 검증하고 끝나는게 아니라

 

여기서 또 check921708 함수를 호출한다.

 

 

check921708 함수도 마찬가지다.

 

 

이런식으로 이 모든 check 함수들을 통과해야 한다.

 

check 함수들에서 검증하는 내용으로 추측해보니

 

플래그의 길이는 22글자 인듯 했다.(가장 높은 배열 인덱스가 a[21])

 

그럼 이건 변수가 22개인 방정식을 풀어야 하는 것이다.

 

문제는 check 함수들을 살펴보면

 

a[0] == 97 이런식으로 특정 위치가 어떤 값을 가지는지 정확히 검사하는 수식은 없다.

 

전부다 위에 봤던것 처럼 여러 변수들의 연산한 값을 비교하고 있다.

 

이런경우 각 자리의 글자를 하나씩 추측해 나가는건 

 

경우의 수가 너무 많아서 시간이 오래걸리게 된다.

 

from z3 import *

conditions = ["(a1[12] - a1[17] + a1[12] + a1[8] == 153)",
"(a1[10] + a1[21] + (a1[19] ^ a1[2]) == 217 )",
"((a1[5] ^ a1[16]) + a1[16] + a1[3] + (a1[0] ^ a1[16]) == 232 )",
"(a1[10] + a1[3] + a1[3] - a1[19] + (a1[19] ^ a1[0]) == 328 )",
"(a1[10] - a1[8] + a1[2] - a1[19] == 74 )",
"(a1[17] - a1[1] + a1[4] + a1[11] + a1[17] - a1[9] == 166 )",
"(a1[14] + a1[10] + a1[18] - a1[9] + a1[5] + a1[10] == 413 )",
"(a1[5] - a1[16] + a1[8] - a1[12] + a1[17] - a1[13] + a1[11] - a1[2] + a1[1] + a1[21] == 98 )",
"((a1[19] ^ a1[13]) + a1[6] - a1[13] + a1[17] - a1[11] + (a1[16] ^ a1[12]) == 85 )",
"(a1[4] - a1[16] + (a1[2] ^ a1[7]) == 77 )",
"(a1[8] - a1[17] + a1[14] - a1[3] + (a1[8] ^ a1[14]) + a1[5] + a1[1] + a1[7] + a1[10] == 384 )",
"(a1[4] - a1[0] + a1[2] - a1[4] + a1[15] - a1[21] + a1[17] + a1[2] == 265 )",
"(a1[5] - a1[18] + a1[17] - a1[4] + a1[15] + a1[2] + a1[21] - a1[18] + a1[7] + a1[6] == 250 )",
"(a1[21] - a1[19] + a1[7] - a1[18] + a1[16] - a1[21] + (a1[12] ^ a1[18]) == 75 )",
"((a1[10] ^ a1[2]) + a1[2]+ a1[7] + a1[20] + a1[13] + (a1[3] ^ a1[16]) + a1[9] + a1[6] == 621 )",
"(a1[8] - a1[3] + (a1[14] ^ a1[2]) + a1[11] + a1[0] + a1[1] - a1[19] == 283 )",
"(a1[16] - a1[14] + (a1[0] ^ a1[11]) + (a1[0] ^ a1[14]) + a1[13] - a1[19] == 106 )",
"(a1[19] + a1[10] + a1[10] + a1[19] + a1[0] - a1[20] + a1[3] - a1[18] == 297 )",
"(a1[0] - a1[15] + a1[20] + a1[18] == 156 )",
"(a1[13] - a1[8] + a1[10] - a1[20] + a1[3] - a1[17] == 85 )",
"(a1[3] - a1[17] + a1[19] + a1[4] + (a1[12] ^ a1[17]) + a1[10] - a1[2] == 160 )",
"(a1[11] - a1[21] + a1[12] - a1[10] == 36 )",
"((a1[18] ^ a1[19]) + a1[6] - a1[16] + (a1[5] ^ a1[16]) == 102 )",
"(a1[6] - a1[13] + (a1[10] ^ a1[15]) + a1[21] - a1[5] == -48 )",
"((a1[5] ^ a1[3]) + a1[12] - a1[11] + (a1[6] ^ a1[4]) == 29 )",
"(a1[6] - a1[14] + a1[9] - a1[2] + a1[8] - a1[15] + a1[21] - a1[11] == -109 )",
"(a1[19] - a1[7] + a1[0] + a1[16] + a1[11] + a1[17] == 361 )"]


a1 = [BitVec(f'arr[{i}]',7) for i in range(22)]

s = Solver()

for i in conditions:
    s.add(eval(i))

print(s.check())
print(s.model())

 

이런 경우에 z3 모듈을 사용해주면 된다.

 

conditions 에 check 함수들에 적혀있는 방정식을 모두 그대로 넣어주고

 

BitVec 를 이용해 변수에 넣고싶은 수와 비트수를 설정한다.

 

arr타입을 할것이고, int형이기 때문에 7비트를 사용한다.

 

s = Solver() 는 원하는 변수에 수식을 넣기위한 준비과정이고

 

s.add()로 계산하고자 하는 수식을 추가한다.

 

s.check()함수는 값이 존재하는지 확인하고, 있으면 sat, 없으면 unsat를 리턴한다.

 

s.model()은 값이 존재할 경우 그 값을 리턴하고, 없으면 에러를 리턴한다.

 

 

코드를 실행시키면

 

몇초만에 해를 구해서 알려준다.

 

arr = [0] * 22

arr[6] = 95
arr[21] = 33
arr[12] = 48
arr[10] = 95
arr[8] = 108
arr[0] = 109
arr[3] = 95
arr[11] = 116
arr[9] = 108
arr[16] = 104
arr[18] = 114
arr[15] = 116
arr[19] = 33
arr[14] = 101
arr[17] = 51
arr[7] = 52
arr[13] = 103
arr[20] = 49
arr[4] = 105
arr[2] = 120
arr[5] = 116
arr[1] = 49

for i in arr:
    print(chr(i), end="")

 

해가 나왔으면

 

출력된 결과를 그대로 복사해서

 

이렇게 써주면 플래그를 볼 수 있다.

 

 

코드를 실행시키면 플래그가 나온다.