247CTF - Flag Keygen

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!");
26 collapsed lines
  }

  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 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}")

BUYRSCLZHPATAQZSLJMJMKOOBFRAOVUX

Enter a valid product key to gain access to the flag:
BUYRSCLZHPATAQZSLJMJMKOOBFRAOVUX
Valid product key!
247CTF{<flag-redacted>}