[Dreamhack] rev-basic-7

문제

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

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

문제 풀이

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

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

 

IDA를 통해 소스코드를 보겠습니다.

 

1. 정적 분석

main 디컴파일

Input을 출력하고 입력을 받고 sub_140001000를 호출하고 참이라면 Correct를 출력합니다.

sub_140001000 함수를 분석해 보겠습니다.

sub_140001000 디컴파일

1을 반환하기 위해선 7번째에 if문의

(i ^ (unsigned __int8)__ROL1__(*(_BYTE *)(a1 + i), i & 7)) != byte_140003000[i] 이 조건이 아니어야 합니다.

(i ^ (unsigned __int8)__ROL1__(*(_BYTE *)(a1 + i), i & 7)) == byte_140003000[i] 이 식을 좀 쉽게 작성해 보면

 

i ^ ROL(a[i], i&7) == byte_140003000[i] 이런 식으로 바꿔볼 수 있습니다.

역연산식으로는 

a1[i] = ROR(byte_140003000[i] ^ i, i & 7) 이렇게 구성됩니다.

 

ROR을 구현하기는 어려울 수 있습니다.

이번 문제는 z3 라이브러리를 이용하여 풀어보겠습니다.

 

export data

일단 byte_140003000의 배열 값을 가져오겠습니다.

from z3 import *

byte_140003000 = bytearray([0x52, 0xDF, 0xB3, 0x60, 0xF1, 0x8B, 0x1C, 0xB5, 0x57, 0xD1, 
  0x9F, 0x38, 0x4B, 0x29, 0xD9, 0x26, 0x7F, 0xC9, 0xA3, 0xE9, 
  0x53, 0x18, 0x4F, 0xB8, 0x6A, 0xCB, 0x87, 0x58, 0x5B, 0x39, 
  0x1E, 0x00])

s = Solver() # Solver 객체 생성

# 31번 반복하여 8비트 변수 생성
a = []
for i in range(31):
    val = BitVec(f'char{i}', 8)
    a.append(val)
    
# 역연산 식 작성
for i in range(31):
    s.add(i ^ RotateLeft(a[i], i&7) == byte_140003000[i])

# 해가 존재하는지 확인
if s.check() == sat:
    m = s.model() # 값을 담는 객체 변수 생성
    # 파이썬 정수 변환 후 아스키 문자로 변환하여 출력
    for i in a: 
        print(chr(m[i].as_long()), end='')

i ^ ROL(a[i], i&7) == byte_140003000[i] 해당 식을

s.add(i ^ RotateLeft(a[i], i&7) == byte_140003000[i]) 로 그대로 작성해 줍니다.

플래그 획득

플래그를 획득합니다.