🇫🇷 FCSC | FCSCLang ⭐⭐⭐

Reverse: FCSCLang ⭐⭐⭐

Introduction

On ouvre l’archive et on découvre

• fcsclang un binaire ELF 64-bit.
• libfcsclang.so une librairie ELF 64 bit.
• program.fcsc un grand fichier texte.

Pour lancer correctement le binaire, il nous faut la version 0.22 de libtree-sitter

On remarque imédiatement que program.fcsc contient du texte complètement lisible, c’est même la copie du voyage au centre de la terre de Jules Vernes, avec quelques legères modifications notement sur la ponctuation et les espaces.

Après une rapide recherche, on apprend que tree-sitter est un outil de parsing de language vers un AST, il permet aussi d’interagir avec les nodes.

NOTE: Pour le reste du write-up, la base address du binaire sera 0x555555554000

Setup du reverse de fcsclang

Le programme va dans un 1er temps:

• Acceder au fichier qu’on lui fournit en 1er argument.
• Va accéder à libfcsclang.so qui contient le language.

Etant donné que le programme a visiblement été compilé en C sans essai de tromper / casser la décompilation on va pouvoir effectuer quelques étapes pour être à l’aise.

On va télécharger sur github la version 0.22 de tree-sitter, ensuite sur ghidra:

File -> Parse C source -> Sources files to parse -> Selectionner tree-sitter-0.22.0/lib/api.h et tree-sitter-0.22.0/lib/src/tree.h

On a donc l’ensemble des structures utilisées par le binaire, notement TSTree et TSNode qui vont nous être très utiles pour la suite.

Mais on peut faire encore mieux, avec ghidra2dwarf on va exporter nos symboles pour générer un nouveau binaire fcsclang_dbg. (Il faut quand même faire un peu attention en utilisant ça, surtout la correlation symbole / pointeur).

On a donc avec notre debugger préféré les symboles du binaire (si celui-ci supporte le format DWARF). On va pouvoir se concentrer uniquement sur le code de l’interpreteur. (Je ré exporte les symboles au fur et a mesure de la comprehension du binaire pour avoir continuelement à jour les symboles.)

L’interpreteur

Contrairement à ce qu’on trouve en CTF la majorité du temps, ce n’est pas une VM dans le sens ou le binaire va lire chaque octet avec des registres et une mémoire virtuelle. Puis interpréter les opcodes comme une architecture classique. C’est un language interprété, exactement comme python.

Plus précisément le language (en texte) va être converti en un AST (Abstract Syntaxt Tree). Qui va être intérpété. Chaque élément va être une “node” qui a un type, et qui va dans la majorité des cas contenir une autre node, jusqu’à tomber sur une expression logique comme une opération ou une assignation.

libfcsclang.so n’est pas vraiment la cible du programme à reverse, étant donné qu’il contient une structure propre à libtree-sitter TsLanguage, qui contient surtout le lexer, qui est la partie du language chargée de comprendre la syntaxe du language et quoi en faire c’est lui qui va créer des nodes à partir de notre texte.

L’interpreteur est récursif, c’est à dire qu’il va traiter la 1ere node, puis la même fonction à l’interieur de la fonction sera appellée avec une autre node “enfant” de celle ci.

Voici une version plus ou moins realiste de ce à quoi un AST ressemblerait pour une fonction donnée (syntaxe python):

A noter aussi que chaque node possède un contexte, qui corréspond à un tableau pour permettre de remonter des informations d’une node, étant donné que chaque node est évaluée elle peut en conséquence remonter une valeur.

Résoudre le problème

Le 1er objectif a été de trouver une “side channel”, c’est à dire dynamiquement trouver une comparaison entre mon entrée et quelque chose qui est ou qui pourrait être le flag. On pourrait donc “leaker” le flag sans vraiment s’embêter à devoir faire tout le travail.

On peut essayer plusieurs stratégies, se poser sur le handler d’assignement d’une valeur et regarder quelle valeur est assignée à quoi, ou alors regarder quelle valeur est comparée à quoi.

