[247CTF] THE SECRET LOCK - 리버싱 / Python

 

247CTF 에서 제공하는

 

MODERATE 난이도의 리버싱 문제

 

반응형

 

 

문제에서 주어지는 것은

 

The Secret Lock.html 파일이다.

 

 

 

문제에서 주어진 HTML 파일을 실행시켜 보면

 

이런 화면이 나온다..

 

번호 40개짜리 자물쇠인데

 

각 번호는 0부터 500까지 구성되어 있다.

 

자전거 자물쇠처럼 돌려서 맞춰야 하는건데

 

일단 확률부터 말도 안되고,

 

실제로 돌려볼려해도 너무 느려서 이번생 안에는 도저히 못한다.

 

 

 

F12를 눌러 개발자도구를 열어

 

Javascript 코드를 보니

 

플래그를 검증하는 듯한 부분이 보였다.

 

 

 

해당 부분을 깔끔하게 보이게 정리해보니

 

이런 형태였다... 무려 120줄이다.

 

이 어마어마한 연립방정식을 풀어야 플래그를 찾을 수 있는데

 

마치 수능을 다시보는 기분이었다.

 

from z3 import *

conditions = ["((flag[37] - flag[37]) * flag[15] == 0)", 
"((flag[3] + flag[31]) ^ (flag[29] + flag[8]) == 234)", 
"((flag[32] - flag[12]) * flag[9] == -2332)", 
"((flag[24] - flag[27] + flag[13]) ^ flag[6] == 114)", 
"((flag[38] - flag[15]) * flag[33] == 800)", 
"((flag[34] - flag[21]) * flag[26] == 98)", 
"((flag[29] + flag[0]) ^ (flag[8] + flag[38]) == 248)", 
"((flag[21] * flag[18]) ^ (flag[7] - flag[15]) == 2694)", 
"((flag[28] * flag[23]) ^ (flag[19] - flag[5]) == -9813)", 
"((flag[34] + flag[30]) ^ (flag[37] + flag[6]) == 72)", 
"((flag[23] - flag[22]) * flag[12] == 4950)", 
"((flag[9] * flag[28]) ^ (flag[20] - flag[11]) == 5143)", 
"((flag[2] * flag[22]) ^ (flag[37] - flag[0]) == 2759)", 
"((flag[26] - flag[12]) * flag[3] == -3350)", 
"((flag[35] * flag[0]) ^ (flag[23] - flag[21]) == 2698)", 
"((flag[20] + flag[31]) ^ (flag[5] + flag[10]) == 22)", 
"((flag[31] * flag[19]) ^ (flag[1] - flag[2]) == -2655)", 
"((flag[38] - flag[14]) * flag[18] == 55)", 
"((flag[29] - flag[19] + flag[10]) ^ flag[2] == 93)", 
"((flag[13] - flag[25] + flag[30]) ^ flag[29] == 13)", 
"((flag[35] + flag[33]) ^ (flag[26] + flag[21]) == 249)", 
"((flag[17] + flag[24]) ^ (flag[34] + flag[1]) == 253)", 
"((flag[32] - flag[35] + flag[19]) ^ flag[1] == 0)", 
"((flag[22] - flag[11] + flag[3]) ^ flag[31] == 113)", 
"((flag[19] - flag[0]) * flag[13] == 108)", 
"((flag[19] - flag[17]) * flag[14] == -2475)", 
"((flag[31] - flag[35] + flag[16]) ^ flag[19] == 84)", 
"((flag[24] * flag[27]) ^ (flag[35] - flag[17]) == -5792)", 
"((flag[11] * flag[35]) ^ (flag[15] - flag[28]) == -2845)", 
"((flag[18] - flag[19] + flag[31]) ^ flag[5] == 112)", 
"((flag[20] - flag[6]) * flag[10] == -3933)", 
"((flag[39] - flag[33]) * flag[6] == 3075)", 
"((flag[22] + flag[1]) ^ (flag[39] + flag[14]) == 211)", 
"((flag[37] * flag[24]) ^ (flag[12] - flag[39]) == -5726)", 
"((flag[29] + flag[3]) ^ (flag[8] + flag[11]) == 195)", 
"((flag[26] * flag[7]) ^ (flag[10] - flag[17]) == -2375)", 
"((flag[11] - flag[12]) * flag[12] == -4653)", 
"((flag[13] * flag[5]) ^ (flag[12] - flag[25]) == 3829)", 
"((flag[24] * flag[0]) ^ (flag[13] - flag[23]) == -2829)", 
"((flag[17] + flag[12]) ^ (flag[8] + flag[14]) == 170)", 
"((flag[38] + flag[23]) ^ (flag[11] + flag[1]) == 245)", 
"((flag[22] + flag[5]) ^ (flag[21] + flag[24]) == 19)", 
"((flag[35] - flag[8] + flag[21]) ^ flag[30] == 85)", 
"((flag[18] - flag[31] + flag[28]) ^ flag[29] == 0)", 
"((flag[30] * flag[35]) ^ (flag[27] - flag[29]) == 5501)", 
"((flag[8] - flag[30] + flag[16]) ^ flag[36] == 81)", 
"((flag[13] * flag[18]) ^ (flag[35] - flag[38]) == -2971)", 
"((flag[27] - flag[14]) * flag[39] == 5875)", 
"((flag[34] - flag[33]) * flag[6] == -6027)", 
"((flag[38] * flag[1]) ^ (flag[20] - flag[10]) == -2915)", 
"((flag[1] - flag[1]) * flag[3] == 0)", 
"((flag[36] - flag[20]) * flag[8] == 2640)", 
"((flag[23] - flag[11] + flag[17]) ^ flag[33] == 246)", 
"((flag[13] - flag[38]) * flag[0] == -100)", 
"((flag[28] - flag[14]) * flag[31] == 2142)", 
"((flag[26] + flag[15]) ^ (flag[13] + flag[31]) == 8)", 
"((flag[36] - flag[15]) * flag[17] == 5238)", 
"((flag[16] - flag[30]) * flag[33] == 0)", 
"((flag[2] - flag[20] + flag[13]) ^ flag[6] == 76)", 
"((flag[10] - flag[14] + flag[31]) ^ flag[13] == 3)", 
"((flag[0] * flag[10]) ^ (flag[14] - flag[31]) == 2854)", 
"((flag[28] - flag[34] + flag[14]) ^ flag[14] == 82)", 
"((flag[28] - flag[25]) * flag[1] == 2444)", 
"((flag[34] - flag[12]) * flag[25] == -2400)", 
"((flag[28] * flag[38]) ^ (flag[17] - flag[4]) == 5429)", 
"((flag[21] - flag[21] + flag[26]) ^ flag[23] == 84)", 
"((flag[9] - flag[4] + flag[18]) ^ flag[35] == 47)", 
"((flag[28] - flag[21] + flag[1]) ^ flag[33] == 0)", 
"((flag[24] - flag[25] + flag[22]) ^ flag[0] == 8)", 
"((flag[28] - flag[25]) * flag[12] == 4653)", 
"((flag[1] * flag[15]) ^ (flag[10] - flag[8]) == 2498)", 
"((flag[5] * flag[7]) ^ (flag[15] - flag[34]) == -3429)", 
"((flag[8] * flag[3]) ^ (flag[23] - flag[22]) == 3671)", 
"((flag[25] - flag[33]) * flag[11] == -2600)", 
"((flag[21] + flag[12]) ^ (flag[37] + flag[28]) == 81)", 
"((flag[30] + flag[33]) ^ (flag[34] + flag[14]) == 162)", 
"((flag[6] - flag[25]) * flag[8] == 4015)", 
"((flag[24] - flag[7] + flag[12]) ^ flag[7] == 90)", 
"((flag[18] * flag[12]) ^ (flag[8] - flag[4]) == -5466)", 
"((flag[32] * flag[7]) ^ (flag[32] - flag[27]) == -2730)", 
"((flag[32] * flag[34]) ^ (flag[29] - flag[16]) == 2804)", 
"((flag[25] * flag[22]) ^ (flag[28] - flag[39]) == -2542)", 
"((flag[8] - flag[15]) * flag[6] == 861)", 
"((flag[20] + flag[18]) ^ (flag[25] + flag[36]) == 245)", 
"((flag[5] - flag[28] + flag[14]) ^ flag[39] == 97)", 
"((flag[30] * flag[11]) ^ (flag[16] - flag[11]) == 5216)", 
"((flag[11] + flag[18]) ^ (flag[7] + flag[9]) == 13)", 
"((flag[9] - flag[2]) * flag[30] == -200)", 
"((flag[12] + flag[37]) ^ (flag[9] + flag[4]) == 78)", 
"((flag[10] - flag[37]) * flag[38] == -2408)", 
"((flag[5] * flag[19]) ^ (flag[20] - flag[21]) == 3645)", 
"((flag[27] * flag[29]) ^ (flag[39] - flag[21]) == 10354)", 
"((flag[15] * flag[32]) ^ (flag[7] - flag[22]) == -2642)", 
"((flag[1] - flag[3] + flag[24]) ^ flag[31] == 25)", 
"((flag[13] - flag[0]) * flag[30] == 400)", 
"((flag[18] - flag[15] + flag[36]) ^ flag[28] == 12)", 
"((flag[34] + flag[21]) ^ (flag[12] + flag[37]) == 163)", 
"((flag[36] - flag[33]) * flag[14] == 110)", 
"((flag[2] - flag[3]) * flag[3] == -804)", 
"((flag[35] - flag[27] + flag[22]) ^ flag[4] == 80)", 
"((flag[10] + flag[9]) ^ (flag[17] + flag[2]) == 246)", 
"((flag[25] * flag[4]) ^ (flag[27] - flag[23]) == 4201)", 
"((flag[32] * flag[19]) ^ (flag[3] - flag[25]) == 2877)", 
"((flag[37] - flag[14]) * flag[23] == 4545)", 
"((flag[32] + flag[13]) ^ (flag[31] + flag[32]) == 7)", 
"((flag[11] - flag[25]) * flag[39] == 250)", 
"((flag[17] + flag[31]) ^ (flag[6] + flag[9]) == 36)", 
"((flag[4] + flag[27]) ^ (flag[2] + flag[31]) == 208)", 
"((flag[6] + flag[7]) ^ (flag[26] + flag[21]) == 206)", 
"((flag[19] + flag[25]) ^ (flag[22] + flag[10]) == 10)", 
"((flag[34] + flag[2]) ^ (flag[8] + flag[26]) == 2)", 
"((flag[7] + flag[5]) ^ (flag[12] + flag[14]) == 237)", 
"((flag[1] - flag[13]) * flag[38] == -112)", 
"((flag[0] - flag[19] + flag[16]) ^ flag[0] == 80)", 
"((flag[31] + flag[36]) ^ (flag[3] + flag[2]) == 227)", 
"((flag[32] - flag[3] + flag[26]) ^ flag[4] == 113)", 
"((flag[3] * flag[6]) ^ (flag[16] - flag[27]) == -8241)", 
"((flag[24] + flag[15]) ^ (flag[2] + flag[30]) == 242)", 
"((flag[11] + flag[21]) ^ (flag[31] + flag[20]) == 12)", 
"((flag[9] - flag[26] + flag[23]) ^ flag[30] == 13)"]


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

s = Solver()

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

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

 

 

하지만 우리에겐 파이썬이 있다.

 

파이썬의 z3를 이용하면 이런것쯤은 금방 해결 가능하다.

 

먼저 조건식들을 배열로 만들어주고

 

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

 

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

 

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

 

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

 

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

 

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

 

 

 

실행시키면 순식간에 결과가 출력된다.

 

배열의 각 값을 합쳐서 chr 로 바꿔 제출하면 된다.