콘텐츠로 건너뛰기

verify

Description

시리얼을 입력받고 간단하게 검증하는 프로그램입니다. 바이너리를 분석하여 플래그를 획득해 보세요! (플래그는 소문자 입니다!)

Files

ubuntu@WSL2:~/CTF/dreamhack.io$ tree verify
verify
└── verify

0 directories, 1 files

ubuntu@WSL2:~/CTF/dreamhack.io$ file verify/verify
verify/verify: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=fec3a94951ab800a54a080e822ffd7750412b1b8, for GNU/Linux 3.2.0, stripped

64비트 리눅스용 실행 파일 하나.


분석

main

__int64 __fastcall main(int a1, char **a2, char **a3)
{
  printf("verify serial: ");
  __isoc99_scanf("%256s", s);
  if ( !sub_55984656D612() )
  {
    puts("Not Verified...");
    exit(0);
  }
  puts("Verified");
  return 0LL;
}

사용자로부터 serial 값을 입력받으면,
sub_55984656D612 함수에서 값을 확인한다. 맞으면 1을 반환시킨다.


sub_55984656D612

_BOOL8 sub_55984656D612()
{
  if ( !sub_55984656D395() )
    return 0LL;
  if ( (unsigned __int8)sub_55984656D1D6() != 1 )
    return 0LL;
  return (unsigned __int8)sub_55984656D4B6();
}

sub_55984656D395, sub_55984656D1D6, sub_55984656D4B6 총 3가지 함수에서 확인 작업을 한다.
각 함수 전부다 1을 반환시켜야 된다.

하나씩 차례대로 살펴보자


sub_55984656D395

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

입력받은 문자열 크기가 43인지 확인한다.


sub_55984656D1D6

__int64 sub_55984656D1D6()
{
  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_559846570060[i] != s[i] )// DH{
      return 0LL;
  }
  if ( byte_5598465700AB != '-' )
    return 0LL;
  if ( byte_5598465700B6 != '-' )
    return 0LL;
  if ( byte_5598465700C1 != '-' )
    return 0LL;
  if ( byte_5598465700CA != '}' )
    return 0LL;
  v1 = strlen(s);
  for ( j = 3; j <= 10 && j < v1; ++j )
  {
    if ( !sub_55984656D199(s[j]) )
      return 0LL;
  }
  for ( k = 12; k <= 21 && k < v1; ++k )
  {
    if ( !sub_55984656D199(s[k]) )
      return 0LL;
  }
  for ( m = 23; m <= 32 && m < v1; ++m )
  {
    if ( !sub_55984656D199(s[m]) )
      return 0LL;
  }
  for ( n = 34; n < v1 - 1; ++n )
  {
    if ( !sub_55984656D199(s[n]) )
      return 0LL;
  }
  return 1LL;
}
_BOOL8 __fastcall sub_55984656D199(char a1)
{
  if ( a1 <= 47 )
    return 0LL;
  if ( a1 <= 70 || a1 > 90 )
    return a1 <= 102;
  return 0LL;
}

우선 입력받은 문자열이 DH{로 시작하는지 확인한다.

그리고 11, 22, 33번째 인덱스의 문자가 전부 ‘‘인지 확인하고, 42번째 인덱스의 문자가 ‘}‘인지 확인한다.

마지막으로 3~10, 12~21, 23~32, 34~41번째 인덱스에 있는 문자를 아스키 코드로 나타냈을때
48~70 또는 90~102 사이에 있어야 된다.

