Systèmes à nombre d’états infini

Systèmes à nombre d’états infini

La vérification de systèmes intéressants–tels que les protocoles de sécurité ou encore les programmes Java– nécessite de considérer un nombre d’états infini. Par exemple, si le système vérifié travaille sur des entiers, il est plus générique de considérer un en semble infini d’entiers. En effet, chaque ordinateur possédant une borne sur les entiers, on pourrait alors imaginer ne considérer qu’un ensemble fini d’entiers pour le problème de vérification.

Cependant, cette borne est différente selon le matériel utilisé et l’usage d’un ensemble infini d’entiers permet d’avoir une méthode de vérification générique ne dépendant pas de la machine sur laquelle le système est exécuté. Contrairement au cas d’un espace d’états fini, le problème de vérification dans le cas infini est bien souvent indécidable.

Prenons par exemple un échange de messages entre un utilisateur, que l’on appellera Alice, et un serveur mail ou un site marchand que l’on appellera Bob. Ces messages contiennent parfois des données sensibles telles qu’un mot de passe ou un numéro de carte de bleue comme nous le voyons en figure 1.4 : l’échange doit donc être sécurisé.

Dans ce but, les messages sont chiffrés par des clés, et les clés de déchiffrement sont connues uniquement d’Alice et de Bob afin d’assurer la confidentialité des données. Dans de tels échanges de messages, il est intéressant de vérifier qu’il est impossible pour une tierce personne de récupérer une information confidentielle ou une clé de déchiffrement.

Une tierce personne (un intrus malveillant) peut tenter de récupérer des données secrètes en envoyant, sous une fausse identité, des messages à Alice ou à Bob (voir figure 1.4). Si les réponses reçues par l’intrus lui permettent d’accéder à des informations confidentielles (comme c’est le cas dans le bug heartbleed), alors le protocole possède une faille qu’il est souhaitable de trouver en vérifiant le système.

Pour vérifier que le protocole ne possède aucune faille, i.e. qu’aucun mauvais com portement tel que la récupération de données secrètes par l’intrus n’est accessible, il faudrait pouvoir calculer tous les messages possibles que l’intrus peut fabriquer. Mais l’intrus, même s’il possède peu d’informations au début, peut éventuellement enrichir sa connaissance grâce aux réponses d’Alice ou de Bob, si elles contiennent des données intéressantes que l’intrus peut utiliser (voir figure 1.4).

Ainsi, il est possible pour l’intrus de construire une infinité de messages différents, et pour vérifier qu’aucun de ces mes sages n’est dangereux, il faudrait alors être capable de tous les calculer, ce qui est bien souvent un problème indécidable. La vérification des protocoles de sécurité ainsi que de la plupart des systèmes à états infinis pose donc deux problèmes difficiles : (1) Comment manipuler et représenter des ensembles infinis? (2) Comment calculer des ensembles infinis en un temps fini? 

Message chiffr´ e Donn´ ees confidentielles Alice (mot de passe, num´ ero de carte bleue, …) R´ eponse d’Alice Message de l’intrus Message de l’intrus Intrus Connaissance de l’intrus Bob R´ eponse de Bob FIGURE 1.4 — Un intrus malveillant peut construire une infinité de messages différents pour tenter de récupérer des données confidentielles.

Une représentation régulière pour les ensembles infinis Pour résoudre le problème (1), récurrent en vérification, il n’existe que des solu tions partielles. Une de ces solutions consiste à représenter chaque état du système par une séquence possiblement infinie de symboles : cette séquence est alors appelée un mot.

L’ensemble des symboles permettant de former un mot est défini au préalable, et consti tue ce que l’on appelle l’alphabet. Soit = 01 un alphabet contenant le symbole 0 et le symbole 1 : on peut alors construire les mots 10, 111, 1001010, etc., soit l’ensemble infini des nombres binaires. Dans ce contexte, les ensembles infinis d’états, qui sont alors des ensembles infinis de mots, sont représentés par une structure finie et symbolique.

Cette structure géné rique est appelée automate fini. Cependant, le problème (1) étant indécidable, les auto mates finis ne permettent de représenter qu’une classe limitée d’ensembles infinis : les ensembles réguliers. Malgré cette contrainte, cette représentation en automate est gé néralement suffisante pour représenter les ensembles d’états accessibles de nombreux systèmes.

La figure 1.5 représente un automate fini construit sur l’alphabet = 01 . Cet automate reconnait l’ensemble infini des nombres pairs en codage binaire. En effet, un nombre binaire est pair s’il termine par un 0. Or cet automate permet de reconnaitre les mots comprenant :– N’importe quelle séquence de symboles 0 ou 1. Ceci est représenté par la boucle 0, 1 : il peut y avoir de zéro jusqu’à une infinité de 0 ou de 1.