[Dreamhack] rev-basic-8

문제

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

해당 바이너리를 분석하여 correct를 출력하는 입력값을 찾으세요!

문제 풀이

먼저 IDA로 분석을 해볼게요.

main 디컴파일

sub_1400011B0은 printf, sub_140001210은 scanf로 대응이 되겠고

sub_140001000이 참이면 Correct를 출력하네요.

sub_140001000을 분석해볼게요.

sub_140001000 디컴파일

21만큼 반복하여 내부 조건문을 만족하지 않으면 return 1;을 하네요.

안의 조건문 코드를 볼게요.

입력값에 -5을 곱한게 byte_140003000의 배열 값과 일치한지 확인하고 있어요.

해당 코드를 쉽게 변환하면 이런 코드로 됩니다.

해당 코드를 역연산 하려고 했으나.. 계속 실패해서

어짜피 값은 1바이트(8비트)이므로 256가지의 경우의 수가 있을 것이고 브루트포스를 통하여 값을 찾아내볼게요.

Export data

byte_140003000의 배열 값을 확인합니다.

어셈블리 확인

해당 코드의 어셈블리를 확인해볼게요.

-5을 곱했으므로 컴퓨터 내에서는 2의 보수를 취하여 연산을 진행합니다.

0000 0101 -- (2의보수) --> 1111 1011

-5는 2의 보수로 0xFB가 됩니다.

그리고 and 0xFF 연산을 통해 1바이트만을 남깁니다.

data = bytearray([0xAC, 0xF3, 0x0C, 0x25, 0xA3, 0x10, 0xB7, 0x25, 0x16, 0xC6, 
  0xB7, 0xBC, 0x07, 0x25, 0x02, 0xD5, 0xC6, 0x11, 0x07, 0xC5, 0x00])

for i in range(21):
    for j in range(255):
      if (j * 0xFB) & 0xFF == data[i]:
        print(chr(j), end='')

0~255가지 총 256가지의 경우의 수를 반복하여 위의 연산대로 로직을 구한 파이썬 코드입니다.

 

브루트포스 익스를 통한 문제풀이도 있지만

z3 라이브러리를 이용한 풀이도 있어요.

 

z3?

- 파이썬에서 수학적/논리적 제약 조건을 만족하는 해를 찾는 SMT(Satisfiability Modulo Theories) 솔버

 

주로 사용 되는 z3 명령어는 다음과 같아요.

 

s = Solver()

- 제약 조건을 저장하고 해를 판별하는 Solver 객체 생성

 

BitVec()

- 비트 단위로 동작하는 미지수를 만듬

 

s.add()

- 계산하고자 하는 수식을 추가

 

s.check()

- 해가 존재하는지(sat) 불가능한지(unsat) 판별

 

s.model()

- 결과가 sat일때 값을 반환

 

from z3 import *

data = bytearray([0xAC, 0xF3, 0x0C, 0x25, 0xA3, 0x10, 0xB7, 0x25, 0x16, 0xC6, 
   0xB7, 0xBC, 0x07, 0x25, 0x02, 0xD5, 0xC6, 0x11, 0x07, 0xC5, 0x00])

# 솔버 생성
s = Solver() 

# 21번 반복하여 8비트 변수 생성
input_data = []
for i in range(21):
    val = BitVec(f'char{i}', 8)
    input_data.append(val)

# 역연산 수식 추가
for i in range(21):
    s.add((-5 * input_data[i]) == data[i])
        
if s.check() == sat: # 해가 존재하는지 확인
    m = s.model() # 값을 담는 객체 변수 생성
    
    for i in input_data:
    	# m[i]: 미지수 i에 해당하는 Z3 정답 객체
        # .as_long(): Z3 객체를 파이썬 정수로 변환
        # chr(): 정수를 아스키 문자로 변환
        print(chr(m[i].as_long()), end='')

z3를 활용한 파이썬 코드입니다.