Par exemple cette fonction ici represente le handler de toutes les operations possibles sur deux expressions

On a aussi un autre problème, tous les handlers de node ne sont pas documentés et je ne les ai pas encore analysés. On va devoir sauter ça pour notre essai de side channel.

On va rapidement coder un petit script gdb franchement pas glorieux pour nous ajouter des nouvelles commandes custom

ça fonctionne car souvenez vous mon binaire a des symboles de debug, sans ça il faudrait exprimer de manière explicite les appels et les types de retours.

import gdb

class DumpNode(gdb.Command):
    def __init__(self):
        super().__init__("dump_node", gdb.COMMAND_USER)

    def invoke(self, arg, from_tty):
        expr = f"*(TSNode*)({arg})"
        self._dump(expr, 0)

    def _dump(self, node_expr, depth):
        indent = "  " * depth        
        typ = gdb.parse_and_eval(f"ts_node_type({node_expr})").string()
        
        val = ""            
        print(f"{indent}- {typ} {val}")

        cnt = int(gdb.parse_and_eval(f"ts_node_child_count({node_expr})"))
        for i in range(cnt):
            child_expr = f"ts_node_child({node_expr}, {i})"
            self._dump(child_expr, depth+1)

class DumpExpr(gdb.Command):
    def __init__(self):
        super().__init__("dump_expr", gdb.COMMAND_USER)

    def invoke(self, arg, from_tty):
        self._dump(arg)

    def _dump(self, arg):
        gdb.execute(f"x/2xg FUN_555555557b97(*(uint64_t*)0x55555555b158,{arg})")
            
DumpNode()
DumpExpr()

On peut donc évaluer des expressions grâce à leur nom (mon entrée = 0xdeadbeef)

On peut aussi afficher l’arbe des enfants de la node à partir de l’adresse de celle-ci

Malheureusement le challenge est bien fait. Mise à part quelques pistes (notement un tableau de 9x9 initialisé, possiblement un sudoku). J’ai décidé d’abandonner l’idée de solve uniquement dynamiquement et de passer aux choses serieuses.

De l’AST au python

Il y’a une bonne moitié des types de nodes qui sont déjà nommées et ne demandent quasiment aucun travail de reverse, la stratégie va être de loader le language en python. Grâce à l’api python py-tree-sitter on va pouvoir charger notre language pour parser program.fcsc et ainsi travailler avec le même AST que fcsclang.

J’ai choisi la fonction 0.21.3 de py-tree-sitter pour pouvoir travailler avec des languages en version 14 sans pour autant avoir à subir le changement d’api qui semble rendre le chargement de languages custom beaucoup plus complexe.

from tree_sitter import Language, Parser
l = Language("libfcsclang.so", "fcsclang")
source_bytes = open("program.fcsc", "rb").read()
parser = Parser()

parser.set_language(l)
tree = parser.parse(source_bytes)

root_node = tree.root_node

Il va ensuite falloir identifier les types non documentés.

On a alors

les chiffres:

undocumented_732293a7c7094ffd : 0
undocumented_f9bfceb10223dcd6 : 1
undocumented_d53cabc7357ff2a5 : 2
undocumented_210eb81a94b8b633 : 3
undocumented_c589a8f3aaff75f7 : 4
undocumented_ac7469dafc6e9c77 : 5
undocumented_8212463fe42cc213 : 6
undocumented_791df7d09856e81f : 7
undocumented_db9dce746e821769 : 8
undocumented_ac3fcec30d0b6a40 : 9

les expressions:

undocumented_0fe135eb8cd073ef: print
undocumented_af0dbc52101afc49: print
undocumented_9bfdf82a969d10c2: input
undocumented_48359b1cc713e5a1: if
undocumented_c44ff70e0a035b84: while

les operations / comparateurs:

