[Dreamhack] rev-basic-5

문제

이 문제는 사용자에게 문자열 입력을 받아 정해진 방법으로 입력값을 검증하여 correct 또는 wrong을 출력하는 프로그램이 주어집니다.

해당 바이너리를 분석하여 correct를 출력하는 입력값을 알아내세요.

문제 풀이

해당 바이너리를 실행해 보겠습니다.

올바른 입력값을 입력해야 Correct를 출력해 줍니다.

IDA를 통해 코드를 분석해 보겠습니다.

 

1. 정적 분석

main 디컴파일

sub_140001000의 리턴값이 참이어야 Correct를 출력합니다.

반복문을 총 24번 돌면서

7번째 줄에 if문의 조건을 만족하지 않아야 1을 반환합니다.

*(unsigned __int8 *)(a1 + i + 1) + *(unsigned __int8 *)(a1 + i) != byte_140003000[i] 해당 식을 쉽게 작성해 보면

a1[i+1] + a1[i] == byte_140003000[i] 이 됩니다.

a1의 입력값을 알기 위해선 이를 역연산 해야 합니다.

a1[i] == byte_140003000[i] - a1[i+1] 이렇게 작성해 볼 수 있습니다.

이 문제는 z3를 이용하여 풀이해보겠습니다.

export data

byte_140003000의 배열 요소들을 가져오겠습니다.

from z3 import *

byte_140003000 = bytearray([0xAD, 0xD8, 0xCB, 0xCB, 0x9D, 0x97, 0xCB, 0xC4, 0x92, 0xA1, 
  0xD2, 0xD7, 0xD2, 0xD6, 0xA8, 0xA5, 0xDC, 0xC7, 0xAD, 0xA3, 
  0xA1, 0x98, 0x4C, 0x00])

s = Solver() # Solver 객체 생성

# 0~24 8비트 변수 생성
a1 = []
for i in range(25):
    val = BitVec(f'char{i}', 8)
    a1.append(val)

# 연산 식 작성
for i in range(24):
    s.add(a1[i+1]+a1[i]==byte_140003000[i])
# a1[23]을 구하기 위해선 a1[24]가 있어야 되므로 a1[24] = 0
s.add(a1[24] == 0)

# 해가 존재하는지 확인
if s.check() == sat:
    m = s.model() # 값을 담는 객체 변수 생성
    for i in a1:
        print(chr(m[i].as_long()), end='')

 

플래그를 획득합니다.