Qu'est-ce que la vérification de modèle symbolique exactement?

8

Je sais que la vérification de modèle symbolique est une traversée de l'espace d'états basée sur des représentations d'ensembles d'états et de relations de transition comme des formules comme dans CTL utilisant des modèles comme Kripke Model. Je connais la théorie. Mais j'ai du mal à comprendre l'application réelle. Où est-il utilisé exactement? Que fait-il exactement et comment fonctionne-t-il?

Quelqu'un peut-il expliquer avec un exemple réel et relier la théorie à la pratique?

Xpleria
la source
1
Cela me semble large. Le "qu'est-ce que ça fait?" une partie peut avoir une portée raisonnable (ou non), mais "où est-elle utilisée?" est a) une autre question entièrement et b) probablement trop large.
Raphael
Mais un exemple peut être pris et expliqué sur cette base. Ce n'est pas trop large.
Xpleria
2
Pourquoi n'êtes-vous pas satisfait de la description de la vérification de modèle symbolique dans un manuel standard, par exemple, "Principes de vérification de modèle" par Christel Baier et Joost-Pieter Katoen? De quelles parties êtes-vous confus?
hengxin
Ils parlent de «comment cela est censé être fait» mais pas «comment exactement cela est fait». J'essaie de relier la théorie et la mise en œuvre pratique. Je suis encore nouveau dans ce domaine et j'ai besoin d'un exemple.
Xpleria
1
Vous êtes peut-être alors sur le mauvais site. Informatique scientifique est sur les concepts ( « comment il doit être fait »), vous devrez demander des praticiens de la « comment faire » partie.
Raphael

Réponses:

4

La vérification de modèle symbolique est une vérification de modèle qui fonctionne sur les états symboliques. Autrement dit, ils codent les états en représentations symboliques, généralement des diagrammes de décision binaires ordonnés (OBDD).

La question est de savoir ce qu'ils font et comment ils fonctionnent.

Vous avez d'abord votre code source pour une application. Vous transformez ensuite votre code source en un graphique de transition d'état comme une structure Kripke. Les états sont remplis de propositions atomiques qui décrivent ce qui est vrai dans cet état particulier. Dans la vérification de modèle symbolique, les propositions atomiques sont codées en tant qu'OBDD pour économiser de l'espace et améliorer les performances.

Le vérificateur de modèle démarre alors à un état initial et explore les états, à la recherche d'erreurs dans le graphique de transition d'état. S'il trouve une erreur, il génère souvent un scénario de test démontrant l'erreur. Il utilise les OBDD symboliques pour naviguer de manière quelque peu optimale dans l'espace d'état. J'aimerais pouvoir expliquer plus là-bas mais toujours en train d'apprendre.

Mais c'est fondamentalement ça. Vous avez un programme converti en modèle formel (graphique de transition d'état), puis vous utilisez des optimisations symboliques pour parcourir l'espace d'état pour rechercher des erreurs (en le comparant à une spécification LTL / CTL). Et si une erreur est trouvée, le vérificateur de modèle vous donne quelques informations pour aider à documenter et à résoudre le problème.

Lance Pollard
la source
5

La vérification des modèles symboliques peut être très utile pour vérifier l'exactitude des communications et des protocoles de sécurité. Par exemple:

  • Un modèle symbolique d'une implémentation OAUTH2 pourrait aider à vérifier les conséquences inattendues lorsqu'un adversaire obtient des jetons d'authentification secrets ou des données circonstancielles connexes qui pourraient les aider à contrevenir au processus.
  • Un modèle symbolique d'un protocole cryptographique, tel qu'une prise de contact TLS, pourrait aider à vérifier que la conception cryptographique n'a pas de conséquences inattendues.

Cela fonctionne en écrivant une description symbolique de toutes les fonctions primitives et algorithmes de protocole, puis en ayant un vérificateur de modèle symbolique, tel que ProVerif , traverse l'espace d'état et tente de détecter les combinaisons d'états qui produisent des résultats défavorables. Dans le cas de ProVerif, les modèles symboliques sont décrits en utilisant le calcul Pi appliqué comme langage de modélisation. Cela permet la description de protocoles dans une syntaxe fonctionnelle de type ML.

kaepora
la source