undocumented_46eb8e8b7b15c3d5:  + 
undocumented_cfd09200be51d38f:  - 
undocumented_b341f271c655aaee:  * 
undocumented_956dd300d7424ff3:  ==
undocumented_0162f13a50afff09:  !=
undocumented_a91bdbbce9e82238:  < 
undocumented_589a700aed48e3a4:  > 
undocumented_2d5b46a88151170b:  <=
undocumented_4c3cc3b8907e3db5:  >=
undocumented_aa1bd5b44f53714d:  &&
undocumented_0e772940f0fd3008:  ||
undocumented_13932b8a4b1bd439:  <<
undocumented_0cd2df8843187030:  >>
undocumented_b858202486aecd0f:  | 
undocumented_24e094c9759dc06c:  & 

Une fois qu’on a tout, il faut construire un handler récursif, comme le handler du programme. On arrive avec le programme suivant:

from tree_sitter import Language, Parser
l = Language("libfcsclang.so", "fcsclang")
source_bytes = open("program.fcsc", "rb").read()

known = {
    "undocumented_732293a7c7094ffd" : 0,
    "undocumented_f9bfceb10223dcd6" : 1,
    "undocumented_d53cabc7357ff2a5" : 2,
    "undocumented_210eb81a94b8b633" : 3,
    "undocumented_c589a8f3aaff75f7" : 4,
    "undocumented_ac7469dafc6e9c77" : 5,
    "undocumented_8212463fe42cc213" : 6,
    "undocumented_791df7d09856e81f" : 7,
    "undocumented_db9dce746e821769" : 8,
    "undocumented_ac3fcec30d0b6a40" : 9,

    "undocumented_46eb8e8b7b15c3d5": ' + ' ,
    "undocumented_cfd09200be51d38f": ' - ' ,
    "undocumented_b341f271c655aaee": ' * ' ,
    "undocumented_956dd300d7424ff3": ' == ',
    "undocumented_0162f13a50afff09": " != ",
    "undocumented_a91bdbbce9e82238": ' < ' ,
    "undocumented_589a700aed48e3a4": ' > ' ,
    "undocumented_2d5b46a88151170b": ' <= ',
    "undocumented_4c3cc3b8907e3db5": ' >= ',
    "undocumented_aa1bd5b44f53714d": ' && ',
    "undocumented_0e772940f0fd3008": ' || ',
    "undocumented_13932b8a4b1bd439": ' << ',
    "undocumented_0cd2df8843187030": ' >> ',
    "undocumented_b858202486aecd0f": ' | ' ,
    "undocumented_24e094c9759dc06c": ' & ',
}
knowfunc = {
    "undocumented_0fe135eb8cd073ef": "print",
    "undocumented_af0dbc52101afc49": "print",
    "undocumented_9bfdf82a969d10c2": "input",
    "undocumented_48359b1cc713e5a1": "if",
    "undocumented_c44ff70e0a035b84": "while",

}
def get_node_val(node):
    return node.text.decode('utf-8').replace('\n','')
def get_node_identifier(node):
    return node.child_by_field_name("identifier")

def recurs_get_elm(node, depth, elmlist):
    if(node):
        elm = node.child_by_field_name("element")
        elmlist.append(elm)
        return recurs_get_elm(node.child_by_field_name("next"), depth+1, elmlist)
    else:
        return elmlist
def get_elm_arr(node):
    liste = node.child_by_field_name("list")
    if(not liste):
        print("error: no list")
        exit(1)
    elmlist = []
    return recurs_get_elm(liste, 0, elmlist)


def recurs_get_param(node, depth, arglist):
    if(not node):
        return arglist
    else:
        param = node.child_by_field_name("param")
        arglist.append(param)
        return recurs_get_param(node.child_by_field_name("next"), depth+1, arglist)

def recurs_get_param_func(node, depth, arglist):
    if(not node):
        return arglist
    else:
        param = node.child_by_field_name("identifier")
        arglist.append(param)
        return recurs_get_param_func(node.child_by_field_name("next"), depth+1, arglist)


def get_parameters(node):
    param = node.child_by_field_name("parameters")
    if(not param):
        print("error: no params...")
        exit(1)
    liste = param.child_by_field_name("list")
    if(not liste):
        print("error: no list")
        exit(1)
    arglist = []
    return recurs_get_param(liste, 0, arglist)

