Overview

We have a very pretty TUI to “refine” numbers:

Reversing

A big part of this challenge, was to reverse the core functions. The binary is stripepd and statically linked, so function/lumina signatures really helped in order to get an overview.

Here’s a rather ugly decompilation:

void* game_loop()

{
    int32_t cur_x = 0;
    int32_t cur_y = 0;
    grid_init(&numbers);
    void* result;

    while (true)
    {
        grid_display(&numbers, cur_x, cur_y);
        int32_t keycode = getc(stdin) & 0xffffffdf;

        if (keycode <= 82)
        {
            if (keycode < 72)
            {
                if (keycode != 0xa && keycode != 0xd)
                    continue;

                if ((&numbers)[(int64_t)cur_y * 0x28 + (int64_t)cur_x])
                    (&numbers)[(int64_t)cur_y * 0x28 + (int64_t)cur_x] = 0;

                toggle_state_check_and_win();
            }
            else if (keycode - 72 <= 0xa)
            {
                result =
                    (int64_t)jpt_402711[(uint64_t)(keycode - 0x48)] + &jpt_402711;

                switch (result)  // switch jump
                {
                    case 0x402714:  // r
                    {
                        grid_init(&numbers);
                        continue;
                    }
                    case 0x402728:  // h
                    {
                        // jumptable 0000000000402711 case 72
                        if (cur_x <= 0)
                            continue;
                        else
                        {
                            cur_x -= 1;
                            continue;
                        }
                        break;
                    }
                    case 0x40273b:  // j
                    {
                        // jumptable 0000000000402711 case 74
                        if (cur_y > 18)
                            continue;
                        else
                        {
                            cur_y += 1;
                            continue;
                        }
                        break;
                    }
                    case 0x40274e:  // k
                    {
                        if (cur_y <= 0)
                            continue;
                        else
                        {
                            cur_y -= 1;
                            continue;
                        }
                        break;
                    }
                    case 0x402761:  // l
                    {
                        if (cur_x > 38)
                            continue;
                        else
                        {
                            cur_x += 1;
                            continue;
                        }
                        break;
                    }
                    case &def_402711:
                    {
                        continue;
                    }
                    case 0x4027fd: // q
                    {
                        break;
                        break;
                    }
                }
            }
        }
    }

    return result;
}

This already covers the main input flow of the program, we can use hjkl to move the cursor, enter to remove a field, q to quit and r to regenerate the field.

There’s a check function, that runs after removing an entry:

int64_t toggle_state_check_and_win()

{
    int64_t left_diagonal_sum = 0;
    int64_t global_sum_this_is_any_positive_nr = 1;

    for (int32_t y_coord = 0; y_coord <= 19; y_coord += 1)
        left_diagonal_sum += (int64_t)(&numbers)[(int64_t)y_coord * 41];

    int64_t second_diagnonal_sum = 0;

    // diagnonal pattern
    for (int32_t rows = 0; rows <= 19; rows += 1)
        second_diagnonal_sum +=
            (int64_t)(&numbers)[(int64_t)rows * 40 + (int64_t)(39 - rows)];

    int64_t checksum =
        (left_diagonal_sum ^ second_diagnonal_sum) + left_diagonal_sum * second_diagnonal_sum;
    int64_t checksum_result = checksum >> 0x11 | checksum << 0x2f;

    for (int32_t rows2 = 0; rows2 <= 19; rows2 += 1)
    {
        int64_t xored_var = 0;
        int64_t row_sum = 0;

        for (int32_t column = 0; column <= 39; column += 1)
        {
            xored_var ^= (int64_t)(&numbers)[(int64_t)rows2 * 0x28 + (int64_t)column];
            row_sum += (int64_t)(&numbers)[(int64_t)rows2 * 0x28 + (int64_t)column];
        }

        if (xored_var == checksum_result && !(row_sum % 997))
            break;
    }

    for (int32_t row = 0; row <= 19; row += 1)  // Final check
    {
        for (int32_t col = 0; col <= 39; col += 1)
            global_sum_this_is_any_positive_nr +=
                (int64_t)(&numbers)[(int64_t)row * 40 + (int64_t)col];
    }

    int64_t result = global_sum_this_is_any_positive_nr ^ checksum_result;

    if (result != checksum_result)
        return result;

    exit(1);
    /* no return */
}

The following constraints are checked by this:

