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값을 확인하는데
다음과 같은 조건을 만족시켜야 되었다.
- code1 + code2 == 0xA255CEA0BA && code2 + code3 == 0xC4259FEEE3,
- code3 + code4 == 0x2284419047
- 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")))