def get_parameters_func(node):
    liste = node.child_by_field_name("list")
    if(not liste):
        print("error: no list")
        exit(1)
    arglist = []
    return recurs_get_param_func(liste, 0, arglist)

INDENT_PADDING = "\t"
supported = ["function_call", "function_definition", "assign", "array", "binexp", "subscript","unexp", "if", "while", "statement", "str", "print", "input"]
def print_node(node, indent=""):
    type_ = node.type
    cont = True
    if(type_ in known.keys()):
        type_ = known[type_]
        print(type_, end="")
        return
    if(type_ in knowfunc.keys()):
        type_ = knowfunc[type_]
    if(indent and type_ in supported):
        print(indent, end="")
        
        
        
    if type_ == supported[9]:
        print("")
    if type_ == supported[10]:
        print(get_node_val(node),end="") 
    elif type_ == supported[11]:
        print("print(",end="")
        print_node(node.child_by_field_name("param"))
        print(")",end="")
    elif type_ == supported[12]:
        print("input()",end="")
    elif type_ == "identifier":
        print(get_node_val(node),end="")

    elif type_ == supported[0]:
        print(get_node_val(get_node_identifier(node)),end="")
        print("(",end="")        
        for x in get_parameters(node):
            print_node(x)
            print(", ", end="")
        print(")",end="")
    elif type_ == supported[1]:
        print("\ndef", get_node_val(get_node_identifier(node)),end="(")
        for child in node.children:
            if(child.type == "arguments"):
                # print([get_parameters_func(child)])
                print(", ".join([get_node_val(x) for x in get_parameters_func(child)]),end="):")
            if(child.type == "scope"):
                print_node(child, indent + INDENT_PADDING)
        
    elif type_ == supported[2]:
        print_node(node.child_by_field_name("lvalue"))
        print(" = ",end="")
        print_node(node.child_by_field_name("value"))
    elif type_ == supported[3]:
        print("[",end="")
        for x in get_elm_arr(node):
            print_node(x)
            print(", ", end="")
        print("]",end="")

    elif type_ == supported[4]:
        op = node.child_by_field_name("op")
        left = op.child_by_field_name("left")
        right = op.child_by_field_name("right")
        print_node(left)
        print_node(op)
        print_node(right)

    elif type_ == supported[5]:
        print_node(node.child_by_field_name("array"))
        print("[",end="")
        print_node(node.child_by_field_name("index"))
        print("]",end="")
    elif type_ == supported[6]:
        argument = node.child_by_field_name("op").child_by_field_name("argument")
        print_node(argument)
        print(" == 0",end="")
    elif type_ == supported[7]:
        expr = node.child_by_field_name("undocumented_f543173dbe320d3f")
        zero = node.child_by_field_name("undocumented_75dc81fb2f8d9ce3")
        notzero = node.child_by_field_name("undocumented_f1e6bfd0a35c19db")
        print("if((",end="")
        print_node(expr)
        print(") == True):",end="")
        for child in notzero.children:
                print_node(child, indent + INDENT_PADDING)
        if(zero):
            print("else:",end="")
            for child in zero.children:
                    print_node(child, indent + INDENT_PADDING)
    elif type_ == supported[8]:
        expr = node.child_by_field_name("undocumented_f543173dbe320d3f")
        loop = node.child_by_field_name("undocumented_a1a48da3b527af4e") 
        print("while(", end="")
        print_node(expr)
        print("):",end="")
        for child in loop.children:
                print_node(child, indent + INDENT_PADDING)
    else:   
        if(cont):
            for child in node.children:
                print_node(child, indent)

def parcours_node(node):
    print_node(node)

parser = Parser()
parser.set_language(l)
tree = parser.parse(source_bytes)

root_node = tree.root_node
if(root_node):
    parcours_node(root_node)

L’affichage de chaque élément de la node a volontairement été formatté pour ressembler au python, j’ai pas une bonne idée de la complexité du programme et je pourrais avoir à analyser un code vraiment complexe.

Voici la sortie:

