Solution de rouaulth pour Triceratops

Table des matières

Ce document présente une résolution du challenge Hackropole triceratops. C’est un problème intéressant, qui mêle plusieurs techniques. On procède en plusieurs étapes :

désassemblage du binaire
formalisation du problème à résoudre
réduction du modèle à une grille $S$ à trois états
construction déterministe d’un serial valide

Une fois le coeur du problème simplifié, il devient possible de construire un algorithme constructif relativement simple.

Codex m’a aidé à interpréter le désassemblage, écrire les modèles, automatiser la génération des serials et valider le service final.

Le flag obtenu est :

FCSC{33e678eba72fbadb38386a7f2a79b5aedc8e93240d7632d360efa4ccef7cb6e2}

Objectif du challenge

Voici l’énoncé :

On vous demande d'écrire un keygen pour ce binaire et de le valider sur le
service en ligne.

Le service commence par demander un serial valide pour FCSC2021. On se rend compte ensuite qu’il demande des serials valides pour 50 noms d’utilisateur aléatoires. Il ne faut donc pas trouver un seul couple utilisateur/serial. Il faut écrire un générateur de serials. Le flag n’est affiché qu’après validation des 51 instances.

Désassemblage

Le binaire principal triceratops est un ELF x86-64 strippé :

$ file triceratops
ELF 64-bit LSB executable, x86-64, dynamically linked, stripped

Le service Docker utilise le même binaire dans /app/triceratops. Le wrapper du service est un script Python dans /app/server.py.

Analyse statique

On peut commencer par importer le binaire dans Ghidra, ce qui permet d’identifier les différentes fonctions.

0x401251  build_username_grid
0x4013b1  advance_grid_cells
0x4015f3  apply_serial_moves
0x401a61  validate_serial_alphabet
0x401aca  collect_grid_signature
0x401f10  popcount64
0x401c42  main
0x4040c0  allowed signature table

main commence par lire le nom d’utilisateur et le serial. Il valide ensuite l’alphabet du serial avec validate_serial_alphabet, puis construit une grille avec build_username_grid à partir du username. Il transforme ensuite la grille en fonction du serial. Il finit par vérifier que la grille transformée satisfait une condition globale.

Le serial doit donc correspondre aux bonnes transformations de la grille pour que cette condition soit validée.

Définition du modèle

On peut maintenant traduire les contraintes du binaire en un modèle discret. Le serial définit une suite de mouvements locaux sur une grille 16x16.

Le pseudo-code Ghidra permet d’extraire les contrats des fonctions importantes :

build_username_grid        construit l'état initial depuis le username
validate_serial_alphabet   vérifie que le serial encode des mouvements valides
apply_serial_moves         applique les mouvements à la grille
collect_grid_signature     calcule la condition finale d'acceptation

État du système

L’état du système est formé de deux grilles 16x16 de trits, c’est-à-dire d’éléments de $\mathbb{Z}/3\mathbb{Z}$. Je note ces deux grilles up et down dans le code et le pseudo-code.

Mathématiquement, pour chaque site $i$, on note ces deux variables $u_i$ et $d_i$ :

$$ u_i, d_i \in \mathbb{Z}/3\mathbb{Z}. $$

On introduit ensuite une troisième grille $S$, définie site par site par :

$$ S_i = u_i + d_i \pmod 3. $$

C’est cette variable $S$ qui rend la dynamique lisible. L’invariant modulo 3 et la condition finale s’expriment simplement en termes de $S$.

Construction de l’état initial

Pour chaque nom d’utilisateur, le binaire construit déterministiquement deux grilles pseudo-aléatoires up et down.

Les grilles sont générées avec SHA-256. Pour la grille up, le préfixe est [0, counter]. Pour la grille down, le préfixe est [1, counter].

Chaque digest est consommé à l’envers. Chaque octet est découpé en quatre blocs de deux bits. Les blocs valant 3 sont ignorés. Tous les autres blocs sont ajoutés comme trits.

Un modèle Python minimal est :

"""Modèle minimal de génération de grille par SHA-256."""

import hashlib

