ILLUSTRATION DU PROBLÈME ET
CONTRIBUTION

Cas d’utilisations

Considérons les trois exemples de diagnostic sur deux architectures différentes, illustrés sur la figure 2.2. Dans le premier cas (1), un ingénieur vérifie le comportement d’un système conçu par un tiers, illustré sur la figure 2.3. L’ingénieur a une pratique de la vérification par model checking, mais peu de connaissances quant au domaine du système. Dans le second cas, un concepteur reprend ce même système, et y ajoute un mécanisme d’exclusion mutuelle, comme illustré sur la figure 2.4, puis le vérifie. Il bénéficie d’une expérience dans le domaine de l’application qu’il conçoit. Dans le dernier cas, un architecte sécurise le système, comme illustré sur la figure 2.5, puis le vérifie. Il bénéficie d’une base de connaissances externe. Rappelons que la question générale qui nous concerne est de faciliter la phase de diagnostic qui survient lorsqu’une vérification a échouée. Premier cas : Vérification du modèle construit par un tiers Dans le premier cas, un ingénieur que nous appellerons Luka, doit vérifier un modèle conçu par un tiers. Luka n’est pas expert dans le domaine des SCADA, mais il a une bonne connaissance en model checking. Il est familier avec les processus communicants décrits dans des langages formels, familier avec les propriétés formelles décrites en logique temporelle, et familier avec la technique d’exploration des LTS. Le modèle qu’il doit vérifier est un modèle formel exprimé en langage Fiacre généré à partir d’un modèle UML (figure 2.3). En parallèle, il lui a été fourni un ensemble de propriétés à vérifier, décrites en LTL. Il dispose également d’un ensemble de scenarii d’utilisations du modèle formalisé sous la forme de contextes CDL. Luka suit l’approche décrite par C.Baier [BK08]. À l’aide d’un model checker (OBP), il génère le LTS correspondant au modèle, et l’explore. Dans un des scenarii, le client envoie plusieurs messages au P LC1 et attend un message d’acquittement (ACK) de la part du système. L’exploration montre que ce scénario ne fonctionne pas car une propriété vérifiant ce comportement est violée (CLT1SendAck), déclenchant ainsi une phase de diagnostic. Cette propriété énonce que si un Client envoie une donnée au P LC1, alors celui-ci recevra fatalement un ACK venant de P LC1. OBP génère un contre-exemple exposant à Luka les configurations amenant à cette conclusion. Grâce à sa connaissance en model checking, Luka peut rejouer le contre-exemple pour en comprendre la cause. Mais la trace produite par le model checker est trop détaillée, constituant un frein à l’analyse manuelle. Il existe un ensemble de techniques d’aide au diagnostic, comme comparer des traces positives et négatives afin d’isoler des parties suspectes de la trace, ou bien réduire la trace par slicing. Luka opte pour l’utilisation d’un outil de visualisation de trace sous forme d’un diagramme de séquence. Le diagramme de séquence permet d’afficher uniquement les interactions entre les différents processus. Cet outil aide Luka à identifier qu’un message n’est pas transmis entre deux processus, P LC1 et Network. Le message ne parvient pas au Network car celui-ci n’est pas transmis par le bon canal. Luka propose un diagnostic, le processus P LC1 est mal connecté. Une fois la correction apportée au modèle, Luka s’assure que celui-ci est correct en effectuant une autre vérification. Mais la propriété est une nouvelle fois violée. À traver le diagramme de séquence, Luka s’aperçoit pourtant que sa correction a fonctionné, le message est correctement transmis. Ici, le diagramme de séquence ne permet pas d’aller plus loin dans l’analyse, il faut changer de stratégie. Luka énonce de nouvelles propriétés lui permettant d’observer des comportements particuliers du modèle, en y ajoutant au besoin quelques annotations. Par exemple, une propriété énonce que quand un channel est lu il doit être dépilé. Ces propriétés de contrôle sont inhérentes aux processus communicants. Le model checker indique maintenant qu’une propriété est violée. Un channel est lu sans être dépilé. Conclusion, le channel doit être dépilé après avoir été lu. Le modèle est une nouvelle fois corrigé, mais la propriété est toujours violée. Bien que Luka ait connaissance des spécifications du problème et de connaissances toujours applicables en matière de model checking, celles-ci sont parfois insuffisantes pour effectuer le diagnostic, le rendant long et fastidieux. De nouvelles connaissances sont alors nécessaires pour comprendre la solution.

Second cas : Conception d’un mécanisme d’exclusion mutuelle

