[Dreamhack] verify

https://dreamhack.io/wargame/challenges/772

verify

리버싱 문제

조금 난이도 있는 리버싱 문제는 처음 도전해본다....한번 가보자고

시리얼을 입력받고 검증하는 프로그램 -> crack me 시리즈가 떠오른다. 

파일을 다운받아보자.

elf 64비트 프로그램

wsl에서 돌려보면 시리얼 값을 받는 입력칸이 나온다.

아마 올바른 시리얼 입력값 or 올바른 시리얼 입력값을 쳤을 때 플래그가 나오거나 할 듯

 

 

Decompiled code

main

__int64 __fastcall main(int a1, char **a2, char **a3)
{
  printf("%s", off_4048);
  __isoc99_scanf("%256s", s);
  sub_165C();
  if ( !sub_160A() )
  {
    puts(off_4058);
    exit(0);
  }
  puts(off_4050);
  return 0LL;
}

사용자로부터 scanf 함수로 입력값을 받고있다.

sub165C() 함수 호출 후, sub_160A() 함수에서 값이 올바른지 올바르지 않은지 확인하고 있다.

만약 올바른 값이면 -> off_4050 변수에 저장된 값을 출력하는듯?

선언된 변수 목록으로, sub_160A에서 검증하는게 맞는듯

 

sub_160A()

_BOOL8 sub_160A()
{
  if ( !sub_1395() )
    return 0LL;
  if ( (unsigned __int8)sub_11D6() != 1 )
    return 0LL;
  return sub_14B6();
}

서브루틴이 3개나 존재한다.

- sub_1395

- sub_11D6

- sub_14B6

c/c++ 에서 1 = true, 0 = false라는 것을 생각해 볼 때, sub_1395 함수랑 sub_11D6 함수 조건문을 넘기고, sub_14B6 함수에서 return 값으로 true or 1을 가져야 한다.

일단 첫번째 서브루틴부터 살펴보자.

 

sub_1395

_BOOL8 sub_1395()
{
  return strlen(s) == 43;
}

 

시리얼의 길이가 43인지 확인하고 있다.

sub_11D6

__int64 sub_11D6()
{
  int v1; // [rsp+8h] [rbp-18h]
  int n; // [rsp+Ch] [rbp-14h]
  int m; // [rsp+10h] [rbp-10h]
  int k; // [rsp+14h] [rbp-Ch]
  int j; // [rsp+18h] [rbp-8h]
  int i; // [rsp+1Ch] [rbp-4h]

  for ( i = 0; i <= 2; ++i )
  {
    if ( off_4060[i] != s[i] )
      return 0LL;
  }
  if ( byte_40AB != 45 )
    return 0LL;
  if ( byte_40B6 != 45 )
    return 0LL;
  if ( byte_40C1 != 45 )
    return 0LL;
  if ( byte_40CA != 125 )
    return 0LL;
  v1 = strlen(s);
  for ( j = 3; j <= 10 && j < v1; ++j )
  {
    if ( !sub_1199(s[j]) )
      return 0LL;
  }
  for ( k = 12; k <= 21 && k < v1; ++k )
  {
    if ( !sub_1199(s[k]) )
      return 0LL;
  }
  for ( m = 23; m <= 32 && m < v1; ++m )
  {
    if ( !sub_1199(s[m]) )
      return 0LL;
  }
  for ( n = 34; n < v1 - 1; ++n )
  {
    if ( !sub_1199(s[n]) )
      return 0LL;
  }
  return 1LL;
}

 

시리얼 포맷 검증

하나하나 살펴보자.

 

• 시리얼 조건
  • **"DH{"**로 시작 (3글자)
  • 특정 위치(3, 11, 22, 33)의 문자가 '-'
  • 마지막(42번째 위치)에 '}'로 끝남
• sub_1199도 살펴보자

sub_1199

 

_BOOL8 __fastcall sub_1199(char a1)
{
  if ( a1 <= 47 )
    return 0LL;
  if ( a1 <= 70 || a1 > 90 )
    return a1 <= 102;
  return 0LL;
}

3~10, 12~21, 23~32, 34~41번째에 오는 문자열들은 아스키 코드 48 ~ 70 사이, 또는 91 ~ 102 사이에 있어야 한다.

즉 범위는 다음과 같다.

(챗 지피티의 도움을 받았습니다.)

48~57	0 1 2 3 4 5 6 7 8 9
58~64	: ; < = > ? @
65~70	A B C D E F
91~96	Z [ \ ] ^ _ \ `
97~102	a b c d e f

※ 0123456789:;<=>?@ABCDEFZ[\]^_`abcdef

즉, 올바른 시리얼 값 = 플래그

대강 플래그 형식은 DH{~} 이렇게 될 것이고, 영문자와 숫자로 이루어져 있을 것이다.

 

sub_14B6