consterner = [[0, 0, 0, 0, 0, 0, 0, 1, 8, ], [0, 0, 5, 6, 1, 0, 0, 2, 0, ], [3, 0, 0, 0, 0, 0, 5, 1, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 2, ], [1, 0, 0, 0, 3, 0, 0, 4, 4, ], [0, 0, 0, 0, 2, 1, 0, 0, 5, ], [0, 0, 0, 0, 4, 3, 0, 6, 1, ], [3, 1, 0, 1, 0, 6, 0, 0, 0, ], [0, 0, 4, 7, 0, 0, 0, 6, 7, ], ]
routine = [[0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 0, 0, 0, 0, ], ]
def inattendu(inoffensif):	
	compulser = 0	
	bienveillante = 0	
	divin = 1	
	while(compulser < 9):		
		ah = inoffensif[compulser]		
		artifice = 1 << ah		
		divin = bienveillante & artifice == 0 && divin		
		divin = ah <= 9 && ah > 0 && divin		
		bienveillante = bienveillante | artifice		
		compulser = compulser + 1	
divin
def bidonner(conduit):	
	hameau = 0	
	divin = 1	
	while(hameau < 9):		
		divin = inattendu(conduit[hameau], ) && divin		
		hameau = hameau + 1	
divin
def mendiant(conduit, compulser):	
	hameau = 0	
	bienveillante = 0	
	divin = 1	
	while(hameau < 9):		
		ah = conduit[hameau][compulser]		
		artifice = 1 << ah		
		divin = bienveillante & artifice == 0 && divin		
		bienveillante = bienveillante | artifice		
		hameau = hameau + 1	
divin
def symboles(conduit):	
	compulser = 0	
	divin = 1	
	while(compulser < 9):		
		divin = mendiant(conduit, compulser, ) && divin		
		compulser = compulser + 1	
divin
def copie(culottes, japonais):	
	divin = [0, 0, 0, 0, 0, 0, 0, 0, 0, ]	
	embrasser = 0	
	aiguille = 0	
	while(embrasser < 3):		
		ventre = 0		
		while(ventre < 3):			
			divin[aiguille] = [culottes * 3 + embrasser, japonais * 3 + ventre, ]			
			ventre = ventre + 1			
			aiguille = aiguille + 1		
		embrasser = embrasser + 1	
divin
def aux(conduit, culottes, japonais):	
	escroc = copie(culottes, japonais, )	
	aiguille = 0	
	bienveillante = 0	
	divin = 1	
	while(aiguille < 9):		
		hameau = escroc[aiguille][0]		
		compulser = escroc[aiguille][1]		
		ah = conduit[hameau][compulser]		
		artifice = 1 << ah		
		divin = bienveillante & artifice == 0 && divin		
		bienveillante = bienveillante | artifice		
		aiguille = aiguille + 1	
divin
def discutable(conduit):	
	hameau = 0	
	divin = 1	
	while(hameau < 3):		
		compulser = 0		
		while(compulser < 3):			
			divin = aux(conduit, hameau, compulser, ) && divin			
			compulser = compulser + 1		
		hameau = hameau + 1	
divin
def central(hameau, compulser, baffe):	
	divin = [0, 0, 0, 0, ]	
	divin[0] = [hameau + baffe, compulser, ]	
	divin[1] = [hameau - baffe, compulser, ]	
	divin[2] = [hameau, compulser + baffe, ]	
	divin[3] = [hameau, compulser - baffe, ]	
divin
def gerber(conduit, hameau, compulser, baffe):	
	divin = 0	
	escroc = central(hameau, compulser, baffe, )	
	aiguille = 0	
	while(aiguille < 4):		
		cyclistes = escroc[aiguille][0]		
		paisible = escroc[aiguille][1]		
		if((cyclistes < 9 && paisible < 9 && cyclistes >= 0 && paisible >= 0) == True):			
			divin = conduit[cyclistes][paisible] == baffe || divin		
		aiguille = aiguille + 1	
