ACTF 2025

import numpy as np
from sympy import Matrix, gcd
from z3 import *

"""

Step 1: RC4

"""

def rc4(key: bytes, l) -> bytes:
    
    # Key Scheduling Algorithm (KSA)
    S = list(range(256))
    j = 0
    for i in range(256):
        j = (j + S[i] + key[i % len(key)]) % 256
        S[i], S[j] = S[j], S[i]

    # Pseudo-Random Generation Algorithm (PRGA) 
    i = 0
    j = 0
    result = []
    for _ in range(l):
        i = (i + 1) % 256
        j = (j + S[i]) % 256
        S[i], S[j] = S[j], S[i]
        k = S[(S[i] + S[j]) % 256]
        result.append(k)
    return bytes(result)

cypher_values = [
    0xAD, 0x00, 0xC0, 0x9F, 0x16, 0x17, 0xEC, 0x25, 0x25, 0x1F,
    0x12, 0xE2, 0x7F, 0x9F, 0x37, 0x53, 0x12, 0xBA, 0x8D, 0x38,
    0x60, 0x14, 0x1B, 0x31, 0x8E, 0x13, 0xE2, 0x56, 0x0A, 0x1A,
    0x25, 0xB9, 0x80, 0x73, 0x8A, 0x60
]

key = bytes([ord(c) for c in "eclipsky"])
keystream = rc4(key, len(cypher_values))

ae = [(c - k) % 256 for c, k in zip(cypher_values, keystream)]

"""

# Step 2: Invert AD matrix modulo 256

"""

ad_columns = [
    [116, 11, 98, 31, 235, 15],
    [174, 193, 214, 30, 25, 191],
    [193, 115, 197, 117, 244, 119],
    [124, 4, 145, 15, 202, 140],
    [102, 127, 97, 230, 73, 94],
    [100, 139, 151, 179, 222, 32]
]

ad_matrix = np.array(ad_columns).T.tolist()
sympy_matrix = Matrix(ad_matrix)
det = sympy_matrix.det() % 256

if gcd(det, 256) != 1:
    raise ValueError("Matrix not invertible modulo 256")

inv_det = pow(int(det), -1, 256)
inv_matrix = (sympy_matrix.adjugate() * inv_det) % 256
inv_np = np.array(inv_matrix.tolist(), dtype=int) % 256

# Compute AC = AE * inv(AD) mod 256
ae_2d = np.array(ae).reshape(6, 6)
ac_2d = np.dot(ae_2d, inv_np) % 256
ac = ac_2d.flatten().tolist()

"""

Step 3: Set up Z3 solver with variable flag length constraints

"""

s = Solver()
aa = [BitVec(f'aa_{i}', 8) for i in range(39)]

# Fix the prefix "ACTF{"
prefix = [ord(c) for c in "ACTF{"]
for i in range(5):
    s.add(aa[i] == prefix[i])
    
# Enforce flag ends with '}' and is followed by zeros
s.add(Or([aa[i] == ord('}') for i in range(5, 39)]))  # At least one '}'
s.add(Sum([If(aa[i] == ord('}'), 1, 0) for i in range(5, 39)]) == 1)  # Exactly one '}'

# Convolution equations for AC (36 equations)
for i in range(36):
    term = (11 * aa[i] + 4 * aa[i + 1] + 5 * aa[i + 2] + 14 * aa[i + 3]) % 256
    s.add(ac[i] == term)

if s.check() == sat:
    model = s.model()
    flag_bytes = [model[aa[i]].as_long() for i in range(39)]
    print(bytes(flag_bytes))
else:
    print("No solution found")
# ACTF{RC4_4nd_FPGA_w4lk_1nt0_4_b4r}

// part_3.cpp
#include <cstdint>
#include <vector>
#include <fstream>
#include <omp.h>
#include <iostream>
#include <cassert>
#define DEBUG

uint8_t SBOX[256] = { ... };

uint8_t TBOX[256] = { ... };

uint8_t INVSBOX[256];
void compute_inv()
{
    for (int i = 0; i < 256; i++)
        INVSBOX[SBOX[i]] = i;
}

