Cet article explore l'utilisation du solveur Z3 de Microsoft pour résoudre des systèmes d'équations, en se concentrent sur la distinction entre les types de données entiers et les vecteurs de bits, ainsi que sur la gestion des opérations bitwise.

Introduction à Z3 et aux types de données

Z3 est un solveur de contraintes puissant qui peut être utilisé pour vérifier la correctoin des programmes ou pour résoudre des problèmes mathématiques complexes. Lors de l'utilisation de Z3 en Python, il est crucial de comprendre les types de données que vous manipulez.

Initialement, un exemple utilise des variables de type Int pour représenter des entiers. Cependant, certaines opérations, comme les décalages de bits (LShR), nécessitent des expressions de type BitVec (vecteur de bits).

Problème avec Int et LShR

L'utilisation de la fonction z3.LShR avec des variables de type Int provoque une Z3Exception car cette fonction attend des expressions de type BitVec. Pour résoudre ce problème, il faut déclarer les variables comme BitVec.

from z3 import *

# Initialisation du solveur
solver = Solver()

# Déclaration des variables comme BitVec de 32 bits
variables = [0] * 10
for i in range(10):
   variables[i] = BitVec(f'variables[{i}]', 32)

# Assignation des variables pour plus de lisibilité
v1 = variables[1]
v2 = variables[0]
v3 = variables[2]
v4 = variables[3]
v5 = variables[4]
v6 = variables[6]
v7 = variables[5]
v8 = variables[7]
v9 = variables[8]
v11 = variables[9]

# Ajout des contraintes à l'aide des variables BitVec
solver.add(-85 * v9 + 58 * v8 + 97 * v6 + v7 + -45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 == 12613)
solver.add(30 * v11 + -70 * v9 + -122 * v6 + -81 * v7 + -66 * v5 + -115 * v4 + -41 * v3 + -86 * v1 - 15 * v2 - 30 * v8 == -54400)
# Note: LShR est utilisé ici, nécessitant des BitVecs
solver.add(-103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 + -89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - (LShR(v6, 6)) - 120 * v9 == -10283)
solver.add(71 * v6 + (LShR(v7, 7)) + 99 * v5 + -111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 == 22855)
solver.add(5 * v11 + 23 * v9 + 122 * v8 + -19 * v6 + 99 * v7 + -117 * v5 + -69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 == -2944)
solver.add(-54 * v11 + -23 * v8 + -82 * v3 + -85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 == -2222)
solver.add(-83 * v11 + -111 * v7 + -57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 == -13258)
solver.add(81 * v11 + -48 * v9 + 66 * v8 + -104 * v6 + -121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 + -85 * v2 + 80 * v1 == -1559)
solver.add(101 * v11 + -85 * v9 + 7 * v6 + 117 * v7 + -83 * v5 + -101 * v4 + 90 * v3 + -28 * v1 + 18 * v2 - v8 == 6308)
solver.add(99 * v11 + -28 * v9 + 5 * v8 + 93 * v6 + -18 * v7 + -127 * v5 + 6 * v4 + -9 * v3 + -93 * v1 + 58 * v2 == -1697)

# Vérification de l'existence d'une solution
if solver.check() == sat:
   model = solver.model()
   # Affichage des valeurs trouvées pour les variables
   for i in range(10):
       print(f'variables[{i}] = {model[variables[i]]}')
else:
   print("Aucune solution trouvée.")
   

Opérations bitwise et types de données

Dans le contexte des opérations bitwise comme le décalage à gauche (<<), Z3 supporte ces opérations directement avec les types Int et BitVec. Cependant, si des fonctions spécifiques aux opérations bitwise sont utilisées (comme LShR pour le décalage logique à droite), l'utilisation de BitVec est impérative.

Décalage à gauche avec BitVec

L'opérateur << peut être utilisé pour le décalage à gauche. Voici un exemple utilisant BitVec et l'opérateur de décalage à gauche :

from z3 import *