Ciprian est le concepteur du modèle, et il le maîtrise. Il souhaite ajouter une nouvelle fonctionnalité. P LC1 et P LC2 partagent tous deux une ressource, lue ou écrite lorsque P LC1 ou P LC2 sont dans leur état Access, soit PLC1@Access ou PLC2@Access 1 . Le modèle doit vérifier l’exigence suivante : il n’est pas possible que P LC1 et P LC2 soient en même temps dans leur état Access, exigence traduite sous la forme d’une propriété PSingleAccess. Pour répondre à ce nouveau problème il opte pour un mécanisme de drapeaux. Le principe est le suivant, P LC1 et P LC2 possèdent tous deux un drapeau. P LC1 ou P LC2 lève son drapeau, pour informer qu’il accède à la ressource. Avant d’accéder à cette ressource, un processus doit vérifier que le drapeau de l’autre processus n’est pas levé, sinon, il doit attendre qu’il soit baissé. Lorsqu’un processus a fini d’utiliser la ressource, il baisse son drapeau et libère la ressource.Après vérification, il s’avère que la propriété PSingleAccess est violée, signalant l’existence d’un contre exemple où P LC1 et P LC2 utilisent en même temps la ressource. Comme précédemment, Ciprian commence par vérifier des propriétés liées à la modélisation des processus communicants (comme dans le cas précédent). Au bout d’un certain temps, sans succès, il en conclut que le problème vient de la manière dont il a conçu le mécanisme. Pour identifier parmi les milliers de configurations de la trace le comportement du mécanisme implémenté, il doit exprimer des propriétés liées à ce mécanisme. Ciprian s’aperçoit alors que le drapeau est levé après le test d’accès à la ressource. Il doit donc corriger le modèle et repartir sur un cycle de vérification. Si Ciprian connaît la spécification du problème et est capable de le résoudre, il n’a pas de connaissances de solutions existantes. Il va devoir concevoir lui-même un mécanisme d’exclusion mutuelle et suivra un cycle itératif de conception-vérification, pouvant être bloqué s’il ne sait pas le résoudre entièrement. Celui-ci pourrait être évité par la réutilisation de solutions du domaine.

Troisième cas : Réutilisation de connaissances

Après avoir assuré un mécanisme d’exclusion mutuelle pour les deux Plc envers la ressource, un autre ingénieur, Philippe, doit sécuriser l’architecture face à des cyberattaques. Pour ce faire, il prévoit d’implémenter un mécanisme de Single Access Point (SAP), réduisant l’accès à la ressource en un point unique. Philippe choisit de réutiliser une solution existante, mettant en œuvre le SAP, qui est accompagnée de propriétés et d’une architecture abstraite. Pour l’utiliser, il doit réaliser un ensemble de modifications dans son modèle, et pour le vérifier, il doit faire correspondre les propriétés exprimées par le patron avec les éléments de son modèle. Après vérification, il s’avère qu’une des propriétés est violée. Grâce au SAP, Philippe bénéficie d’un ensemble de propriétés qui peuvent l’aider à localiser le problème. La connaissance du domaine, c’est-à-dire la connaissance de solutions, permet alors de le guider dans le diagnostic. Finalement, il s’avère que la solution construite n’est pas conforme. Bien que des propriétés aient pu aider au diagnostic, la solution conçue de manière ad hoc, reste difficile à diagnostiquer. Philippe doit donc comprendre comment il a mis en œuvre la solution pour comprendre l’origine du problème. Une nouvelle exigence, traduite sous la forme d’une propriété formelle, exige que si le client a les droits suffisants, il doit être autorisé à accéder à la ressource. Le mécanisme de SAP n’est plus suffisant pour protéger l’architecture SCADA. Un mécanisme d’autorisation (AUTH) doit être ajouté. Ainsi, seuls les clients autorisés pourront accéder à la ressource. Cette fois-ci, il existe un patron d’autorisation incluant une solution adaptable. Philippe applique ce patron à son modèle. La propriété est tout de même violée, préfigurant deux problèmes. Soit l’adaptation du patron a été mal réalisée, c’est-à-dire par exemple que le patron n’est pas adapté au modèle de la bonne manière, soit c’est un mauvais choix de patron. Une fois corrigée, la solution est capturée sous la forme d’un composant réutilisable. Ici c’est la méthode employée qui est au cœur du problème. La solution choisie amène avec elle un lot de propriétés liées aux composants intégrés. Le modèle est ainsi constitué d’un ensemble de composants, chacun associé à un ensemble de propriétés axiomatiques dont certaines permettent de contrôler l’intégration. Cette couverture permet d’isoler plus précisément le composant qui porte le problème, réduisant ainsi l’effort de diagnostic.