The Plank
by Sean
rev
500 pts
You have been forced to walk the plank. There are rumors of some who have survived, but those are only rumors... right?
The flag is in the format BCCTF{.*} This challenge only works on python3.12
Step 1: Deobfuscation
The challenge file plank.py is a single obfuscated line:
print('You Made IT!!!!'if bytes([state:=[lambda x,y:[x[i]^x[(i+y)%len(x)] for i in range(len(x))],lambda x,y:[x[(i+y)%len(x)] for i in range(len(x))],lambda x,y:[x[i]^y for i in range(len(x))],lambda x,y:[x[i]*y%256 for i in range(len(x))],lambda x,y:[(x[i]+y)%256 for i in range(len(x))]][2*j%5](state if'state'in dir()else input('Walk the plank!\n').encode(),140*j+133)for j in range(100)][-1])==b'c\xc9\xa2+\xcf\xef\xd4+\xeb\x83w&\xe7\xfd\t\xde\xf3\xe5\xdeO\x13\x0bl\xb7\x1b\xab\x0f\x8a\x13\xc5\xfd\x92'else'Splash!!!')
This requires Python 3.12 due to PEP 709 (inlined comprehensions), which makes the walrus operator (:=) visible to dir() within list comprehensions.
Deobfuscated, it applies 100 sequential transformations to the 32-byte input, cycling through 5 operations selected by (2*j) % 5 with parameter y = 140*j + 133:
| Op | (2*j)%5 |
Operation | Description |
|---|---|---|---|
| 0 | 0 | new[i] = old[i] ^ old[(i+y)%32] |
XOR with shifted self |
| 1 | 2 | new[i] = old[i] ^ y |
XOR with constant |
| 2 | 4 | new[i] = (old[i] + y) % 256 |
Add constant mod 256 |
| 3 | 1 | new[i] = old[(i+y)%32] |
Rotation/permutation |
| 4 | 3 | new[i] = old[i] * y % 256 |
Multiply mod 256 |
The cycle repeats 20 times (100 steps / 5 ops). The result must equal a 32-byte target.
Step 2: Initial Analysis
Key observations:
- Flag format: BCCTF{...} -- 7 known bytes (positions 0-5 and 31), 25 unknown
- All multiply constants are odd (y mod 4 = 1 for all j), so multiplication is invertible mod 256
- XOR-shift is the only non-invertible operation: the matrix I + P^s over GF(2) has rank 31 (kernel = all-ones vector), since gcd(s, 32) = 1 for all shifts
- 20 XOR-shift steps compound the rank deficiency: the composed GF(2) transformation matrix A has rank 12 out of 32 (kernel dimension 20)
Step 3: Failed Approaches
Z3 SMT Solving (Multiple Variants)
- Direct expressions (no intermediate variables,
Then('simplify', 'bit-blast', 'sat')tactic): Timed out at 10 minutes -- expressions too deeply nested - Intermediate variables at each step with bit-blast tactic: Also timed out
- Chain-structured with variables only at XOR-shift boundaries: Timed out at 3 minutes
Direct SAT Encoding (pysat)
- Manually encoded the Boolean circuit (XOR gates, ripple-carry adders, shift-and-add multipliers)
- CryptoMiniSat crashed; Glucose4 timed out building the circuit
Backtracking with Parity Check
- Invert the chain step-by-step, using parity constraints to prune XOR-shift inversions
- Too many valid candidates per level (4-32 instead of ~1), creating exponential search tree
Bit-Slicing GF(2) Solver (Python)
- Correct approach but had bugs with free variable enumeration
- Coupling between bit planes through carry constraints made naive enumeration fail
Step 4: The Breakthrough -- Bit-Slicing with Carry-Consistency
Core Insight: Bit-Plane Decomposition
In mod-256 arithmetic, bit k of the output depends only on bits 0..k of the input (carries propagate upward). This means we can solve 8 independent GF(2) systems, one per bit plane, from LSB to MSB.
For each bit plane k:
- The transformation is affine over GF(2): output_k = A * input_k + b_k
- Matrix A is identical for all 8 planes (only XOR-shift and rotation contribute to the linear part)
- Constant vector b_k differs per plane (carries from bits 0..k-1 in add/multiply operations)
- A has rank 12 with 25 unknowns -> 13 free variables (null space dimension) per plane
The Carry-Consistency Constraint
The null space combo at bit plane k is constrained by the consistency of the GF(2) system at bit plane k+1. The key mathematical argument:
- Flipping a null vector at bit k changes bit k of the initial flag at certain positions
- This change propagates linearly through the 100-step transformation (XOR-shift and rotation are linear; add/mul have identity linear part since all constants are odd)
- The changed intermediate states produce different carries into bit k+1
- These carry changes affect the RHS of the bit k+1 system
- The 20 redundant equations (32 equations - 12 rank) must still be satisfied -> 20 linear equations in 13 unknowns constraining the null combo
Special Structure: y mod 4 = 1
A critical discovery: since y = 140j + 133 and 140 = 0 (mod 4), 133 = 1 (mod 4), we have y mod 4 = 1 for ALL steps. This means:
- Bit 0 -> bit 1 carries cancel perfectly: Each add step's carry delta equals
A * v = 0(by definition of null space), so the bit 0 null combo is completely unconstrained by bit 1 consistency (all 8192 combos valid) - Higher bits DO provide constraints: The carry coefficient becomes a non-identity diagonal matrix (depending on lower-bit carry values), breaking the cancellation
Algorithm
1. Precompute A matrix (same for all bit planes)
2. Precompute consistency check matrix T (20 rows from RREF)
3. DFS over bit planes k = 0..7:
a. Solve A*x_k = rhs_k -> particular solution + 13 null vectors
b. For k < 7: compute carry deltas for each null vector
-> build 20x13 GF(2) system -> solve for valid combos
c. For k = 7: enumerate combos, check printability
d. Recurse to k+1 with each valid combo
The pruning is dramatic: at each level, the 20x13 system typically has rank ~13, leaving 0-16 valid combos. The search tree is narrow enough to explore completely.
Implementation in C
The Python implementation was too slow (~5 minutes for the DFS with 8192 bit-0 combos x recomputation of carries). Rewriting in C with -O2 brought the solve time to ~10 seconds.
Step 5: Solution
$ ./solve_fast
Building A matrix...
Computing consistency check matrix...
Consistency equations: 20
Starting DFS...
FLAG: BCCTF{y0U_mUs7_w4lK_A_f1N3_L1n3}
Verify: PASS
Flag
BCCTF{y0U_mUs7_w4lK_A_f1N3_L1n3}
"you must walk a fine line" -- fitting the plank-walking theme.
Solve Scripts
solve_fast.c
/*
* Fast CTF solver for the plank challenge.
* Uses bit-slicing with DFS over null space combinations.
*
* Build: gcc -O2 -o solve_fast solve_fast.c
*/
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <stdint.h>
#define N 32
#define NSTEPS 100
static const uint8_t target[N] = {
0x63, 0xc9, 0xa2, 0x2b, 0xcf, 0xef, 0xd4, 0x2b,
0xeb, 0x83, 0x77, 0x26, 0xe7, 0xfd, 0x09, 0xde,
0xf3, 0xe5, 0xde, 0x4f, 0x13, 0x0b, 0x6c, 0xb7,
0x1b, 0xab, 0x0f, 0x8a, 0x13, 0xc5, 0xfd, 0x92
};
/* Forward transformation */
void forward(const uint8_t *flag, uint8_t *out) {
uint8_t state[N];
memcpy(state, flag, N);
for (int j = 0; j < NSTEPS; j++) {
int y = 140*j + 133;
int op = (2*j) % 5;
uint8_t tmp[N];
if (op == 0) {
int s = y % N;
for (int i = 0; i < N; i++)
tmp[i] = state[i] ^ state[(i+s)%N];
memcpy(state, tmp, N);
} else if (op == 1) {
for (int i = 0; i < N; i++)
tmp[i] = state[(i+y)%N];
memcpy(state, tmp, N);
} else if (op == 2) {
uint8_t c = y & 0xFF;
for (int i = 0; i < N; i++)
state[i] ^= c;
} else if (op == 3) {
uint8_t c = y % 256;
for (int i = 0; i < N; i++)
state[i] = (uint8_t)(state[i] * c);
} else if (op == 4) {
uint8_t c = y % 256;
for (int i = 0; i < N; i++)
state[i] = (uint8_t)(state[i] + c);
}
}
memcpy(out, state, N);
}
/* GF(2) matrix-vector multiply: A is n rows, each row is a bitmask */
uint32_t mat_vec(const uint32_t *A, uint32_t v) {
uint32_t r = 0;
for (int i = 0; i < N; i++) {
if (__builtin_popcount(A[i] & v) & 1)
r |= (1u << i);
}
return r;
}
/* GF(2) matrix multiply */
void mat_mul(const uint32_t *A, const uint32_t *B, uint32_t *R) {
uint32_t BT[N] = {0};
for (int i = 0; i < N; i++)
for (int j = 0; j < N; j++)
if (B[i] & (1u<<j)) BT[j] |= (1u<<i);
for (int i = 0; i < N; i++) {
R[i] = 0;
for (int j = 0; j < N; j++)
if (__builtin_popcount(A[i] & BT[j]) & 1)
R[i] |= (1u<<j);
}
}
/* Known positions and values */
#define NUM_KNOWN 7
static const int known_pos[NUM_KNOWN] = {0, 1, 2, 3, 4, 5, 31};
static const uint8_t known_val[NUM_KNOWN] = {'B', 'C', 'C', 'T', 'F', '{', '}'};
#define NUM_UNK 25
static int unk_pos[NUM_UNK];
/* Precomputed A matrix */
static uint32_t A_mat[N];
/* Build A matrix (same for all bit planes) */
void build_A(void) {
/* Start with identity */
for (int i = 0; i < N; i++) A_mat[i] = (1u << i);
for (int j = 0; j < NSTEPS; j++) {
int y = 140*j + 133;
int op = (2*j) % 5;
if (op == 0) {
int s = y % N;
uint32_t Aj[N];
for (int i = 0; i < N; i++)
Aj[i] = (1u<<i) | (1u<<((i+s)%N));
uint32_t tmp[N];
mat_mul(Aj, A_mat, tmp);
memcpy(A_mat, tmp, sizeof(A_mat));
} else if (op == 1) {
int r = y;
uint32_t Aj[N];
for (int i = 0; i < N; i++)
Aj[i] = 1u << ((i+r)%N);
uint32_t tmp[N];
mat_mul(Aj, A_mat, tmp);
memcpy(A_mat, tmp, sizeof(A_mat));
}
}
}
/* Forward partial: compute state at bits 0..k-1 at each step */
void forward_partial(const uint8_t *flag, int mask, uint8_t history[NSTEPS+1][N]) {
uint8_t state[N];
for (int i = 0; i < N; i++) state[i] = flag[i] & mask;
memcpy(history[0], state, N);
for (int j = 0; j < NSTEPS; j++) {
int y = 140*j + 133;
int op = (2*j) % 5;
uint8_t tmp[N];
if (op == 0) {
int s = y % N;
for (int i = 0; i < N; i++)
tmp[i] = (state[i] ^ state[(i+s)%N]) & mask;
memcpy(state, tmp, N);
} else if (op == 1) {
for (int i = 0; i < N; i++)
tmp[i] = state[(i+y)%N];
memcpy(state, tmp, N);
} else if (op == 2) {
uint8_t c = y & mask;
for (int i = 0; i < N; i++)
state[i] = (state[i] ^ c) & mask;
} else if (op == 3) {
uint8_t c = y % 256;
for (int i = 0; i < N; i++)
state[i] = ((uint16_t)state[i] * c) & mask;
} else if (op == 4) {
uint8_t c = y % 256;
for (int i = 0; i < N; i++)
state[i] = ((uint16_t)state[i] + c) & mask;
}
memcpy(history[j+1], state, N);
}
}
/* Compute constant vector b for bit plane k */
uint32_t compute_b(int k, const uint8_t *flag) {
int mask = (1 << k) - 1;
uint8_t history[NSTEPS+1][N];
if (k > 0)
forward_partial(flag, mask, history);
else
memset(history, 0, sizeof(history));
uint32_t b = 0;
for (int j = 0; j < NSTEPS; j++) {
int y = 140*j + 133;
int op = (2*j) % 5;
if (op == 0) {
int s = y % N;
uint32_t Aj[N];
for (int i = 0; i < N; i++)
Aj[i] = (1u<<i) | (1u<<((i+s)%N));
b = mat_vec(Aj, b);
} else if (op == 1) {
int r = y;
uint32_t Aj[N];
for (int i = 0; i < N; i++)
Aj[i] = 1u << ((i+r)%N);
b = mat_vec(Aj, b);
} else if (op == 2) {
int y_low = y & 0xFF;
if ((y_low >> k) & 1)
b ^= 0xFFFFFFFFu;
} else if (op == 3) {
int y_mul = y % 256;
uint32_t bj = 0;
if (k > 0) {
for (int i = 0; i < N; i++) {
int val = history[j][i] * y_mul;
bj |= (((val >> k) & 1) << i);
}
}
b ^= bj;
} else if (op == 4) {
int y_add = y % 256;
int add_k = (y_add >> k) & 1;
uint32_t bj = 0;
if (k > 0) {
int y_add_low = y_add & mask;
for (int i = 0; i < N; i++) {
int carry = ((history[j][i] + y_add_low) >> k) & 1;
bj |= ((add_k ^ carry) << i);
}
} else {
if (add_k) bj = 0xFFFFFFFFu;
}
b ^= bj;
}
}
return b;
}
/* Solve GF(2) system. Returns number of free variables, fills particular[] and null_vecs[][] */
int solve_gf2(uint32_t rhs, int particular[NUM_UNK], int null_vecs[13][NUM_UNK]) {
/* Build submatrix for unknown columns */
uint32_t mat[N];
int rhs_bits[N];
for (int row = 0; row < N; row++) {
uint32_t r = 0;
for (int idx = 0; idx < NUM_UNK; idx++) {
if (A_mat[row] & (1u << unk_pos[idx]))
r |= (1u << idx);
}
mat[row] = r;
rhs_bits[row] = (rhs >> row) & 1;
}
/* Gaussian elimination */
int pivot_row[NUM_UNK];
memset(pivot_row, -1, sizeof(pivot_row));
int cur_row = 0;
for (int col = 0; col < NUM_UNK; col++) {
int piv = -1;
for (int row = cur_row; row < N; row++) {
if (mat[row] & (1u << col)) { piv = row; break; }
}
if (piv == -1) continue;
/* Swap */
uint32_t tmp_m = mat[piv]; mat[piv] = mat[cur_row]; mat[cur_row] = tmp_m;
int tmp_r = rhs_bits[piv]; rhs_bits[piv] = rhs_bits[cur_row]; rhs_bits[cur_row] = tmp_r;
pivot_row[col] = cur_row;
for (int row = 0; row < N; row++) {
if (row != cur_row && (mat[row] & (1u << col))) {
mat[row] ^= mat[cur_row];
rhs_bits[row] ^= rhs_bits[cur_row];
}
}
cur_row++;
}
/* Check consistency */
for (int row = 0; row < N; row++) {
if (mat[row] == 0 && rhs_bits[row] == 1) return -1;
}
/* Particular solution */
memset(particular, 0, NUM_UNK * sizeof(int));
for (int col = 0; col < NUM_UNK; col++) {
if (pivot_row[col] >= 0)
particular[col] = rhs_bits[pivot_row[col]];
}
/* Null space */
int free_cols[13], num_free = 0;
for (int col = 0; col < NUM_UNK; col++) {
if (pivot_row[col] < 0)
free_cols[num_free++] = col;
}
for (int fi = 0; fi < num_free; fi++) {
memset(null_vecs[fi], 0, NUM_UNK * sizeof(int));
null_vecs[fi][free_cols[fi]] = 1;
for (int col = 0; col < NUM_UNK; col++) {
if (pivot_row[col] >= 0 && (mat[pivot_row[col]] & (1u << free_cols[fi])))
null_vecs[fi][col] = 1;
}
}
return num_free;
}
/* Precomputed consistency check matrix T (rows for non-pivot equations) */
static uint32_t consistency_T[20];
static int num_consistency;
void compute_consistency_T(void) {
uint32_t mat[N];
uint32_t T[N];
for (int row = 0; row < N; row++) {
uint32_t r = 0;
for (int idx = 0; idx < NUM_UNK; idx++) {
if (A_mat[row] & (1u << unk_pos[idx]))
r |= (1u << idx);
}
mat[row] = r;
T[row] = (1u << row);
}
int cur_row = 0;
for (int col = 0; col < NUM_UNK; col++) {
int piv = -1;
for (int row = cur_row; row < N; row++) {
if (mat[row] & (1u << col)) { piv = row; break; }
}
if (piv == -1) continue;
uint32_t tmp;
tmp = mat[piv]; mat[piv] = mat[cur_row]; mat[cur_row] = tmp;
tmp = T[piv]; T[piv] = T[cur_row]; T[cur_row] = tmp;
for (int row = 0; row < N; row++) {
if (row != cur_row && (mat[row] & (1u << col))) {
mat[row] ^= mat[cur_row];
T[row] ^= T[cur_row];
}
}
cur_row++;
}
num_consistency = N - cur_row;
for (int i = 0; i < num_consistency; i++)
consistency_T[i] = T[cur_row + i];
}
/* Known column vectors for adjustment */
static uint32_t known_cols[NUM_KNOWN];
void precompute_known_cols(void) {
for (int ki = 0; ki < NUM_KNOWN; ki++) {
uint32_t col = 0;
for (int row = 0; row < N; row++) {
if (A_mat[row] & (1u << known_pos[ki]))
col |= (1u << row);
}
known_cols[ki] = col;
}
}
uint32_t get_adjusted_rhs(int k, uint32_t b_val) {
uint32_t target_bits = 0;
for (int i = 0; i < N; i++)
target_bits |= (((target[i] >> k) & 1) << i);
uint32_t rhs = target_bits ^ b_val;
for (int ki = 0; ki < NUM_KNOWN; ki++) {
if ((known_val[ki] >> k) & 1)
rhs ^= known_cols[ki];
}
return rhs;
}
/* DFS solver */
static int found = 0;
static uint8_t solution[N];
void dfs(int k, uint8_t *flag) {
if (found) return;
if (k == 8) {
/* Check printability */
for (int i = 6; i < 31; i++) {
if (flag[i] < 0x20 || flag[i] > 0x7e) return;
}
/* Verify */
uint8_t out[N];
forward(flag, out);
if (memcmp(out, target, N) == 0) {
memcpy(solution, flag, N);
found = 1;
}
return;
}
/* Compute b_k */
uint32_t b = compute_b(k, flag);
uint32_t rhs = get_adjusted_rhs(k, b);
/* Solve GF(2) system */
int particular[NUM_UNK];
int null_vecs[13][NUM_UNK];
int num_free = solve_gf2(rhs, particular, null_vecs);
if (num_free < 0) return; /* Inconsistent */
if (k < 7) {
/* Use carry-consistency to constrain null combo */
/* Apply particular solution first */
uint8_t base_flag[N];
memcpy(base_flag, flag, N);
for (int idx = 0; idx < NUM_UNK; idx++)
base_flag[unk_pos[idx]] |= (particular[idx] << k);
/* Compute b_{k+1} for base */
uint32_t b_next_base = compute_b(k+1, base_flag);
uint32_t adj_rhs_base = get_adjusted_rhs(k+1, b_next_base);
/* Compute consistency bits for base */
int cons_base[20];
for (int r = 0; r < num_consistency; r++)
cons_base[r] = __builtin_popcount(consistency_T[r] & adj_rhs_base) & 1;
/* Compute deltas for each null vector */
uint32_t cons_mat[20]; /* bitmask: bit j = consistency row r dot delta_j */
memset(cons_mat, 0, sizeof(cons_mat));
for (int j = 0; j < num_free; j++) {
uint8_t flipped[N];
memcpy(flipped, base_flag, N);
for (int idx = 0; idx < NUM_UNK; idx++) {
if (null_vecs[j][idx])
flipped[unk_pos[idx]] ^= (1 << k);
}
uint32_t b_next_flip = compute_b(k+1, flipped);
uint32_t delta = b_next_base ^ b_next_flip;
for (int r = 0; r < num_consistency; r++) {
if (__builtin_popcount(consistency_T[r] & delta) & 1)
cons_mat[r] |= (1u << j);
}
}
/* Solve consistency system: cons_mat * c = cons_base */
/* Small system: 20 equations in num_free unknowns */
uint32_t cm[20];
int cr[20];
memcpy(cm, cons_mat, sizeof(cm));
memcpy(cr, cons_base, sizeof(cr));
int pivot[13];
memset(pivot, -1, sizeof(pivot));
int crow = 0;
for (int col = 0; col < num_free; col++) {
int piv = -1;
for (int row = crow; row < num_consistency; row++) {
if (cm[row] & (1u << col)) { piv = row; break; }
}
if (piv == -1) continue;
uint32_t t; int ti;
t = cm[piv]; cm[piv] = cm[crow]; cm[crow] = t;
ti = cr[piv]; cr[piv] = cr[crow]; cr[crow] = ti;
pivot[col] = crow;
for (int row = 0; row < num_consistency; row++) {
if (row != crow && (cm[row] & (1u << col))) {
cm[row] ^= cm[crow];
cr[row] ^= cr[crow];
}
}
crow++;
}
/* Check consistency of the consistency system */
for (int row = 0; row < num_consistency; row++) {
if (cm[row] == 0 && cr[row] == 1) return; /* No valid combo */
}
/* Find free vars in consistency system */
int cfree[13], ncfree = 0;
for (int col = 0; col < num_free; col++) {
if (pivot[col] < 0)
cfree[ncfree++] = col;
}
/* Enumerate valid combos */
uint64_t total_combos = 1ULL << ncfree;
for (uint64_t cbits = 0; cbits < total_combos; cbits++) {
if (found) return;
int combo[13] = {0};
/* Set free vars */
for (int fi = 0; fi < ncfree; fi++)
combo[cfree[fi]] = (cbits >> fi) & 1;
/* Solve for pivot vars */
for (int col = 0; col < num_free; col++) {
if (pivot[col] >= 0) {
int val = cr[pivot[col]];
for (int fi = 0; fi < ncfree; fi++) {
if (cm[pivot[col]] & (1u << cfree[fi]))
val ^= ((cbits >> fi) & 1);
}
combo[col] = val;
}
}
/* Apply combo to flag */
uint8_t new_flag[N];
memcpy(new_flag, flag, N);
for (int idx = 0; idx < NUM_UNK; idx++) {
int bit = particular[idx];
for (int j = 0; j < num_free; j++) {
if (combo[j] && null_vecs[j][idx])
bit ^= 1;
}
new_flag[unk_pos[idx]] |= (bit << k);
}
/* Restore known values */
for (int ki = 0; ki < NUM_KNOWN; ki++)
new_flag[known_pos[ki]] = known_val[ki];
dfs(k+1, new_flag);
}
} else {
/* Bit 7: enumerate all null combos, check printability */
uint64_t total = 1ULL << num_free;
for (uint64_t bits = 0; bits < total; bits++) {
if (found) return;
uint8_t new_flag[N];
memcpy(new_flag, flag, N);
for (int idx = 0; idx < NUM_UNK; idx++) {
int bit = particular[idx];
for (int j = 0; j < num_free; j++) {
if ((bits >> j) & 1) {
if (null_vecs[j][idx])
bit ^= 1;
}
}
new_flag[unk_pos[idx]] |= (bit << k);
}
for (int ki = 0; ki < NUM_KNOWN; ki++)
new_flag[known_pos[ki]] = known_val[ki];
/* Quick printability check */
int ok = 1;
for (int i = 6; i < 31; i++) {
if (new_flag[i] < 0x20 || new_flag[i] > 0x7e) { ok = 0; break; }
}
if (!ok) continue;
/* Verify */
uint8_t out[N];
forward(new_flag, out);
if (memcmp(out, target, N) == 0) {
memcpy(solution, new_flag, N);
found = 1;
return;
}
}
}
}
int main(void) {
/* Set up unknown positions */
int is_known[N] = {0};
for (int i = 0; i < NUM_KNOWN; i++) is_known[known_pos[i]] = 1;
int ui = 0;
for (int i = 0; i < N; i++) {
if (!is_known[i]) unk_pos[ui++] = i;
}
printf("Building A matrix...\n");
build_A();
printf("Computing consistency check matrix...\n");
compute_consistency_T();
precompute_known_cols();
printf(" Consistency equations: %d\n", num_consistency);
printf("Starting DFS...\n");
uint8_t flag[N] = {0};
for (int i = 0; i < NUM_KNOWN; i++)
flag[known_pos[i]] = known_val[i];
dfs(0, flag);
if (found) {
printf("\nFLAG: ");
for (int i = 0; i < N; i++) printf("%c", solution[i]);
printf("\n");
/* Verify */
uint8_t out[N];
forward(solution, out);
printf("Verify: %s\n", memcmp(out, target, N) == 0 ? "PASS" : "FAIL");
} else {
printf("\nNo solution found.\n");
}
return 0;
}
solve_final.py
#!/usr/bin/env python3
"""
Bit-slicing solver with corrected GF(2) Gaussian elimination.
Handles free variables by enumerating all 2^(num_free) possibilities.
"""
import itertools
target = b'c\xc9\xa2+\xcf\xef\xd4+\xeb\x83w&\xe7\xfd\t\xde\xf3\xe5\xdeO\x13\x0bl\xb7\x1b\xab\x0f\x8a\x13\xc5\xfd\x92'
n = 32
def forward(flag_bytes):
state = list(flag_bytes)
for j in range(100):
y = 140*j + 133
op = (2*j) % 5
if op == 0: state = [state[i] ^ state[(i+y)%n] for i in range(n)]
elif op == 1: state = [state[(i+y)%n] for i in range(n)]
elif op == 2: state = [state[i] ^ y for i in range(n)]
elif op == 3: state = [state[i] * y % 256 for i in range(n)]
elif op == 4: state = [(state[i] + y) % 256 for i in range(n)]
return bytes(state)
def mat_mul(A, B):
BT = [0]*n
for i in range(n):
for j in range(n):
if B[i] & (1<<j): BT[j] |= (1<<i)
R = [0]*n
for i in range(n):
for j in range(n):
if bin(A[i] & BT[j]).count('1') & 1: R[i] |= (1<<j)
return R
def mat_vec(A, v):
r = 0
for i in range(n):
if bin(A[i] & v).count('1') & 1: r |= (1<<i)
return r
def identity():
return [(1<<i) for i in range(n)]
def forward_partial_all(flag_vals, mask):
state = [f & mask for f in flag_vals]
history = [list(state)]
for j in range(100):
y = 140*j + 133
op = (2*j) % 5
if op == 0: state = [(state[i] ^ state[(i+y)%n]) & mask for i in range(n)]
elif op == 1: state = [state[(i+y)%n] for i in range(n)]
elif op == 2: state = [(state[i] ^ (y & 0xFF)) & mask for i in range(n)]
elif op == 3: state = [(state[i] * (y%256)) & mask for i in range(n)]
elif op == 4: state = [(state[i] + (y%256)) & mask for i in range(n)]
history.append(list(state))
return history
def solve_gf2_all(A_full, rhs_full, unknowns, knowns):
"""Solve A*x = rhs over GF(2). Returns (particular_solution, null_space_vectors)."""
num_unk = len(unknowns)
# Adjust RHS for known values
rhs = rhs_full
for pos, val in knowns.items():
if val:
col = 0
for row in range(n):
if A_full[row] & (1 << pos):
col |= (1 << row)
rhs ^= col
# Extract submatrix: n rows x num_unk cols
mat = [0] * n
rhs_bits = [0] * n
for row in range(n):
r = 0
for idx, u in enumerate(unknowns):
if A_full[row] & (1 << u):
r |= (1 << idx)
mat[row] = r
rhs_bits[row] = (rhs >> row) & 1
# Gaussian elimination
pivot_row = {} # col -> row index after elimination
cur_row = 0
for col in range(num_unk):
# Find pivot
piv = -1
for row in range(cur_row, n):
if mat[row] & (1 << col):
piv = row
break
if piv == -1:
continue
# Swap to cur_row
mat[piv], mat[cur_row] = mat[cur_row], mat[piv]
rhs_bits[piv], rhs_bits[cur_row] = rhs_bits[cur_row], rhs_bits[piv]
pivot_row[col] = cur_row
# Eliminate
for row in range(n):
if row != cur_row and mat[row] & (1 << col):
mat[row] ^= mat[cur_row]
rhs_bits[row] ^= rhs_bits[cur_row]
cur_row += 1
# Check consistency
for row in range(n):
if mat[row] == 0 and rhs_bits[row] == 1:
return None, None # Inconsistent
# Identify free variables
free_cols = [col for col in range(num_unk) if col not in pivot_row]
# Particular solution (free vars = 0)
particular = [0] * num_unk
for col, row in pivot_row.items():
particular[col] = rhs_bits[row]
# Null space basis vectors
null_vecs = []
for fc in free_cols:
vec = [0] * num_unk
vec[fc] = 1
# For each pivot column, check if it depends on this free column
for col, row in pivot_row.items():
if mat[row] & (1 << fc):
vec[col] = 1
null_vecs.append(vec)
return particular, null_vecs
def build_affine_transform(k, history):
"""Build the composed affine transformation (A, b) for bit plane k."""
A = identity()
b = 0
mask = (1 << k) - 1
for j in range(100):
y = 140*j + 133
op = (2*j) % 5
if op == 0: # XOR shift
s = y % n
A_j = [0]*n
for i in range(n):
A_j[i] = (1<<i) | (1<<((i+s)%n))
b = mat_vec(A_j, b)
A = mat_mul(A_j, A)
elif op == 1: # Rotation
r = y
A_j = [0]*n
for i in range(n):
A_j[i] = 1 << ((i+r)%n)
b = mat_vec(A_j, b)
A = mat_mul(A_j, A)
elif op == 2: # XOR const
y_low = y & 0xFF
if (y_low >> k) & 1:
b ^= (1<<n) - 1
elif op == 3: # Multiply
y_mul = y % 256
b_j = 0
for i in range(n):
val = (history[j][i] * y_mul) if k > 0 else 0
b_j |= (((val >> k) & 1) << i)
b ^= b_j
elif op == 4: # Add
y_add = y % 256
add_k = (y_add >> k) & 1
b_j = 0
if k > 0:
y_add_low = y_add & mask
for i in range(n):
carry = ((history[j][i] + y_add_low) >> k) & 1
b_j |= ((add_k ^ carry) << i)
else:
if add_k:
b_j = (1<<n) - 1
b ^= b_j
return A, b
# Known flag bytes
flag_known = {0: ord('B'), 1: ord('C'), 2: ord('C'), 3: ord('T'),
4: ord('F'), 5: ord('{'), 31: ord('}')}
known_positions = set(flag_known.keys())
unknown_positions = sorted(set(range(n)) - known_positions)
# Solve all 8 bit planes, collecting free variable choices
flag_vals = [0] * n
for pos, val in flag_known.items():
flag_vals[pos] = val
all_free_choices = [] # List of (bit_plane, null_vecs, particular, unknowns)
print("Solving bit planes...")
for k in range(8):
mask = (1 << k) - 1
history = forward_partial_all(flag_vals, mask) if k > 0 else [[0]*n]*101
A, b = build_affine_transform(k, history)
target_bits = 0
for i in range(n):
target_bits |= (((target[i] >> k) & 1) << i)
rhs = target_bits ^ b
knowns_k = {pos: (val >> k) & 1 for pos, val in flag_known.items()}
particular, null_vecs = solve_gf2_all(A, rhs, unknown_positions, knowns_k)
if particular is None:
print(f" Bit {k}: INCONSISTENT - trying with current flag state")
break
num_free = len(null_vecs)
print(f" Bit {k}: rank deficit = {num_free} free variable(s)")
if num_free == 0:
# Unique solution
for idx, pos in enumerate(unknown_positions):
flag_vals[pos] |= (particular[idx] << k)
else:
# Try all combinations of free variables
all_free_choices.append((k, particular, null_vecs))
# For now, use particular solution (free vars = 0)
for idx, pos in enumerate(unknown_positions):
flag_vals[pos] |= (particular[idx] << k)
# Enumerate free variable combinations
total_free = sum(len(nv) for _, _, nv in all_free_choices)
print(f"\nTotal free variables: {total_free}")
print(f"Enumerating {2**total_free} combinations...")
# Build list of all free variable flips
free_bits = [] # (bit_plane, null_vec_index, null_vec)
for k, particular, null_vecs in all_free_choices:
for nvi, nv in enumerate(null_vecs):
free_bits.append((k, nv))
best_flag = None
for combo in itertools.product([0, 1], repeat=total_free):
# Start from particular solution
test_flag = list(flag_vals) # Already has particular solutions set
# First, reset the bits for planes with free variables
for k, particular, null_vecs in all_free_choices:
for idx, pos in enumerate(unknown_positions):
test_flag[pos] &= ~(1 << k) # Clear bit k
test_flag[pos] |= (particular[idx] << k) # Set particular
# Apply free variable flips
for fi, (k, nv) in enumerate(free_bits):
if combo[fi]:
for idx, pos in enumerate(unknown_positions):
if nv[idx]:
test_flag[pos] ^= (1 << k)
# Check constraints
ok = True
for pos, val in flag_known.items():
if test_flag[pos] != val:
ok = False
break
if not ok:
continue
# Check printable ASCII
all_print = True
for i in range(6, 31):
if test_flag[i] < 0x20 or test_flag[i] > 0x7E:
all_print = False
break
if not all_print:
continue
# Verify forward
result = forward(bytes(test_flag))
if result == target:
best_flag = bytes(test_flag)
print(f"\nFLAG FOUND: {best_flag.decode()}")
break
if best_flag is None:
# Also try without printability constraint
print("\nTrying without printability constraint...")
for combo in itertools.product([0, 1], repeat=total_free):
test_flag = list(flag_vals)
for k, particular, null_vecs in all_free_choices:
for idx, pos in enumerate(unknown_positions):
test_flag[pos] &= ~(1 << k)
test_flag[pos] |= (particular[idx] << k)
for fi, (k, nv) in enumerate(free_bits):
if combo[fi]:
for idx, pos in enumerate(unknown_positions):
if nv[idx]:
test_flag[pos] ^= (1 << k)
result = forward(bytes(test_flag))
if result == target:
best_flag = bytes(test_flag)
print(f"FLAG FOUND: {best_flag}")
try:
print(f"Decoded: {best_flag.decode()}")
except:
print("(not decodable as UTF-8)")
break
if best_flag is None:
print("No solution found!")