divin
def ferrailleur(conduit, poser):	
	hameau = 0	
	divin = 1	
	while(hameau < 9):		
		compulser = 0		
		while(compulser < 9):			
			baffe = poser[hameau][compulser]			
			if((baffe != 0) == True):				
				divin = gerber(conduit, hameau, compulser, baffe, ) && divin			
			compulser = compulser + 1		
		hameau = hameau + 1	
divin
def lancinante(conduit, poser):	
	divin = bidonner(conduit, )	
	divin = symboles(conduit, ) && divin	
	divin = discutable(conduit, ) && divin	
	divin = ferrailleur(conduit, poser, ) && divin	
divin
def pipe(conduit):	
	hameau = 0	
	while(hameau < 9):		
		compulser = 0		
		while(compulser < 9):			
			ah = input()			
			conduit[hameau][compulser] = ah			
			compulser = compulser + 1		
		hameau = hameau + 1
def venture(conduit):	
	hameau = 0	
	while(hameau < 9):		
		compulser = 0		
		while(compulser < 9):			
			print(conduit[hameau][compulser])			
			print(" ")			
			compulser = compulser + 1		
		print("")		
		hameau = hameau + 1
def dictature(conduit):	
	print("FCSC{")	
	hameau = 0	
	while(hameau < 9):		
		compulser = 0		
		while(compulser < 9):			
			print(conduit[hameau][compulser])			
			compulser = compulser + 1		
		hameau = hameau + 1	
	print("}")
pipe(routine, )
if((lancinante(routine, consterner, )) == True):	
	dictature(routine, )	
else:	
	print("No")	

On le remarque imédiatement, il s’agit bien d’un sudoku, mais un sudoku custom.

On a:

• pipe(routine) : lit 81 entrées utilisateur et les stocke dans routine[0..8][0..8].
• Lignes (bidonner → inattendu) : pour chaque ligne, il vérifie unicité de 1 à 9 sans répétition ni hors‑plage.
• Colonnes (symboles → mendiant) : même check appliqué aux colonnes.
• Vérification “masque” (ferrailleur + gerber), gerber calcule les 4 voisins à coté de chaque élément.
• Si toutes les verifications passent, lancinante est vrai et on nous affiche le flag (le sudoku résolut).
• Si échec alors on nous affiche “No”.

ça tombe bien, avec le teaser de cette année, j’ai un script z3 tout fait pour travailler avec des sudokus. Mais pour un 9x9 j’ai préféré adapter un script que j’ai trouvé sur github.

J’ai récupéré la valeur de “escroc” en la recalculant en python pour faciliter le travail avec z3

def copie(culottes, japonais):    
    divin = [0, 0, 0, 0, 0, 0, 0, 0, 0, ]    
    embrasser = 0    
    aiguille = 0    
    while(embrasser < 3):
        ventre = 0
        while(ventre < 3):
            divin[aiguille] = [culottes * 3 + embrasser, japonais * 3 + ventre, ]
            ventre = ventre + 1
            aiguille = aiguille + 1
        embrasser = embrasser + 1    
    return divin

for x in range(9):
    for y in range(9):
        print(copie(x,y))

from z3 import *

sudoku_puzzle = [
[0, 0, 0, 0, 0, 0, 0, 1, 8],
[0, 0, 5, 6, 1, 0, 0, 2, 0], 
[3, 0, 0, 0, 0, 0, 5, 1, 0], 
[0, 0, 0, 0, 0, 0, 0, 0, 2], 
[1, 0, 0, 0, 3, 0, 0, 4, 4], 
[0, 0, 0, 0, 2, 1, 0, 0, 5], 
[0, 0, 0, 0, 4, 3, 0, 6, 1], 
[3, 1, 0, 1, 0, 6, 0, 0, 0], 
[0, 0, 4, 7, 0, 0, 0, 6, 7]]

sudoku_grid = [[Int(f"cell*{row}\_{col}") for col in range(9)]
               for row in range(9)]
cell_constraints = [
    And(1 <= cell, cell <= 9)
    for row in sudoku_grid
    for cell in row
]

row_constraints = [Distinct(row) for row in sudoku_grid]

col_constraints = [
    Distinct([sudoku_grid[row][col] for row in range(9)])
    for col in range(9)
]