static uint8_t kernel(int i, uint8_t b3)
{
    uint8_t bid = i / 256;
    uint8_t tid = i % 256;
    uint8_t key = bid ^ tid;
    uint8_t b1, b2;

    for (int j = 4137822; j >= 8; j--)
    {
        b2 = INVSBOX[b3] ^ TBOX[j & 0xFF];
        b1 = (b2 - key) * 197;
        b3 = (b1 << 5) | (b1 >> 3); // rotate right 3
    }

    return b3;
}

int main()
{
    compute_inv();
    std::ifstream in_file("deep_flag.bin", std::ios::binary);

    #ifdef DEBUG
    assert(in_file.is_open());
    #endif

    in_file.seekg(0, std::ios::end);
    size_t file_size = in_file.tellg();

    #ifdef DEBUG
    assert(file_size == 256 * 256);
    #endif

    in_file.seekg(0, std::ios::beg);

    std::vector<uint8_t> input_data(file_size);
    in_file.read(reinterpret_cast<char *>(input_data.data()), file_size);
    in_file.close();

    const uint8_t *input = input_data.data();
    std::vector<uint8_t> output(256 * 256);

#pragma omp parallel for schedule(static)
    for (int i = 0; i < 256 * 256; ++i)
    {
        output[i] = kernel(i, input[i]);
    }

    std::ofstream out_file("part_3_in.bin", std::ios::binary);
    out_file.write(reinterpret_cast<const char *>(output.data()), output.size());
    out_file.close();

    return 0;
}
// Usage: g++ .\part_3.cpp -o part_3.exe -fopenmp -std=c++17 -O2 -Wall

# part_2.sage
import functools as ft

import tqdm
from sage.all import *

# fmt: off
SBOX = bytes([ ... ])
# SBOX_INV = bytes(SBOX.index(i) for i in range(256))
TBOX = bytes([ ... ])
# TBOX_INV = bytes((TBOX.index(i) for i in range(256)))
# fmt: on

THREADS_PER_BLOCK = 256

Zmod256 = Integers(256)

# @ft.cache
def get_coeff(thread_id: int):
    s = SBOX[thread_id]
    coeffs = []
    for _ in range(THREADS_PER_BLOCK):
        coeffs.append(TBOX[s & 0xFF])
        s = ((s * 5) + 17) & 0xFF
    return vector(Zmod256, coeffs)


# @ft.cache
def get_coeff_mat():
    rows = []
    for j in range(THREADS_PER_BLOCK):
        rows.append(get_coeff(j))
    return Matrix(Zmod256, rows)


with open("part_3_in.bin", "rb") as f:
    in_buf = f.read()

assert len(in_buf) % THREADS_PER_BLOCK == 0

results = []
mat_a = get_coeff_mat()