GRID_CELLS = 256
SKIPPED_TRIT = 3


def build_grid(username: str, *, down: bool) -> list[int]:
    """Construit une grille 16x16 de trits pour un nom d'utilisateur."""
    cells: list[int] = []
    counter = 0
    prefix = 1 if down else 0
    username_bytes = username.encode()

    while len(cells) < GRID_CELLS:
        digest = hashlib.sha256(
            bytes([prefix, counter & 0xFF]) + username_bytes,
        ).digest()
        counter += 1
        for byte in reversed(digest):
            for shift in (0, 2, 4, 6):
                trit = (byte >> shift) & SKIPPED_TRIT
                if trit != SKIPPED_TRIT:
                    cells.append(trit)
                    if len(cells) == GRID_CELLS:
                        return cells

    message = "unreachable"
    raise RuntimeError(message)

Après construction des deux grilles, le binaire modifie les sites égaux :

if up[i] == down[i]:
    up[i]   = up[i]   + 1 mod 3
    down[i] = down[i] + 2 mod 3

Cette opération conserve $S_i$. En effet, si $u_i = d_i$, alors la somme est modifiée de $1 + 2 = 0$ modulo 3. Après cette correction, on a donc $u_i \neq d_i$ pour tout site $i$. C’est une propriété importante pour simplifier la condition d’acceptation des mouvements.

Actions et transitions

Le serial encode une suite d’actions locales. Chaque action choisit une arête horizontale ou verticale de la grille.

Le binaire impose d’abord que strlen(serial) % 3 == 0. Le serial est découpé en trois parties de même longueur.

La première partie contient des caractères de ligne entre a et p. La deuxième partie contient des caractères de colonne entre a et p. La troisième partie contient des directions A ou B.

Chaque mouvement est donc encodé par une ligne, une colonne et une direction.

premier tiers  -> ligne, 0..15
deuxième tiers -> colonne, 0..15
troisième tiers -> direction A ou B

La direction A sélectionne une arête horizontale :

(row, col) -> (row, col + 1)

La direction B sélectionne une arête verticale :

(row, col) -> (row + 1, col)

Les mouvements qui sortent par le bord droit ou le bord bas sont rejetés. De plus, seuls certains mouvements sont autorisés suivant l’état des deux sites considérés. Tout mouvement rejeté rend le serial final invalide.

Pour une arête $(i, j)$, la condition d’acceptation locale peut s’écrire simplement :

$$ u_i \neq d_i, \qquad u_j \neq d_j, \qquad S_i \neq S_j. $$

Les deux premières conditions disent que les deux couches sont différentes sur chacun des deux sites. La dernière condition dit que les deux valeurs voisines de $S$ sont différentes.

La construction initiale impose déjà $u_i \neq d_i$ pour tous les sites. La règle de transition préserve ensuite cette propriété. Sur les états réellement atteignables par le programme, les deux premières conditions sont donc toujours satisfaites.

La condition d’acceptation se réduit alors à :

$$ S_i \neq S_j. $$

Cette réduction est le point clef. Pour chercher un serial, on peut oublier les deux couches up et down et ne raisonner que sur la grille $S$.

Le binaire implémente cette condition avec une table. Pour cela, il encode d’abord les quatre trits locaux dans une signature entière :

$$ \sigma_{ij} = 100(10u_i + u_j) + 10d_i + d_j = 1000u_i + 100u_j + 10d_i + d_j. $$

Cet encodage est injectif. La signature identifie donc univoquement la configuration locale $(u_i, u_j, d_i, d_j)$.

Le test algorithmique consiste alors à vérifier si cette signature appartient à la table située à 0x4040c0. Cette table contient 24 signatures, qui sont exactement les états satisfaisant les trois conditions précédentes. Les valeurs sont écrites ici en hexadécimal, comme elles apparaissent dans le désassemblage.

"""Signatures de mouvement autorisées."""