# Initialisation du solveur
solver_bv = Solver()

# Déclaration de variables comme BitVec de 8 bits pour cet exemple
v0, v1, v2, v3, v4, v5, v6, v7, v8, v9 = BitVecs('v0 v1 v2 v3 v4 v5 v6 v7 v8 v9', 8)

# Ajout des contraintes avec l'opérateur de décalage à gauche
solver_bv.add(-85 * v8 + 58 * v7 + 97 * v6 + v5 + -45 * v4 + 84 * v3 + 95 * v0 - 20 * v1 + 12 * v2 == 12613)
solver_bv.add(30 * v9 + -70 * v8 + -122 * v6 + -81 * v5 + -66 * v4 + -115 * v3 + -41 * v2 + -86 * v1 - 15 * v0 - 30 * v7 == -54400)
# Utilisation de l'opérateur de décalage à gauche (<<)
solver_bv.add(-103 * v9 + 120 * v7 + 108 * v5 + 48 * v3 + -89 * v2 + 78 * v1 - 41 * v0 + 31 * v4 - (v6 << 6) - 120 * v8 == -10283)
solver_bv.add(71 * v6 + (v5 << 7) + 99 * v4 + -111 * v2 + 85 * v1 + 79 * v0 - 30 * v3 - 119 * v7 + 48 * v8 - 16 * v9 == 22855)
solver_bv.add(5 * v9 + 23 * v8 + 122 * v7 + -19 * v6 + 99 * v5 + -117 * v4 + -69 * v2 + 22 * v1 - 98 * v0 + 10 * v3 == -2944)
solver_bv.add(-54 * v9 + -23 * v7 + -82 * v2 + -85 * v0 + 124 * v1 - 11 * v3 - 8 * v4 - 60 * v5 + 95 * v6 + 100 * v8 == -2222)
solver_bv.add(-83 * v9 + -111 * v5 + -57 * v0 + 41 * v1 + 73 * v2 - 18 * v3 + 26 * v4 + 16 * v6 + 77 * v7 - 63 * v8 == -13258)
solver_bv.add(81 * v9 + -48 * v8 + 66 * v7 + -104 * v6 + -121 * v5 + 95 * v4 + 85 * v3 + 60 * v2 + -85 * v0 + 80 * v1 == -1559)
solver_bv.add(101 * v9 + -85 * v8 + 7 * v6 + 117 * v5 + -83 * v4 + -101 * v3 + 90 * v2 + -28 * v1 + 18 * v0 - v7 == 6308)
solver_bv.add(99 * v9 + -28 * v8 + 5 * v7 + 93 * v6 + -18 * v5 + -127 * v4 + 6 * v3 + -9 * v2 + -93 * v1 + 58 * v0 == -1697)

# Vérification et affichage du modèle
check_result = solver_bv.check()
print(f"Résultat de la vérification : {check_result}")
if check_result == sat:
   model_bv = solver_bv.model()
   print(f"Modèle trouvé : {model_bv}")
else:
   print("Aucune solution pour ce système.")
   

Interprétation des résultats et conversion de type

Lorsque Z3 retourne un modèle, les valeurs des variables sont des expressions Z3. Pour obtenir des représentations Python utilisables (comme des entiers), il peut être nécessaire de convertir ces expressions. Par exemple, pour obtenir des caractères ASCII à partir de valeurs numériques, on peut utiliser la fonction chr().

La résolution de ce type de problème peut impliquer l'identification de transformatiosn de données, comme des chiffrements ou des encodages, qui peuvent être représentés et résolus par Z3.

Dans certains cas, il peut être plus simple d'utiliser des variables Int pour des opérations arithmétiques standard et de passer à BitVec uniquement lorsque des opérations bitwise spécifiques sont nécessaires. L'exemple final montre comment Z3 peut être utilisé pour découvrir des clés ou des paramètres cachés dans un système d'équations, menant potentiellement à la découverte d'un flag ou d'une information secrète.