Both diagonals have all been removed (otherwise checksum is nonzero)
We add up and xor every row, break early if we hit an empty row or a row that sum % 997 == 0
We add up all fields together

However, this check function will always return early, as checksum_result will always either be 0 or a very large number. The checks don’t make a lot of sense and we can never reach the exit(1) in the end, required for the remote to give us the flag.

After a longer struggle, I stepped through the binary and found a function at the end, that gets called after hitting q:

void backdoor() __noreturn {
  int ok_rows = 1;

  for (int r = 0; r < 20; r++) {
    int64_t sum = 0;
    for (int c = 0; c < 40; c++) {
      sum += (int64_t)get_field_at(r, c);
    }
    ok_rows &= (sum == 42);
  }

  int ok_cols = 1;

  for (int c = 0; c < 40; c++) {
    int64_t sum = 0;
    for (int r = 0; r < 20; r++) {
      sum += (int64_t)get_field_at(r, c);
    }
    ok_cols &= (sum != 0);
  }

  int status = ok_rows & ok_cols;
  syscall(SYS_exit, status);
}

So, essentially, if all rows add up to 42 and all columns have a nonzero sum, we exit with 1.

Now, all that’s left is to script this:

import re

from pwn import *
from rich import print
from rich.progress import track
from z3 import *

start_char = "╭".encode()
end_char = "╰".encode()

p = remote("challs.qualifier.swiss-hacking-challenge.ch", 30271)


# replace empty spaces with nulls
def expand_gaps(line: bytes) -> bytes:
    def repl(m):
        spaces = len(m.group(0))
        zeros = spaces // 2
        return b" " + b"0 " * zeros

    return re.sub(rb" {2,}", repl, line)


def get_grid():
    matrix = []
    p.recvuntil(start_char)
    p.recvline()
    while True:
        line = p.recvline()
        if end_char in line:
            break
        line = line.replace(b"\x1b[0;36m", b"")  # ]
        line = line.replace(b"\x1b[1;36m", b"")  # ]
        line = expand_gaps(line)
        matrix.append([int(x) for x in line.decode().split() if x in "1234567890"])
    for row in matrix:
        print("[ ", end="")
        for col in row:
            if col == 0:
                print(f"[red]{col}[/red], ", end="")
            else:
                print(f"{col}, ", end="")
        print("],  ")
    return matrix


def remove_char(x, y):
    # print(f"removing {x=} {y=}")
    for i in range(0x28):
        p.send(b"h")
        p.recvuntil(end_char)
    for i in range(0x15):
        p.send(b"k")
        p.recvuntil(end_char)
    for i in range(x):
        p.send(b"l")
        p.recvuntil(end_char)
    for i in range(y):
        p.send(b"j")
        p.recvuntil(end_char)
    p.sendline()


success("Old grid: ")
matrix = get_grid()


ROWS = 20
COLS = 40

s = Solver()

remove = [[Bool(f"rem_{r}_{c}") for c in range(COLS)] for r in range(ROWS)]

val = [[If(remove[r][c], 0, matrix[r][c]) for c in range(COLS)] for r in range(ROWS)]

for r in range(ROWS):
    s.add(Sum(val[r]) == 42)

for c in range(COLS):
    s.add(Sum([val[r][c] for r in range(ROWS)]) != 0)

if s.check() != sat:
    print("unsat")
    sys.exit(0)

info("Calculating new grid")
m = s.model()

# get new grid calculated by z3
new_grid = []
for r in range(ROWS):
    row = []
    for c in range(COLS):
        row.append(0 if is_true(m[remove[r][c]]) else matrix[r][c])
    new_grid.append(row)

# ensure we're at the start
for i in range(0x28):
    p.send(b"h")
    p.recvuntil(end_char)
for i in range(0x15):
    p.send(b"k")
    p.recvuntil(end_char)

# set all fields to their desired state
for row in track(range(ROWS)):
    for col in range(COLS):
        if new_grid[row][col] != matrix[row][col]:
            p.sendline()
        p.send(b"l")
        p.recvuntil(end_char)
    for i in range(0x28):
        p.send(b"h")
    p.send(b"j")
p.send(b"j")

p.sendline("q")
success("Program should exit with 1 now, press enter to switch to internyactive :3")
input()
p.interactive()

In action:

Flag:

dach2026{1t5_r4r3_t0_m33t_4_s0ph1st1c4t3_8499cf614a_b394e8c95bf0}

Overview#

Reversing#

Overview

Reversing