ALLOWED: set[int] = {
    0x000C,
    0x0015,
    0x0070,
    0x0078,
    0x007A,
    0x00D2,
    0x00D3,
    0x00DD,
    0x03EA,
    0x03FD,
    0x03FE,
    0x044E,
    0x0460,
    0x04B0,
    0x04B1,
    0x04C4,
    0x07D1,
    0x07DB,
    0x07DC,
    0x0834,
    0x0836,
    0x083E,
    0x0899,
    0x08A2,
}

Si le mouvement est accepté, les valeurs up et down des deux sites de l’arête sont réécrites.

En termes de la grille $S$, les mouvements acceptés sont :

Un mouvement accepté prend donc deux voisins inégaux et les rend égaux. La nouvelle valeur est l’élément manquant de {0, 1, 2}.

Il n’y a pas de mouvement neutre dans cette projection sur $S$.

La règle sur $S$ ne suffit toutefois pas à déterminer les nouvelles valeurs de $u$ et $d$. Le binaire choisit cette décomposition en fonction de la parité damier du site.

On pose :

$$ v = S_i + S_j \pmod 3. $$

Si le site $k$ est sur une case paire, c’est-à-dire si row + col est pair, alors :

$$ u’_k = v + 1 \pmod 3, \qquad d’_k = v + 2 \pmod 3. $$

Si le site $k$ est sur une case impaire, alors :

$$ u’_k = v + 2 \pmod 3, \qquad d’_k = v + 1 \pmod 3. $$

Deux sites voisins ont toujours des parités opposées. Les deux extrémités de l’arête reçoivent donc les deux décompositions opposées. Dans les deux cas, les nouvelles valeurs vérifient encore $u’_k \neq d’_k$. Les actions préservent donc la propriété $u_i \neq d_i$ pour tous les sites.

Vérification finale

La dernière fonction vérifie que toutes les valeurs de la grille $S$ sont égales.

On obtient donc un objectif clair pour le solveur. Pour un nom d’utilisateur donné, il faut transformer la grille initiale 16x16 en une grille $S$ constante.

Invariant

La règle de mouvement conserve la somme globale des valeurs de $S$ modulo 3. Par exemple :

$$ 0 + 1 = 1 \pmod 3 $$

$$ 2 + 2 = 1 \pmod 3. $$

Comme il y a 256 sites, la cible est imposée par :

$$ 256 \times t = \sum_i S_i^{\mathrm{initial}} \pmod 3. $$

Or $256 = 1 \pmod 3$, donc :

$$ t = \sum_i S_i^{\mathrm{initial}} \pmod 3. $$

Pour FCSC2021, la cible vaut 1. Pour les noms aléatoires du service, elle se calcule de la même manière.

Résolution constructive

Une fois la cible $t$ connue, les sites tels que $S_i \neq t$ sont des défauts. Les deux autres couleurs sont notées $a$ et $b$.

Deux défauts voisins de couleurs différentes s’annihilent immédiatement :

a b -> t t
b a -> t t

Un défaut peut aussi être déplacé de deux cases à travers une zone déjà à la couleur cible. Par exemple :

a t t
b b t
b a a
t t a

Chaque ligne est obtenue par un mouvement autorisé sur deux sites voisins. Ce motif permet de rapprocher deux défauts sans détruire la zone déjà résolue.

Si tous les défauts restants ont la même couleur, il suffit d’en convertir un au contact d’un site cible :

a t -> b b

On remplace alors un défaut de couleur $a$ par deux défauts de couleur $b$. Cela permet de recréer une paire de couleurs différentes, puis de continuer les annihilations.

L’algorithme utilisé est donc glouton, mais déterministe :

calculer les défauts courants
annihiler directement les paires voisines de couleurs différentes
sinon rapprocher la paire de défauts de couleurs différentes la moins chère
convertir un défaut si aucune paire de couleurs différentes n’existe
convertir plus tôt un défaut central si trois défauts de même couleur sont suffisamment compacts

Pour FCSC2021, cet algorithme trouve directement :

target=1
moves=219
serial_len=657
defects=0

Le coeur de la méthode peut s’écrire directement comme un solveur sur une grille $S$ déjà construite. Le script suivant renvoie une liste de mouvements (row, col, direction).

