Contexte
Trouver un moyen d’afficher le flag à partir du programme chiffre-unique. L’utilisation d’outils d’ingénierie inverse (Ghidra, Hex-Rays, RetDec, Binary Ninja, …) va permettre d’analyser le programme.
Analyse
Recherche du point d’entrée du programme:
$ readelf -h chiffre-unique
En-tête ELF:
Magique: 7f 45 4c 46 02 01 01 00 00 00 00 00 00 00 00 00
...
Version: 0x1
Adresse du point d'entrée: 0x1170
Début des en-têtes de programme : 64 (octets dans le fichier)
...
Table d'index des chaînes d'en-tête de section: 27
Le point d’entrée du programme se trouve donc à l’adresse 0x1170.
Décompilation par RetDec de la fonction située à l’adresse 0x1170:
// Address range: 0x1170 - 0x119b
int64_t entry_point(int64_t a1, int64_t a2, int64_t a3, int64_t a4) {
// 0x1170
int64_t v1; // 0x1170
__libc_start_main(0x10a0, (int32_t)a4, (char **)&v1, (void (*)())0x1420, (void (*)())0x1480, (void (*)())a3);
__asm_hlt();
// UNREACHABLE
}
La fonction __libc_start_main est utilisée pour appeler la foncion main qui se situe à l’adresse 0x10a0.
Décompilation par Angr et simplification de la fonction située à l’adresse 0x10a0:
input[256];
x = 0;
do {
__isoc99_scanf("%x", &c);
i = *((int *)&c);
if ((unsigned int)i > 15) {
puts("Invalid argument.");
return 1;
}
input[x] = c;
} while (x != 256);
if (!(sub_401255(&input) & sub_4012a7(&input) & sub_4012f2(&input) & sub_40136c(&input))) {
puts("Input incorrect.");
return 1;
}
puts("Congratulations ! ");
sub_40139d(&input);
return 0;
Le programme attend donc 256 caractères. Ces caractères doivent être saisis caractère par caractère et doivent tous être un caractère hexadécimal [0-9a-f].
Les 256 caractères passent ensuite par 4 fonctions de contrôle qui devront toutes retourner 1. Si c’est la cas on sera félicité et la fonction située à l’adresse 0x139d sera appellée.
Décompilation par Hex-Rays et simplification de la fonction située à l’adresse 0x139d:
x = 0;
SHA256_Init(v5);
SHA256_Update(v5, input, 256);
SHA256_Final(v4, v5);
printf("FCSC{");
do
{
v2 = (unsigned __int8)v4[x];
printf("%02x", v2);
x++;
}
while ( x != 32 );
return puts("}");
Les 256 caractères passent par une fonction de hachage SHA-256 et le flag sera le résultat de ce hachage.
Inutile donc de rechercher une quelconque vulnérabilité dans le programme.
Il va falloir saisir tous les caractères correctement et que les 4 fonctions de contrôle renvoient 1.
Analyse des 4 fonctions de contôle
Pour la suite, la fonction ctoi suivante sera utilisée:
int ctoi(char c)
{
if (c >= 'a' && c <= 'f')
{
return 10 + c - 'a';
}
if (c >= '0' && c <= '9')
{
return c - '0';
}
return -1;
}
Fonction 0x1255
Décompilation par Hex-Rays et simplification de la fonction:
p = input;
p_end = p + 256;
sum = 0;
do
{
x = 0;
bool b[16] = {0};
do
{
b[ctoi(p[x])] = 1;
x++;
}
while ( x != 16 );
for ( i = 0; i != 16; ++i )
{
sum += b[i];
}
p += 16;
}
while ( p != p_end );
return sum == 256;
La chaine de 256 caractères est divisée en 16 blocs de 16 caractères.
Pour chaque bloc, le nombre d’éléments présents parmi les 16 chiffres hexadécimaux [0-9a-f] est calculée.
Exemple, un bloc contenant 01234567890abcdef vaudra 16 car les 16 chiffres hexadécimaux sont présents.
Un bloc 0000000000000000 vaudra 1.
Les somme des valeurs des 16 blocs est finalement calculée.
Pour que cette fonction renvoie 1, il faut que cette somme soit égale à 256.
Chaque bloc doit avoir une valeur de 16 pour obtenir une somme finale de 256.
Il faut donc que chacun des blocs contienne une seule fois tous les chiffres hexadécimaux.
Fonction 0x12a7
Décompilation par Hex-Rays et simplification de la fonction:
p = input
p_end = input + 16;
bool res = 1;
do
{
bool b[16] = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1];
p_col = p;
do
{
x = ctoi(*p_col);
res &= b[x];
b[x] = 0;
p_col += 16;
}
while ( p_col != p + 256 );
p++;
}
while ( p_end != p );
return res;
Cette fonction est similaire dans le traitement à la précédente.
La chaine de 256 caractères est traitée comme une matrice 16x16.
Les 16 colonnes de cette matrice sont les 16 blocs de la fonction précédente.
A nouveau pour que cette fonction renvoie 1 il faut que chaque bloc (colonne) contienne une seule fois tous les chiffres hexadécimaux.
Interlude
A partir d’ici, on remarque une similitude avec les rêgles du sudoku mais avec une grille 16x16 et où les ensembles doivent contenir tous les chiffres hexadécimaux de 0 à f.
Fonction 0x136c
Décompilation par Hex-Rays et simplification de la fonction:
x = 0;
bool res = 1;
bool b;
do
{
c = array_3080[x];
b = input[x] == c;
x++;
res &= (c == 0xFF) || b;
}
while ( x != 256 );
return res;
Cette fonction compare la chaine de 256 caractères d’entrée avec une chaine de caractères array_3080.
Pour qu’elle renvoie 1 il faut soit que chaque élément de l’entrée ait la même valeur que l’élément correspondant de array_3080, soit que cet élément de array_3080 ait pour valeur 0xff.
On dumpe la chaine de caractères array_3080 et on remplace les 0xff par .. pour plus de lisibilité:
$ xxd -s 0x3080 -l 256 -c 16 chiffre-unique |colrm 1 10 | colrm 40 | sed 's/^ff/../g' | sed 's/ff /.. /g' | sed 's/ ff/ ../g' | sed 's/ff$/../g'
..00 0103 09.. ..05 ..0a ..02 08.. ..0e
.... 0d.. 0a06 .... 0904 .... ..03 ....
02.. 06.. 03.. .... 050d ..01 ..0b 0a..
09.. 0b.. ..02 .... 060c .... 0f.. ..05
.... 0409 0b0e .... .... 0207 ..01 ..0d
.... .... .... .... 04.. 0903 .... ....
..0c .... 0d.. 02.. 0f.. .... 0009 0704
.... 070f .... .... ..01 0d.. 0608 05..
..0d 050b 0f03 ..02 .... .... .... ..06
0708 03.. ..0a 0e.. ..0f .... .... ....
..02 ..01 04.. 0d06 .... ..0b 05.. 00..
.... ..06 0c0b ..00 ..02 ..05 ..07 0308
08.. .... 0200 ..01 0c.. ..0d .... ..09
0d.. .... .... 030f 0b.. ..04 0700 080c
0b.. .... ..09 070d ..03 .... .... ..01
..0f 0005 .... 0b.. .... .... 0d0a ....
Cela confirme à nouveau l’hypothése d’une grille type sudoku où quelques valeurs sont déjà disposées.
La dernière fonction 0x12f2 implémente la dernière rêgle avec des régions sur des carrés 4x4.
Résolution de la grille
On va utiliser le solveur Z3 de Microsoft pour compléter la grille.
On va se baser sur une implémentation disponible sur le blog de Giuseppe Cardone en l’adaptant à une grille 16x16.
#!/usr/bin/env python3
# https://www.gcardone.net/2020-06-03-solving-the-miracle-sudoku-in-z3/
import itertools
import sys
import z3
def rows():
"""Returns the indexes of rows."""
return range(0, 16)
def cols():
"""Returns the indexes of columns."""
return range(0, 16)
def sudoku_from_string(s):
"""Builds a sudoku from a string.
Args:
s: string representing a sudoku cell by cell from the top row to the
bottom road. Admissible characters are 0-9 for known values, . for
unknown values, and \n (ignored).
Returns:
A dictionary (int, int) -> int representing the known values of the
puzzle. The first int in the tuple is the row (i.e.: y coordinate),
the second int is the column (i.e.: x coordinate).
"""
valid_chars = set([str(f'{x:x}') for x in range(0, 16)])
valid_chars.add('.')
sudoku = {}
if len(s) != 256:
raise ValueError('wrong input size')
invalid_chars = set(s).difference(valid_chars)
if invalid_chars:
err_str = ', '.join(invalid_chars)
raise ValueError('unexpected character(s): %s' % err_str)
for r in rows():
for c in cols():
char = s[0]
if char != '.':
sudoku[(r, c)] = s[0]
s = s[1:]
return sudoku
def read_sudoku(f):
"""Reads a sudoku from a file-like object.
Args:
f: file object.
Returns: dictionary (int, int) -> int. See sudoku_from_string for details.
"""
sudoku = {}
invar = ''
valid_chars = set([str(f'{x:x}') for x in range(0, 15)])
valid_chars.add('.')
for l in f:
line = l.strip()
invar = invar + line
return sudoku_from_string(invar)
def solve_sudoku(known_values):
"""Solves a sudoku and prints its solution.
Args:
known_values: a dictionary of (int, int) -> int representing the known
values in a sudoku instance (i.e.: hints). The first int in
the tuple of the keys is the row (0-indexed), the second
one is the column (0-indexed).
"""
# Create a Z3 solver
s = z3.Solver()
# Create a matrix of None, which will be replaced by Z3 variables. This
# is our sudoku.
cells = [ [ None for _ in cols() ] for _ in rows() ]
for r in rows():
for c in cols():
# Z3 variables have a name
v = z3.Int('c_%d_%d' % (r, c))
# Keep a reference to the Z3 variable in our sudoku.
cells[r][c] = v
# If this cell contains a hint, then add a constraint that force
# the current variable to be equal to the hint.
# print(f'r={r}, c={c}')
if (r, c) in known_values:
# print(f'Adding {r} {c}')
s.add(v == int(known_values[(r, c)], 16))
# This function adds all the constraints of a classic sudoku
add_constraints(s, cells)
if s.check() == z3.sat:
# Retrieve the model from the solver. In this model all the variables
# are grounded (i.e.: they have a value)
m = s.model()
for r in rows():
for c in cols():
# Retrieve the grounded value and print it.
v = m.evaluate(cells[r][c]).as_long()
print(f'{v:x}', end=' ')
# Add vertical spacing for a subgrid
#if (c+1) % 3 == 0:
# print(' ', end='')
print()
# Add horizontal spacing for a subgrid
#if (r+1) % 3 == 0:
# print()
print()
def add_constraints(s, cells):
classic_constraints(s, cells)
def classic_constraints(s, cells):
"""Adds constraints to a z3 solver.
Args:
s: z3.Solver instance.
cells: a 16x16 list of lists, where each element is a z3.Int instance.
"""
# All values must be 0 <= x <= 15.
for r in rows():
for c in cols():
v = cells[r][c]
s.add(v >= 0)
s.add(v <= 15)
# All cells on the same row must be distinct.
for r in rows():
s.add(z3.Distinct(cells[r]))
# All cells on the same column must be distinct.
for c in cols():
col = [cells[r][c] for r in rows()]
s.add(z3.Distinct(col))
# All cells in a 4x4 subgrid must be distinct: for each top left cell of
# each subgrid select all the other cells in the same subgrid.
offsets = list(itertools.product(range(0, 4), range(0, 4)))
for r in range(0, 16, 4):
for c in range(0, 16, 4):
group_cells = []
for dy, dx in offsets:
group_cells.append(cells[r+dy][c+dx])
s.add(z3.Distinct(group_cells))
# Main: read a sudoku from a file or stdin
if __name__ == '__main__':
if len(sys.argv) == 2:
with open(sys.argv[1]) as f:
known_values = read_sudoku(f)
else:
known_values = read_sudoku(sys.stdin)
#print(f'{known_values}')
solve_sudoku(known_values)
Le script python attend la grille en entrée sous la forme d’une chaine de 256 caractères où chacun des caractères est soit un chiffre hexadécimal, soit un point.
$ xxd -s 0x3080 -l 256 -c 16 chiffre-unique |colrm 1 10 | colrm 40 | sed 's/^ff/../g' | sed 's/ff /.. /g' | sed 's/ ff/ ../g' | sed 's/ff$/../g' | tr '\n' ' ' | sed -E 's/[.0-9a-f]([.0-9a-f])[.0-9a-f]([.0-9a-f])/\1\2/g' | tr -d ' '
.0139..5.a.28..e..d.a6..94...3..2.6.3...5d.1.ba.9.b..2..6c..f..5..49be....27.1.d........4.93.....c..d.2.f...0974..7f.....1d.685..d5bf3.2.......6783..ae..f.......2.14.d6...b5.0....6cb.0.2.5.7388...20.1c..d...9d.....3fb..4708cb....97d.3.....1.f05..b.....da..
Utilisation d’un container pour installer Z3:
$ podman run --rm -it -v .:/workdir ubuntu:24.04
# apt update -y
# apt install -y python3-z3 bsdextrautils xxd
# cd /workdir
# time xxd -s 0x3080 -l 256 -c 16 chiffre-unique |colrm 1 10 | colrm 40 | sed 's/^ff/../g' | sed 's/ff /.. /g' | sed 's/ ff/ ../g' | sed 's/ff$/../g' | tr '\n' ' ' | sed -E 's/[.0-9a-f]([.0-9a-f])[.0-9a-f]([.0-9a-f])/\1\2/g' | tr -d ' ' | python3 sudoku_resolve.py | tee sudoku_resolve.txt
f 0 1 3 9 d 4 5 7 a b 2 8 6 c e
5 7 d 8 a 6 c b 9 4 f e 2 3 1 0
2 4 6 c 3 8 f e 5 d 0 1 9 b a 7
9 e b a 1 2 0 7 6 c 3 8 f d 4 5
a 5 4 9 b e 6 c 8 0 2 7 3 1 f d
0 1 2 d 7 f 5 8 4 6 9 3 b c e a
6 c 8 e d 1 2 3 f b 5 a 0 9 7 4
3 b 7 f 0 4 9 a e 1 d c 6 8 5 2
e d 5 b f 3 8 2 a 7 c 0 1 4 9 6
7 8 3 0 5 a e 9 1 f 4 6 c 2 d b
c 2 a 1 4 7 d 6 3 9 8 b 5 e 0 f
4 9 f 6 c b 1 0 d 2 e 5 a 7 3 8
8 3 e 7 2 0 a 1 c 5 6 d 4 f b 9
d a 9 2 6 5 3 f b e 1 4 7 0 8 c
b 6 c 4 8 9 7 d 0 3 a f e 5 2 1
1 f 0 5 e c b 4 2 8 7 9 d a 6 3
real 0m1.587s
user 0m1.503s
sys 0m0.102s
# exit
Problème résolu en moins de 2 secondes.
Utilisation de la grille
Le programme chiffre-unique a besoin de libcrypto.so.1.1 pour fonctionner.
On va utiliser un container Ubuntu 20.04 pour pouvoir l’installer :
$ podman run --rm -it -v .:/workdir ubuntu:20.04
# apt update -y
# apt install -y libssl1.1
# cd /workdir
# chmod +x ./chiffre-unique
# cat sudoku_resolve.txt | tr -d '\n' | tr ' ' '\n' | ./chiffre-unique
Congratulations !
FCSC{00119cf9663f8f5448fe632c0776484f8ca5a5d323a02b469b4cf66af54c53e6}