subgrid_constraints = [
    Distinct([
        sudoku_grid[3 * block_row + row][3 * block_col + col]
        for row in range(3)
        for col in range(3)
    ])
    for block_row in range(3)
    for block_col in range(3)
]


all_constraints = cell_constraints + row_constraints + col_constraints + subgrid_constraints


solver = Solver()
solver.add(all_constraints)
escrocs = [[[1, 7], [-1, 7], [0, 8], [0, 6]], [[8, 8], [-8, 8], [0, 16], [0, 0]], [[6, 2], [-4, 2], [1, 7], [1, -3]], [[7, 3], [-5, 3], [1, 9], [1, -3]], [[2, 4], [0, 4], [1, 5], [1, 3]], [[3, 7], [-1, 7], [1, 9], [1, 5]], [[5, 0], [-1, 0], [2, 3], [2, -3]], [[7, 6], [-3, 6], [2, 11], [2, 1]], [[3, 7], [1, 7], [2, 8], [2, 6]], [[5, 8], [1, 8], [3, 10], [3, 6]], [[5, 0], [3, 0], [4, 1], [4, -1]], [[7, 4], [1, 4], [4, 7], [4, 1]], [[8, 7], [0, 7], [4, 11], [4, 3]], [[8, 8], [0, 8], [4, 12], [4, 4]], [[7, 4], [3, 4], [5, 6], [5, 2]], [[6, 5], [4, 5], [5, 6], [5, 4]], [[10, 8], [0, 8], [5, 13], [5, 3]], [[10, 4], [2, 4], [6, 8], [6, 0]], [[9, 5], [3, 5], [6, 8], [6, 2]], [[12, 7], [0, 7], [6, 13], [6, 1]], [[7, 8], [5, 8], [6, 9], [6, 7]], [[10, 0], [4, 0], [7, 3], [7, -3]], [[8, 1], [6, 1], [7, 2], [7, 0]], [[8, 3], [6, 3], [7, 4], [7, 2]], [[13, 5], [1, 5], [7, 11], [7, -1]], [[12, 2], [4, 2], [8, 6], [8, -2]], [[15, 3], [1, 3], [8, 10], [8, -4]], [[14, 7], [2, 7], [8, 13], [8, 1]], [[15, 8], [1, 8], [8, 15], [8, 1]]]

idx = 0
for i in range(9):
    for j in range(9):
        val = sudoku_puzzle[i][j]
        if val != 0:
            contenu = []
            for x, y in escrocs[idx]:
                if (0 <= x < 9 and 0 <= y < 9):
                    contenu.append(sudoku_grid[x][y])
            solver.add(Or([elem == val for elem in contenu]))
            idx+=1

if solver.check() == sat:
    model = solver.model()
    solution = [
        [model.evaluate(sudoku_grid[row][col]) for col in range(9)] for row in range(9)
    ]
    
    stri = ""
    for elm in solution:
        print(elm)
        stri+="".join([str(x) for x in elm])
    print(stri)
else:
    print("Skill issue ???")

Voici la sortie du script z3

[8, 3, 6, 2, 1, 9, 7, 5, 4]
[5, 4, 9, 7, 8, 6, 3, 1, 2]
[1, 2, 7, 3, 4, 5, 9, 6, 8]
[6, 5, 8, 1, 9, 3, 4, 2, 7]
[3, 1, 4, 8, 2, 7, 6, 9, 5]
[7, 9, 2, 5, 6, 4, 8, 3, 1]
[9, 6, 5, 4, 7, 1, 2, 8, 3]
[4, 8, 1, 6, 3, 2, 5, 7, 9]
[2, 7, 3, 9, 5, 8, 1, 4, 6]
836219754549786312127345968658193427314827695792564831965471283481632579273958146

FLAG: FCSC{836219754549786312127345968658193427314827695792564831965471283481632579273958146}

Conclusion

Un challenge vraiment hors de l’ordinaire que j’ai totalement adoré. Je me demande encore comment c’est possible d’avoir fait un challenge aussi complet avec un résultat final aussi proche d’un roman.