"""Solveur constructif minimal sur la grille S."""

from collections import deque
from dataclasses import dataclass

N = 16
NEIGHBORS = ((0, -1), (-1, 0), (0, 1), (1, 0))


@dataclass(frozen=True)
class Move:
    row: int
    col: int
    direction: str
    first: int
    second: int


def index(row: int, col: int) -> int:
    return row * N + col


def row_col(cell: int) -> tuple[int, int]:
    return divmod(cell, N)


def neighbors(cell: int) -> list[int]:
    row, col = row_col(cell)
    result = []
    for dr, dc in NEIGHBORS:
        nr, nc = row + dr, col + dc
        if 0 <= nr < N and 0 <= nc < N:
            result.append(index(nr, nc))
    return result


def pair_move(first: int, second: int) -> Move:
    row1, col1 = row_col(first)
    row2, col2 = row_col(second)
    if row1 == row2:
        col = min(col1, col2)
        left = index(row1, col)
        return Move(row1, col, "A", left, left + 1)
    row = min(row1, row2)
    top = index(row, col1)
    return Move(row, col1, "B", top, top + N)


def apply_move(grid: list[int], move: Move) -> None:
    a, b = grid[move.first], grid[move.second]
    if a == b:
        raise ValueError("mouvement inactif")
    value = (-a - b) % 3
    grid[move.first] = value
    grid[move.second] = value


def target(grid: list[int]) -> int:
    return sum(grid) % 3


def defects(grid: list[int], t: int) -> list[int]:
    return [cell for cell, value in enumerate(grid) if value != t]


def manhattan(a: int, b: int) -> int:
    row1, col1 = row_col(a)
    row2, col2 = row_col(b)
    return abs(row1 - row2) + abs(col1 - col2)


def adjacent_opposite(grid: list[int], t: int) -> Move | None:
    for cell in defects(grid, t):
        for other in neighbors(cell):
            if cell < other and grid[other] != t and grid[cell] != grid[other]:
                return pair_move(cell, other)
    return None


def target_neighbors(grid: list[int], cell: int, t: int) -> set[int]:
    return {other for other in neighbors(cell) if grid[other] == t}


def target_path(
    grid: list[int],
    source: int,
    goals: set[int],
    t: int,
) -> list[int] | None:
    queue = deque([source])
    previous = {source: None}
    while queue:
        cell = queue.popleft()
        if cell in goals:
            path = []
            while cell is not None:
                path.append(cell)
                cell = previous[cell]
            return list(reversed(path))
        for other in neighbors(cell):
            if other in previous:
                continue
            if other != source and grid[other] != t:
                continue
            previous[other] = cell
            queue.append(other)
    return None


def helper_for_step(
    grid: list[int],
    source: int,
    destination: int,
    t: int,
) -> int | None:
    source_row, source_col = row_col(source)
    destination_row, _ = row_col(destination)
    candidates = []
    if source_row == destination_row:
        for row in (source_row - 1, source_row + 1):
            if 0 <= row < N:
                candidates.append(index(row, source_col))
    else:
        for col in (source_col - 1, source_col + 1):
            if 0 <= col < N:
                candidates.append(index(source_row, col))
    return next(
        (cell for cell in candidates if cell != destination and grid[cell] == t),
        None,
    )


def move_defect_step(
    grid: list[int],
    source: int,
    destination: int,
    t: int,
    moves: list[Move],
) -> bool:
    helper = helper_for_step(grid, source, destination, t)
    if helper is None or grid[destination] != t:
        return False
    for move in (
        pair_move(source, helper),
        pair_move(source, destination),
        pair_move(source, helper),
    ):
        apply_move(grid, move)
        moves.append(move)
    return True


def pair_cost(grid: list[int], a: int, b: int, t: int) -> int:
    best = N * N
    for source, goal_defect in ((a, b), (b, a)):
        goals = target_neighbors(grid, goal_defect, t)
        path = target_path(grid, source, goals, t)
        if path is not None:
            best = min(best, len(path))
    if best < N * N:
        return best
    return manhattan(a, b) + N * N