문자로 나타냈을때 범위는 0123456789:;<=>?@ABCDEF 또는 Z[]^_`abcdef 문자 중 하나가 되겠다.


sub_55984656D4B6

__int64 sub_55984656D4B6()
{
  __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]
  bool v7; // [rsp+3Fh] [rbp-1h]

  dest = (char *)calloc(1uLL, 8uLL);
  v5 = (char *)calloc(1uLL, 10uLL);
  strncpy(dest, src, 8uLL);
  v4 = sub_55984656D3BC(dest);
  strncpy(v5, unk_5598465700AC, 10uLL);
  v3 = sub_55984656D3BC(v5);
  strncpy(v5, unk_5598465700B7, 10uLL);
  v2 = sub_55984656D3BC(v5);
  strncpy(dest, unk_5598465700C2, 8uLL);
  v1 = sub_55984656D3BC(dest);
  if ( !sub_55984656D6FC(v4, v3, v2) )
    return 0LL;
  v7 = sub_55984656D784(v2, v1);
  if ( !v7 )
    return 0LL;
  if ( sub_55984656D7B6(v4, v3, v2, v1) )
    return 1LL;
  return v7;
}
__int64 __fastcall sub_55984656D3BC(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 = 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;
}

입력받은 문자열이 DH{XXXXXXXX-YYYYYYYYYY-ZZZZZZZZZZ-QQQQQQQQ}로 가정했을때,

XXXXXXXX-> src,
YYYYYYYYYY-> unk_5598465700AC,
ZZZZZZZZZZ-> unk_5598465700B7,
QQQQQQQQ-> unk_5598465700C2
가 각각 들어가있고 strncpy해서 sub_55984656D3BC 함수로 넘겨준다.

그 함수에서는 문자값을 무언가(?)로 변환시키는데,
문자가 전부다 16진수 값 범위(0~9, A~F)면 그걸 16진수 값으로 변환시켜주지만,
한 인덱스의 문자가 그 범위 밖이면 변환없이 그냥 넘기는 듯하다.
(파이썬3으로도 구현시켜봤는데 맨 끝에 있음)

이를 테면,
문자값이 “ABCDEF01″이면 숫자인 0xabcdef01을 반환시키고,
문자값이 “ABCDEF<>”이면 0xabcdef,
문자값이 “ABCD><10″이면 0xabcd10 이렇게 나온다.

XXXXXXXX, YYYYYYYYYY, ZZZZZZZZZZ, QQQQQQQQ를 sub_55984656D3BC 함수에 넘기고 난 후의 리턴값을
다시 code1, code2, code3, code4로 각각 가정을 하면,

sub_55984656D6FC, sub_55984656D784, sub_55984656D7B6에서 각 code값을 확인하는데
다음과 같은 조건을 만족시켜야 되었다.

  1. code1 + code2 == 0xA255CEA0BA && code2 + code3 == 0xC4259FEEE3,
  2. code3 + code4 == 0x2284419047
  3. code1 + code4 == 0xB470421E && (code2 ^ code3 ^ code4) == 0x8391639987

Solution

from z3 import *

code1 = BitVec('code1', 64)
code2 = BitVec('code2', 64)
code3 = BitVec('code3', 64)
code4 = BitVec('code4', 64)

equations = [
    code1 + code2 == 0xA255CEA0BA,
    code2 + code3 == 0xC4259FEEE3,
    code3 + code4 == 0x2284419047,
    code1 + code4 == 0xB470421E,
    code2 ^ code3 ^ code4 == 0x8391639987
]

solver = Solver()

for equation in equations:
    solver.add(equation)

solutions = []
while solver.check() == sat:
    model = solver.model()
    solution = {
        'code1': model[code1].as_long(),
        'code2': model[code2].as_long(),
        'code3': model[code3].as_long(),
        'code4': model[code4].as_long(),
    }
    solutions.append(solution)
    solver.add(Or(code1 != model[code1], code2 != model[code2], code3 != model[code3], code4 != model[code4]))

for i, solution in enumerate(solutions):
    print(f"Solution {i + 1}:")
    for var_name, value in solution.items():
        print(f"{var_name}: {hex(value)}")
    print()
PS Microsoft.PowerShell.Core\FileSystem::\\wsl.localhost\Ubuntu\home\ubuntu\CTF\dreamhack.io\verify> python3 solve.py
Solution 1:
code1: 0x62f0aaba
code2: 0xa1f2ddf600
code3: 0x2232c1f8e3
code4: 0x517f9764

각 code 값들은 python3 z3 모듈을 사용하여 덕분에 쉽게 풀 수 있었다.

ubuntu@WSL2:~/CTF/dreamhack.io/verify$ ./verify
verify serial: DH{62f0aaba-a1f2ddf600-2232c1f8e3-517f9764}
Verified

FLAG

DH{62f0aaba-a1f2ddf600-2232c1f8e3-517f9764}


sub_55984656D3BC를 파이썬으로 구현시킨 코드

def verify_convert(word):
    result = 0
    for i in range(len(word)):
        oneWord = ord(word[i])
        if(oneWord <= 47 or oneWord > 57):
          if(oneWord <= 64 or oneWord > 70):
             if(oneWord > 96 and oneWord <= 102):
                result = 16 * result + oneWord - 87; 
          else:
            result = 16 * result + oneWord - 55
        else:
           result = 16 * result + oneWord - 48

    return result

print(hex(verify_convert("ABCD><10")))
태그:

답글 남기기