_BOOL8 sub_14B6()
{
  __int64 v1; // [rsp+8h] [rbp-38h]
  __int64 v2; // [rsp+10h] [rbp-30h]
  __int64 v3; // [rsp+18h] [rbp-28h]
  __int64 v4; // [rsp+20h] [rbp-20h]
  char *v5; // [rsp+28h] [rbp-18h]
  char *dest; // [rsp+30h] [rbp-10h]

  dest = (char *)calloc(1uLL, 8uLL);
  v5 = (char *)calloc(1uLL, 0xAuLL);
  strncpy(dest, src, 8uLL);
  v4 = sub_13BC(dest);
  strncpy(v5, byte_40AC, 0xAuLL);
  v3 = sub_13BC(v5);
  strncpy(v5, byte_40B7, 0xAuLL);
  v2 = sub_13BC(v5);
  strncpy(dest, byte_40C2, 8uLL);
  v1 = sub_13BC(dest);
  if ( !sub_16F4(v4, v3, v2) )
    return 0LL;
  if ( !sub_177C(v2, v1) )
    return 0LL;
  return sub_17AE(v4, v3, v2, v1);
}

시리얼을 '-' 기준으로 4가지 부분으로 나누고 있다.

각 부분을 part1, part2, part3, part4... 이렇게 할당한다고 할 때, 아래와 같은 수학적 검증을 통과해야 한다.

 

• part1 + part2 == 0xA255CEA0BA 
• part2 + part3 == 0xC4259FEEE3
• part3 + part4 == 0x2284419047 
• part1 + part4 == 3027255838
• (part4 ^ part3 ^ part2) == 0x8391639987 

 

 

sub_13BC

__int64 __fastcall sub_13BC(const char *a1)
{
  char *s; // [rsp+8h] [rbp-18h]
  int v3; // [rsp+10h] [rbp-10h]
  int i; // [rsp+14h] [rbp-Ch]
  __int64 v5; // [rsp+18h] [rbp-8h]

  s = (char *)a1;
  v5 = 0LL;
  v3 = strlen(a1);
  for ( i = 0; i < v3; ++i )
  {
    if ( *s <= 47 || *s > 57 )
    {
      if ( *s <= 64 || *s > 70 )
      {
        if ( *s > 96 && *s <= 102 )
          v5 = 16 * v5 + *s - 87;
      }
      else
      {
        v5 = 16 * v5 + *s - 55;
      }
    }
    else
    {
      v5 = 16 * v5 + *s - 48;
    }
    ++s;
  }
  return v5;
}

입력된 문자열을 16진수로 해석 후, 수학적 검증을 거친 후 정수로 변환한 값을 반환하고 있다.

수학적 검증 -> 입력값으로 받는 문자열이 16진수의 범위(0-9, a-f)에 포함되는지 확인하고 있다.

만약 범위에 포함되지 않는다면 (예를 들어 z라는 문자가 들어왔다면) 아예 제외시켜버리는듯

예를 들어 1687z 라는 문자열이 들어오면 -> 16진수로 처리하기 위해 0x1687 이런 식으로 변환한다. (아예 문자 제외)

(s <= 47 || s > 102 에서 자동적으로 걸러져서 리턴됨)

 

exploit code

from z3 import *

# Z3 변수 정의 (64비트 정수형으로 표현)
Part1 = BitVec('Part1', 64)
Part2 = BitVec('Part2', 64)
Part3 = BitVec('Part3', 64)
Part4 = BitVec('Part4', 64)

# z3 Solver 초기화
solver = Solver()

# 식 정의
solver.add(Part1 + Part2 == 0xA255CEA0BA)  # Part1 + Part2 = 17699680141370
solver.add(Part2 + Part3 == 0xC4259FEEE3)  # Part2 + Part3 = 20205008432355
solver.add(Part3 + Part4 == 0x2284419047)  # Part3 + Part4 = 936518515911
solver.add(Part1 + Part4 == 0xB470421E)    # Part1 + Part4 = 3027255838
solver.add((Part4 ^ Part3 ^ Part2) == 0x8391639987)  # xor 조건



# 풀이
if solver.check() == sat:  # 원하는 값을 찾았을 경우
    model = solver.model()
    part1 = model[Part1].as_long() # z3 변수값을 파이썬 변수로 변환
    part2 = model[Part2].as_long()
    part3 = model[Part3].as_long()
    part4 = model[Part4].as_long()

    # 시리얼을 소문자로 변환 -> 나중에 dh는 DH로
    flag = f"DH{{{part1:04X}-{part2:010X}-{part3:010X}-{part4:010X}}}".lower()
    print(flag)
else:
    print("error")

z3 solver 안쓰면 아예 답 출력이 안됨...

참고로, Part4의 값에서 00은 제외시켜줘야 한다.

플래그 결과값은 

※ z3 - solver

https://github.com/Z3Prover/z3

GitHub - Z3Prover/z3: The Z3 Theorem Prover

여러 복잡하고 시간이 오래 걸리는 수식을 풀어주는 SMT solver(쉽게 말해서 수식을 만족하는 값이 존재하는지 찾아준다고 생각하면 됨) 모듈