def move_pair_together(
    grid: list[int],
    a: int,
    b: int,
    t: int,
    moves: list[Move],
) -> bool:
    for source, goal_defect in ((a, b), (b, a)):
        goals = target_neighbors(grid, goal_defect, t)
        path = target_path(grid, source, goals, t)
        if path is None:
            continue
        snapshot = grid[:]
        old_len = len(moves)
        current = source
        for next_cell in path[1:]:
            if not move_defect_step(grid, current, next_cell, t, moves):
                grid[:] = snapshot
                del moves[old_len:]
                break
            current = next_cell
        else:
            if grid[current] != grid[goal_defect]:
                move = pair_move(current, goal_defect)
                apply_move(grid, move)
                moves.append(move)
                return True
            grid[:] = snapshot
            del moves[old_len:]
    return False


def convert_one_defect(grid: list[int], t: int, moves: list[Move]) -> bool:
    for cell in defects(grid, t):
        for other in neighbors(cell):
            if grid[other] == t:
                move = pair_move(cell, other)
                apply_move(grid, move)
                moves.append(move)
                return True
    return False


def convert_defect(grid: list[int], cell: int, t: int, moves: list[Move]) -> bool:
    for other in neighbors(cell):
        if grid[other] == t:
            move = pair_move(cell, other)
            apply_move(grid, move)
            moves.append(move)
            return True
    return False


def same_color_triplets(grid: list[int], t: int) -> list[tuple[int, int]]:
    triplets = []
    for color in range(3):
        if color == t:
            continue
        colored = [cell for cell in defects(grid, t) if grid[cell] == color]
        for center in colored:
            if not any(grid[other] == t for other in neighbors(center)):
                continue
            distances = sorted(
                manhattan(center, other) for other in colored if other != center
            )
            if len(distances) >= 2:
                triplets.append((distances[0] + distances[1], center))
    return sorted(triplets)


def convert_compact_triplet(
    grid: list[int],
    t: int,
    moves: list[Move],
    pair_distance: int,
) -> bool:
    triplets = same_color_triplets(grid, t)
    if not triplets or triplets[0][0] > 2.2 * pair_distance:
        return False
    _, center = triplets[0]
    return convert_defect(grid, center, t, moves)


def solve_from_grid(initial: list[int]) -> tuple[int, list[Move]]:
    grid = initial[:]
    t = target(grid)
    moves: list[Move] = []

    while defects(grid, t):
        move = adjacent_opposite(grid, t)
        if move is not None:
            apply_move(grid, move)
            moves.append(move)
            continue

        pairs = sorted(
            [
                (pair_cost(grid, a, b, t), a, b)
                for i, a in enumerate(defects(grid, t))
                for b in defects(grid, t)[i + 1 :]
                if grid[a] != grid[b]
            ]
        )
        if not pairs:
            if convert_one_defect(grid, t, moves):
                continue
            raise RuntimeError("plus aucun mouvement utile")

        if convert_compact_triplet(grid, t, moves, pairs[0][0]):
            continue

        for _, a, b in pairs:
            if move_pair_together(grid, a, b, t, moves):
                break
        else:
            raise RuntimeError("échec du rapprochement des défauts")

    return t, moves


def serial_from_moves(moves: list[Move]) -> str:
    rows = "".join(chr(ord("a") + move.row) for move in moves)
    cols = "".join(chr(ord("a") + move.col) for move in moves)
    directions = "".join(move.direction for move in moves)
    return rows + cols + directions

Pour résoudre une instance complète, il reste seulement à construire la grille $S$ depuis le nom d’utilisateur avec la fonction build_grid donnée plus haut.

Limite de longueur

Le binaire lit le serial avec :

fgets(serial, 0x1000, stdin);

Il peut donc lire au plus 4095 caractères d’entrée utiles. Chaque mouvement utilise trois caractères de serial. La limite est donc de 1365 mouvements :

floor(4095 / 3) = 1365 mouvements

Avec le solveur déterministe, les serials obtenus sont très loin de cette limite.

Client final

