[CISCN 2021 Preliimnary] babybc

This challenge provdies a 64-bit ELF binary obfuscated with LLVM control-flow flattening, distributed as a BC LLVM IR file. Reverse engineering reveals the core problem is a constrained 5x5 sudoku puzzle, with custom order constraints encoded in two matrices, which can be solved with the Z3 theorem solver.

from z3 import *
from hashlib import md5

# Row order constraints: 1 = current > next, 2 = current < next
row_constraints = [
    [0x00, 0x00, 0x00, 0x01],
    [0x01, 0x00, 0x00, 0x00],
    [0x02, 0x00, 0x00, 0x01],
    [0x00, 0x00, 0x00, 0x00],
    [0x01, 0x00, 0x01, 0x00]
]

# Column order constraints: 1 = current < next, 2 = current > next
col_constraints = [
    [0x00, 0x00, 0x02, 0x00, 0x02],
    [0x00, 0x00, 0x00, 0x00, 0x00],
    [0x00, 0x00, 0x00, 0x01, 0x00],
    [0x00, 0x01, 0x00, 0x00, 0x01]
]

solver = Solver()

# Initialize 5x5 grid of integer variables
grid = [[None for _ in range(5)] for _ in range(5)]
for i in range(5):
    for j in range(5):
        grid[i][j] = Int(f"cell_{i}_{j}")

# Add pre-known fixed values
solver.add(grid[2][2] == 4)
solver.add(grid[3][3] == 3)

# Basic bound constraint: all values 1-5
for i in range(5):
    for j in range(5):
        solver.add(grid[i][j] >= 1)
        solver.add(grid[i][j] <= 5)

# Row uniqueness: no duplicate values per row
for i in range(5):
    for j in range(5):
        for k in range(j):
            solver.add(grid[i][j] != grid[i][k])

# Column uniqueness: no duplicate values per column
for j in range(5):
    for i in range(5):
        for k in range(i):
            solver.add(grid[i][j] != grid[k][j])

# Apply custom row order constraints
for i in range(5):
    for j in range(4):
        if row_constraints[i][j] == 1:
            solver.add(grid[i][j] > grid[i][j + 1])
        elif row_constraints[i][j] == 2:
            solver.add(grid[i][j] < grid[i][j + 1])

# Apply custom column order constraints
for i in range(4):
    for j in range(5):
        if colnms[i][j] == 2:
            solver.add(grid[i][j] > grid[i + 1][j])
        elif colnms[i][j] == 1:
            solver.add(grid[i][j] < grid[i + 1][j])

if solver.check() == sat:
    model = solver.model()
    solved_values = []
    for row in grid:
        for cell in row:
            solved_values.append(model[cell].as_long())
    
    # Convert to ASCII bytes and generate flag hash
    byte_list = [val + 48 for val in solved_values]
    byte_list[12] = 48
    byte_list[18] = 48
    input_bytes = bytes(byte_list)
    flag_md5 = md5(input_bytes).hexdigest()
    print(f"CISCN{{{flag_md5}}}")

Final flag: CISCN{8a04b4597ad08b83211d3adfa1f61431}

---

[HNCTF 2022 Week 4] ez_maze

This challenge distributes a pyc bytecdoe file that cannot be decompiled with uncompyle6. Decompiling with pycdc reveals a 31×31 maze problem where valid paths can only traverse cells marked 0. A DFS-based solution can be used to find the correct path:

from hashlib import md5
maze = [[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1],
        [1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1],
        [1, 0, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 0, 1, 0, 1, 1, 1, 1, 1, 1, 1, 0, 1],
        [1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 1],
        [1, 0, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 0, 1, 0, 1, 0, 1, 0, 1],
        [1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0,