247CTF - Flag Keygen

Posted on In Views: Disqus: Word count in article: 490 Reading time ≈ 2 mins.

We created a service which can read and print the flag for you. To use the application, you first need to enter a valid product key. Can you reverse the algorithm and generate a valid key?

Reversing

The binary reads a product key, validates it, and prints the flag only if validation succeeds.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
int __fastcall main(int argc, char **argv, char **envp)
{
  int is_valid;
  char input_key[136];

  setbuf(stdout, 0);
  memset(input_key, 0, 129);
  puts("Enter a valid product key to gain access to the flag:");
  fgets(input_key, 128, stdin);
  input_key[strcspn(input_key, "\n")] = 0;

  is_valid = validate_product_key(input_key);
  if (is_valid)
  {
    puts("Valid product key!");
    print_flag_file();
  }
  else
  {
    puts("Invalid product key!");
  }

  return 0;
}

bool __fastcall validate_product_key(const char *product_key)
{
  int i;
  int checksum;

  if (strlen(product_key) != 32)
    return 0;

  // Allowed characters: 0x40..0x5A ('@'..'Z')
  for (i = 0; i < strlen(product_key); ++i)
  {
    if (product_key[i] <= 63 || product_key[i] > 90)
      return 0;
  }

  checksum = 247;
  for (i = 1; i < strlen(product_key); ++i)
    checksum += transform_char(product_key[i]) - i + 247;

  return checksum % 248 == transform_char(product_key[0])
      && checksum % 248 == 247;
}

int __fastcall transform_char(unsigned __int8 ch)
{
  if ((char)ch <= 'M')
    return (char)ch + 181;
  return (char)ch + 177;
}

From validate_product_key:

  • Key length must be exactly 32.
  • Each character must be in 0x40..0x5A (@ to Z).
  • Final condition enforces checksum % 248 == 247.
  • Also, transform_char(key[0]) must equal that same value.

Because transform_char(c) == 247 only when c == 'B', the first character is fixed to B.

Z3 solver

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
from z3 import *
from z3 import BitVec, BitVecVal, If, Solver, ZeroExt, sat

s = Solver()

# 1. 定义 32 个 8-bit 的符号变量（代表字符）
flag = [BitVec(f"flag[{i}]", 8) for i in range(32)]


# 2. 施加字符集约束 ('@' to 'Z')
for i in range(32):
    # Integer Promotion converts c to a 32-bit integer = 8 bits(char) + 24 bits
    s.add(flag[i] >= 65, flag[i] <= 90)


# 3. 核心转换逻辑 (transform_char)
def transform(c):
    # z3 的 If 语法：If(条件, 真值, 假值)
    return If(c <= 77, ZeroExt(24, c) + 181, ZeroExt(24, c) + 177)


# 4. 累加校验和计算
# 使用 32-bit 位向量防止整数溢出，就像 C 语言里的 int 一样
# Integer Promotion converts c to a 32-bit integer = 8 bits(char) + 24 bits
checksum = BitVecVal(247, 32)
for i in range(1, 32):
    checksum += transform(flag[i]) - i + 247

s.add(checksum % 248 == 247)
s.add(checksum % 248 == transform(flag[0]))

if s.check() == sat:
    model = s.model()
    # 提取计算出的字符并拼接
    flag = "".join(chr(model[flag[i]].as_long()) for i in range(32))
    print(f"[+] Valid Product Key: {flag}")

Solver output:

1
BUYRSCLZHPATAQZSLJMJMKOOBFRAOVUX

Remote verification

1
nc 892dc593a381aaea.247ctf.com 50478
1
2
3
4
Enter a valid product key to gain access to the flag:
BUYRSCLZHPATAQZSLJMJMKOOBFRAOVUX
Valid product key!
247CTF{********************************}
247CTF{fb88b9fe80e969e73a27541f62d6f89c}