Pour résoudre tout le service, on applique le même solveur déterministe à chaque nom d’utilisateur demandé.

Le client final reprend trois blocs :

lire le nom d’utilisateur envoyé par le service
générer la grille $S$ et la cible correspondante
construire un serial déterministe, puis l’envoyer

La boucle d’automatisation finale peut être ajoutée à la suite des deux blocs Python précédents :

"""Résout le service en ligne triceratops."""

import re
import socket
import sys
from re import Pattern

HOST = "127.0.0.1"
PORT = 4000
PROMPT = b">>> "
MAX_MOVES = 1365
USERNAME_RE: Pattern[bytes] = re.compile(rb"username: ([^\r\n]+)")


def initial_grid(username: str) -> list[int]:
    """Construit la grille S initiale depuis le username."""
    up = build_grid(username, down=False)
    down = build_grid(username, down=True)
    for i, (u, d) in enumerate(zip(up, down, strict=True)):
        if u == d:
            up[i] = (u + 1) % 3
            down[i] = (d + 2) % 3
    return [(u + d) % 3 for u, d in zip(up, down, strict=True)]


def recv_until(sock: socket.socket, marker: bytes) -> bytes:
    """Lit une socket jusqu'à un marqueur ou jusqu'à fermeture."""
    data = bytearray()
    while marker not in data:
        chunk = sock.recv(4096)
        if not chunk:
            break
        data.extend(chunk)
    return bytes(data)


def find_serial(username: str) -> str:
    """Construit un serial valide avec le solveur déterministe."""
    _target, moves = solve_from_grid(initial_grid(username))
    grid = initial_grid(username)
    for move in moves:
        apply_move(grid, move)
    if any(value != grid[0] for value in grid):
        raise RuntimeError(username)
    if len(moves) > MAX_MOVES:
        raise RuntimeError(username)
    return serial_from_moves(moves)


with socket.create_connection((HOST, PORT)) as sock:
    while True:
        data = recv_until(sock, PROMPT)
        if b"flag" in data.lower():
            sys.stdout.write(data.decode())
            break
        match = USERNAME_RE.search(data)
        if match is None:
            raise RuntimeError(data.decode(errors="replace"))
        username = match.group(1).decode()
        sock.sendall(find_serial(username).encode() + b"\n")

Exécution finale

L’exécution finale a résolu :

FCSC2021
50 noms d'utilisateur aléatoires

Les serials générés restent très largement sous la limite de 1365 mouvements.

Le service a alors affiché :

Well done! Here is the flag:
FCSC{33e678eba72fbadb38386a7f2a79b5aedc8e93240d7632d360efa4ccef7cb6e2}

Validation locale

Pour valider un serial contre le binaire interne du conteneur, on peut envoyer le nom d’utilisateur puis le serial sur l’entrée standard :

{
  printf 'FCSC2021\n'
  printf '%s\n' "$SERIAL"
} | docker exec -i <container> /app/triceratops

La sortie attendue est :

[+] Valid username/serial! Now write a keygen.

Commentaire sur la conception

Le challenge donne l’impression d’un problème volontairement plus compliqué que sa structure réduite. Le binaire manipule deux couches up et down, une table de signatures et des réécritures locales qui semblent dépendre de quatre variables. Cette représentation pousse naturellement à raisonner sur l’état complet.

La réduction à la grille $S$ montre pourtant que, sur les états atteignables, la condition d’acceptation ne dépend plus que de deux valeurs voisines de $S$. Cette complexité apparente sert surtout à cacher le coeur du problème. Le solveur devient simple uniquement après avoir identifié le bon invariant et la bonne projection.

Il ne faut pas chercher à optimiser directement le modèle à deux couches. Il faut d’abord identifier les contraintes invariantes et projeter le problème sur les variables qui portent réellement la dynamique.

Conclusion

Le coeur mathématique du challenge est une grille $S$ 16x16 à trois états. Le serial décrit un chemin de réécritures locales autorisées. L’invariant modulo 3 fixe la valeur constante de l’état final. La réduction à la grille $S$ transforme ensuite le problème en annihilation de défauts de deux couleurs.