for i in tqdm.tqdm(range(len(in_buf) // THREADS_PER_BLOCK)):
    vec_b = vector(Zmod256, in_buf[i * THREADS_PER_BLOCK : (i + 1) * THREADS_PER_BLOCK])
    vec_x = mat_a.solve_right(vec_b)
    results.extend(vec_x)

with open("part_2_in.bin", "wb") as f:
    f.write(bytes(results))

// part_1.cpp
#include <stdio.h>
#include <cstdint>
#include <vector>
#include <iostream>
#include <fstream>
#include <cassert>
#define DEBUG

const uint32_t K0 = 1386807340;
const uint32_t K1 = 2007053320;
const uint32_t K2 = 621668851;
const uint32_t K3 = -862448841;

void tea_kernel(uint32_t v[2]) {
    uint32_t v0 = v[0], v1 = v[1], delta = -1708609273, sum = 1786956040 + delta * 3238567;
    for (int i = 0; i < 3238567; i++) {
        sum -= delta;
        v0 += ((v1 << 4) + K2) ^ (v1 + sum) ^ ((v1 >> 5) + K3);
        v1 -= ((v0 << 4) + K0) ^ (v0 + sum) ^ ((v0 >> 5) + K1);
    }
    v[0] = v0;
    v[1] = v1;
}

int main(){
    
    std::ifstream in_file("part_2_in.bin", std::ios::binary);

    #ifdef DEBUG
    assert(in_file.is_open());
    #endif

    in_file.seekg(0, std::ios::end);
    size_t file_size = in_file.tellg();
    in_file.seekg(0, std::ios::beg);

    #ifdef DEBUG
    assert(file_size == 256 * 256);
    assert(in_file.tellg() == 0);
    #endif

    std::vector<uint8_t> input(file_size);

    in_file.read(reinterpret_cast<char *>(input.data()), file_size);
    in_file.close();

    uint8_t *input_ptr = input.data();

// Granularity: BYTE
#pragma omp parallel for schedule(static)
    for(size_t i = 0; i < file_size; i++){
        uint8_t bid = i / 256;
        uint8_t tid = i % 256;
        input_ptr[i] ^= bid & tid;
    }

// Granularity: QWORD
#pragma omp parallel for schedule(static)
    for(size_t i = 0; i < file_size; i += 8){
        tea_kernel((uint32_t *)&input_ptr[i]);
    }

// Granularity: BYTE    
#pragma omp parallel for schedule(static)
    for(size_t i = 0; i < file_size; i++){
        uint8_t bid = i / 256;
        uint8_t tid = i % 256;
        input_ptr[i] ^= bid | tid;
    }

    std::ofstream out_file("part_1_in.bin", std::ios::binary);

    out_file.write(reinterpret_cast<char *>(input_ptr), file_size);

    return 0;
}

# format_IDA_data.py
import re
import struct

def parse_rodata_floats(data_string):
    """
    Parses a string containing .rodata definitions and extracts float values.

    Args:
        data_string: A multiline string containing the .rodata dump.

    Returns:
        A list of floats extracted from the data.
    """
    all_floats = []
    lines = data_string.strip().split('\n')

    for line_number, line in enumerate(lines, 1):
        # Look for lines containing 'dd ' which signifies data definition
        if 'dd ' not in line:
            continue

        try:
            # Split by 'dd ' and take the second part
            data_part = line.split(' dd ', 1)[1]
            
            # Remove comments if any (stuff after ';')
            if ';' in data_part:
                data_part = data_part.split(';', 1)[0]

            potential_floats = data_part.split(',')
            for val_str in potential_floats:
                cleaned_val_str = val_str.strip()
                if cleaned_val_str: 
                    try:
                        all_floats.append(float(cleaned_val_str))
                    except ValueError:
                        print(f"Warning (line {line_number}): Could not convert '{cleaned_val_str}' to float from: \"{line.strip()}\"")
        except IndexError:
            print(f"Warning (line {line_number}): Malformed line or unexpected structure after 'dd ': \"{line.strip()}\"")
            continue
            
    return all_floats

def save_floats_to_file(floats_list, output_filename):
    """
    Saves a list of floats to a text file, one float per line.

    Args:
        floats_list: A list of float numbers.
        output_filename: The name of the file to save the floats to.

    Returns:
        True if saving was successful, False otherwise.
    """
    write_buf = []
    with open(output_filename, 'w') as f:
        for item in floats_list:
            write_buf.append(str(item))
        f.write(', '.join(write_buf))
    print(f"Successfully saved {len(floats_list)} numbers to '{output_filename}'")
    return True

# The data provided by the user
rodata_input = """
.rodata:0000000000483020 _ZL6motion      dd 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.012483786, 0.042622309
...
.rodata:00000000004833E0                 dd 0.0, 0.0055596731, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0
"""

if __name__ == "__main__":
    # Parse the data
    print("Parsing rodata input...")
    extracted_floats = parse_rodata_floats(rodata_input)
    
    if extracted_floats:
        print(f"Successfully parsed {len(extracted_floats)} numbers.")
        
        # Define the output filename
        output_file = "extracted_data.txt"
        
        # Save the floats to the text file
        save_floats_to_file(extracted_floats, output_file)
    else:
        print("No floats were extracted from the input.")