Principes généraux de la sûreté de fonctionnement informatique

Télécharger le fichier pdf d’un mémoire de fin d’études

Fragilité des systèmes autonomes

L’autonomie soulève des problématiques de sûreté de fonctionnement dues à l’en-vironnement dynamique et inconnu dans lequel le système opère. L’autonomie induit aussi des logiciels de contrôle complexes qui sont difficiles à valider vu l’explosion du nombre d’états. Pour ces mêmes raisons, il est difficile d’évaluer la complétude des cas de tests effectués. De plus, l’utilisation des heuristiques afin d’accélérer la recherche de solution induit une complexité supplémentaire ; le système décisionnel devient impré-visible, ce qui rend le test et la vérification encore plus difficiles.
La couche décisionnelle est particulièrement vulnérable car elle produit et raffine les commandes ; ce qui pourrait être particulièrement dangereux.
En s’inspirant des travaux présentés dans [ALRL04] et [PTF02], Baudin et al. ont proposé, dans [BBGP07], de classifier les menaces que peuvent rencontrer les systèmes autonomes comme suit :
– Fautes de développement : introduites lors de la modélisation du système ou lors de l’implémentation.
– Fautes physiques se produisant pendant la phase opérationnelle et affectant les ressources physiques (capteurs, actionneurs, processeurs, sources d’énergie).
2. Les menaces exogènes, provenant de l’environnement physique, logique et humain du système autonome :
– Fautes externes comme les interférences, les attaques malveillantes et les fautes de coopération inter-systèmes (dont les fautes d’interaction avec l’humain).
– Mauvaise perception de l’environnement (manque d’observabilité, capteurs im-parfaits, etc.).
– Les aléas de l’environnement (événements incontrôlables, circonstances impré-vues, etc.).
L’environnement dynamique est pris en compte par les mécanismes décisionnels en utilisant des techniques de l’intelligence artificielle comme les systèmes experts, la planification à l’aide de solveurs, les réseaux Bayésiens, les réseaux de neurones artificiels, le raisonnement basé modèle etc. Ces mécanismes prennent des décisions selon leur perception de l’environnement, leur perception de leur état interne, et selon les moyens disponibles pour atteindre leurs objectifs. Ces processus décisionnels com-portent des connaissances spécifiques au domaine et des mécanismes d’inférence sur ces connaissances. Ces techniques conduisent à considérer plusieurs classes de fautes spécifiques [PTF02] :
1. Fautes propres au mécanisme décisionnel :
– une base de connaissances erronée, incomplète ou inconsistante,
– une inférence non-valide : la base de connaissances est correcte mais l’inférence produite peut être fausse à cause d’une procédure d’inférence utilisée d’une façon incorrecte,
– les imprévus : la base de connaissances peut être correcte, mais le raisonnement qui y est appliqué peut ne pas aboutir lorsqu’il est confronté à une situation inhabituelle, non prévue par le concepteur,
– spécificité des critères de décision : les critères de décision intégrés dans le système peuvent ne pas être universellement acceptables, c’est-à-dire, ils pour-raient avoir des effets secondaires indésirables dans certaines situations.
2. Fautes d’interaction entre le mécanisme décisionnel et l’humain :
– incompatibilité ontologique : la base de connaissances peut être correcte, mais une discordance se produit entre le sens du terme tel qu’il est utilisé par le système et le sens que l’utilisateur lui attribue,
– un optimisme déplacé dans les capacités du système : l’utilisateur place une trop grande confiance dans les décisions prises par le mécanisme décisionnel ; par exemple les résultats donnés par le mécanisme décisionnel sont très précis, conférant une illusion d’exactitude, mais faux,
– une incrédulité dans les capacités du système : l’utilisateur n’a pas confiance dans les décisions du système, par exemple si le processus de raisonnement du système lui paraît incompréhensible.

Les moyens de la sûreté de fonctionnement

Afin d’aboutir à un système aussi sûr que possible, on peut avoir recours à une combinaison de méthodes [ALRL04] qui sont :
– la prévention de fautes : comment empêcher l’occurrence ou l’introduction de fautes,
– la tolérance aux fautes : comment fournir un service à même de remplir la fonction du système en dépit des fautes,
– l’élimination des fautes : comment réduire la présence (nombre, sévérité) des fautes,
– la prévision des fautes : comment estimer la présence, les taux futurs, et les possibles conséquences des fautes.
Comme présenté dans la Figure 1.4, l’activation d’une faute engendre une erreur, qui, si rien n’est fait, peut conduire à une défaillance. La notion de tolérance aux fautes ne se limite pas aux mécanismes mis en place pour assurer une continuité de service (fiabilité) ; elle s’étend à tout mécanisme servant à endiguer la propagation d’erreurs dans le but d’éviter ou diminuer la gravité des défaillances (sécurité-innocuité).
La prévention de fautes et l’élimination des fautes peuvent être regroupées en une classe de méthodes d’évitement des fautes car elles visent la réalisation de systèmes exempts de fautes. La tolérance aux fautes et la prévision de fautes font partie de la classe de méthodes d’acceptation des fautes car elles prennent en compte le fait que tout système réel est sujet à des fautes, qu’il s’agisse de fautes matérielles, de fautes de développement résiduelles ou des fautes d’interaction, etc.

La sécurité des systèmes autonomes

Dans cette section, nous présentons des exemples des différentes méthodes de sûreté de fonctionnement dans le contexte des systèmes autonomes. Nous distinguons, d’une part, les méthodes qui s’appliquent hors-ligne, avant le déploiement du système et, d’autre part, les méthodes embarquées dans le système et qui s’appliquent en-ligne pendant son utilisation.

La sécurité des systèmes autonomes

Méthodes de sécurité hors-ligne

Nous focalisons sur les méthodes d’élimination de fautes, et en particulier la véri-fication basée modèle, la preuve de théorème et le test.

La vérification basée modèle

La vérification basée modèle (ou le model checking) est une méthode de vérifica-tion automatique qui explore l’ensemble des états du système et détermine si, étant donné un modèle M du système et une propriété φ, toutes les exécutions du modèle M satisfont φ. La vérification basée modèle est une méthode applicable principale-ment à des systèmes à états finis pour lesquelles toutes les exécutions possibles du système peuvent être énumérées exhaustivement [CGP99]. Si l’ensemble des proprié-tés vérifiées sont satisfaites, l’outil de vérification de modèle informe l’utilisateur que la vérification a réussi. Dans le cas contraire, un contre-exemple d’une exécution qui ne satisfait pas une des propriétés est donné. Le contre-exemple est utile pour remon-ter jusqu’aux causes du problème. Le nombre d’états, le temps et l’espace mémoire nécessaire pour les explorer croît rapidement avec la complexité des systèmes vérifiés, ce que l’on appelle l’explosion des états (ou l’explosion combinatoire). Le problème est particulièrement exacerbé avec les systèmes autonomes, dont la complexité est notoire. L’explosion combinatoire a fait l’objet de recherches actives au sein de la communauté scientifique. Le problème a été partiellement résolu dans les années ’80 à la suite de la découverte des OBDD (Ordered Binary Decision Diagrams), qui permettent d’obte-nir une représentation compactée des états du système. La vérification basée modèle traditionnelle combinée à l’utilisation des OBDD a donné naissance à la vérification basée modèle symbolique qui permet de vérifier des systèmes extrêmement grands en un temps et un espace mémoire acceptables [CGP99].
La vérification basée modèle a l’avantage de pouvoir être utilisée dès les premières phases de spécification du système, vu qu’elle ne nécessite qu’un modèle du système. Ceci a une contrepartie : les vérifications qui montrent que le système répond aux propriétés énoncées ne sont valables que pour le modèle du système utilisé, qui ne correspond pas forcément à l’implémentation réelle du système. Plus le modèle utilisé lors de la vérification est proche du système réel plus la vérification est pertinente.
Les propriétés vérifiées dans la vérification basée modèle peuvent être des :
– propriétés de sûreté : qui stipulent que quelque chose ne doit pas se produire (par exemple : pas de deadlock ),
– propriété de vivacité : qui stipule que quelque chose doit nécessairement se pro-duire (par exemple : chaque client doit avoir accès à une ressource partagée).

La preuve de théorème

La preuve de théorème (ou theorem proving) est une autre méthode qui permet d’effectuer des vérifications sur des modèles formels du système. Elle permet de dé-montrer que le modèle du système obéit à un ensemble de propriétés de la même façon que la preuve en mathématique démontre l’exactitude d’un théorème. Elle consiste à énoncer des propositions et à les démontrer dans un système de déduction de la logique mathématique, en particulier dans le calcul des prédicats. La preuve de théorèmes est une méthode difficile à manier car elle requiert une grande expertise technique et une connaissance pointue de la spécification du système [MP05]. Cette approche tend à être automatisée et assistée par ordinateur en utilisant les démonstrateurs de théo-rème. L’inconvénient majeur de cette approche est le fait que si un expert n’arrive pas à finir une preuve en utilisant un démonstrateur de preuves, l’outil ne donne aucune information quant à la faisabilité de la preuve ou quant à la nécessité d’informations supplémentaires pour compléter la preuve [LS09].
La preuve de théorème, par rapport à la vérification basée modèle, a l’avantage d’être indépendante de la taille de l’espace des états, et peut donc s’appliquer sur des systèmes complexes. L’explosion du nombre d’états n’étant plus un problème, la vérification peut être effectuée sur le modèle entier. La majorité des démonstrateurs de preuves sont très expressifs. Certaines propriétés, qui ne peuvent pas être spécifiées en utilisant les vérificateurs de modèles (par exemple : comparer les propriétés de deux états qui ne sont pas temporairement liés), peuvent être aisément spécifiées dans la majeure partie des langages des démonstrateurs de théorèmes [LS09].
Néanmoins, comme cela est le cas pour la vérification basée modèle, la validité de cette méthode repose sur l’hypothèse que le modèle du système et de son environne-ment reflète parfaitement le système et l’environnement réels. Or, ce n’est généralement pas le cas, surtout dans le contexte des systèmes autonomes complexes.

Le test

Le test est défini par la norme IEEE 829-2008 [IEE08] comme étant : « une activité dans laquelle un système ou un composant est exécuté sous des conditions spécifiques ; les résultats sont observés ou enregistrés ; et l’évaluation de certains aspects du système ou du composant est effectuée ». Un test est un ensemble de cas à tester. Un cas à tester est défini, selon la même norme, par : des données d’entrées, des conditions d’exécution et les résultats attendus pour un objectif donné (l’objectif peut être, par exemple, que le programme respecte une propriété spécifique). Différents types de test permettent de détecter différents types d’erreurs. Le test peut être classé selon le niveau du cycle de développement du logiciel dans lequel il est effectué : test composant (unitaire), test d’intégration, test système (ou test fonctionnel) et test d’acceptation. Il peut être classé aussi selon sa caractéristique : test de performance (validation que les performances spécifiées du système sont respectées), test fonctionnel (vérification que les fonctionnalités répondent aux attentes), test de vulnérabilité (vérification de la sécurité du logiciel) et test de robustesse (validation de l’aptitude du système à délivrer un service correct dans la durée, ou bien en présence d’entrées invalides ou de conditions environnementales stressantes) [Chu11].

Méthodes de sécurité en-ligne

Etant données les limitations intrinsèques des méthodes de vérification basées mo-dèles, de preuve de théorème et de test, il nous semble indispensable, surtout pour les systèmes critiques, de les compléter par des méthodes de vérification en ligne pour assurer la sécurité.
Nous classons dans cette catégorie de techniques, toute approche visant à détec-ter un comportement incorrect d’un système et éventuellement à réagir avant qu’un événement indésirable ne survienne. Nous pouvons citer, par exemple, toutes les mé-thodes classiques de détection d’erreurs utilisées en tolérance aux fautes (voir Sec-tion 2.1.1.2 de [LAB+96]), ainsi que les techniques de diagnostic utilisées de façon pro-active pour révéler l’existence de fautes, et éventuellement les isoler (par exemple, l’approche FDIR) 3 [PRDS07].
Cependant, nous allons nous focaliser sur deux techniques de vérification en-ligne plus spécifiquement ciblées sur des comportements incorrects dus à des fautes rési-duelles de développement ou sur des comportements dangereux vis-à-vis de la sécurité.

La vérification à l’exécution

Au début des année 2000, le terme “vérification à l’exécution” (ou runtime verifica-tion) a été introduit dans le contexte de recherches à la frontière entre la vérification formelle (basée modèle ou par preuve de théorèmes) et le test 4. Cette communauté s’est intéressée à la vérification qu’une exécution respecte des propriétés spécifiées formelle-ment, issues ou non de la spécification du système. Il s’agit en fait d’une généralisation de la notion d’assertions exécutables [Sai77, RBQ96] à des propriétés le plus souvent dynamiques, relatives par exemple, aux événements dans une trace d’exécution.
L’IEEE définit la vérification à l’exécution comme « une discipline de l’informatique qui pour objectif l’étude, le développement et l’application de techniques de vérification qui permettent de vérifier si l’exécution du système répond ou viole des propriétés pré-définies » [IEE05]. De nombreux travaux ont étudié la pertinence d’avoir recours à cette technique dans le contexte des systèmes autonomes critiques [LS09, GP10, PNW11].
Les principales différences entre la vérification basée modèle et la vérification en ligne sont :
– la dimension de l’espace d’états à vérifier : la vérification basée modèle vérifie si 3. FDIR (Fault diagnosis, isolation and reconfiguration) est un terme utilisé pour désigner toute approche de tolérance aux fautes distinguant les trois étapes : détermination des causes des erreurs (les fautes), isolation de celles-ci, puis reconfiguration du système de telle façon que les composants non-défaillants puissent délivrer un service acceptable (même s’il est dégradé) toutes les exécutions possibles d’un système satisfont une propriété donnée alors que la vérification à l’exécution vérifie une trace d’exécution finie,
– la représentation du système à vérifier : la vérification basée modèle s’appuie, comme son nom l’indique, sur un modèle du système alors que la vérification à l’exécution vérifie l’exécution du système réel.

Les dispositifs de surveillance pour la sécurité

Lorsque les propriétés à vérifier ciblent plus spécifiquement la sécurité, au sens de l’évitement de défaillances catastrophiques, la vérification en ligne s’effectue au moyen d’un dispositif de sécurité.
Les dispositifs de surveillance apparaissent dans la littérature sous différentes ap-pellations : “safety manager” [PS00], “autonomous safety system” [RRAA04], “che-cker” [IP02], “guardian agent” [Fox01], “safety bag” [Kle91], ou bien “moniteur de sécu-rité” [IEC10]. Les auteurs de ces travaux présentent différents dispositifs de surveillance que nous pouvons distinguer selon deux critères : indépendance physique ou matérielle du dispositif de surveillance par rapport au système surveillé et l’indépendance logi-cielle du dispositif de surveillance par rapport au système surveillé.
1. Indépendance physique : la norme IEC 61508 [IEC10] distingue « le moniteur et le système surveillé présents sur la même plate-forme avec une certaine ga-rantie d’indépendance entre les deux » et « le moniteur et le système surveillé sur des plates-formes indépendantes ». Dans ce dernier cas, le dispositif de sur-veillance est appelé moniteur diversifié 5 dont le but est « de garantir une protec-tion contre les fautes résiduelles de spécification et de mise en œuvre du logiciel qui pourraient porter atteinte à sécurité du système ». Schroeder [Sch95] parle de moniteur intrusif lorsque le dispositif de surveillance et le système surveillé partagent des ressources communes (CPU, dispositifs d’entrée/sortie, chaînes de communication etc.). A l’opposé, le dispositif de surveillance est appelé moniteur non-intrusif lorsqu’il utilise un équipement qui lui est dédié. L’auteur définit un moniteur de sécurité comme étant : « un observateur externe voué à être per-manent et qui surveille une application opérationnelle ».
2. Indépendance logicielle : Goodloe et Pike [GP10] définissent un moniteur de sécurité ainsi : « le moniteur observe le comportement d’un système et détecte s’il est cohérent avec une spécification donnée ». Ils parlent de moniteur “in-line” lorsque le moniteur est inséré dans le code (annotations, assertions etc.) et de moniteur “out-line” lorsque le moniteur est exécuté dans un processus indépendant du système surveillé. Ils abordent aussi la notion de recouvrement, qui n’est pas présente dans les précédentes définitions : « les moniteurs (in-line et out-line) vérifient le respect de la spécification lors de l’exécution et peuvent remettre le système dans un état acceptable lorsque ce dernier se met à dévier de sa spécification ».
5. Dans la première version de l’IEC 61508 (1998), un tel moniteur était appelé safety bag, terme utilisé dans de précédents travaux sur les moniteurs diversifiés dans le contexte du contrôle ferro-viaire [Kle91]

La sécurité des systèmes autonomes

Nous nous intéressons particulièrement aux dispositifs de surveillance indépendants physiquement car ils permettent de se prémunir des fautes résiduelles de spécification et de développement qui ont résisté aux méthodes de vérification hors-ligne. De plus, ils permettent de se protéger des défaillances de mode commun (une défaillance du système cible n’aura pas d’impact sur le dispositif de surveillance) et de la propaga-tion des erreurs (une donnée erronée utilisée par le système cible n’affectera pas le traitement effectué par le dispositif de surveillance).
On peut distinguer deux sortes de dispositifs de surveillance selon le type d’action qu’ils peuvent enclencher vis-à-vis du système surveillé :
1. Action de blocage : le dispositif de surveillance observe que le système est dans état sûr mais que l’exécution de telle ou telle tâche le mettrait dans un état catas-trophique, il enclenche une action qui consiste à bloquer cette (ou ces) tâche(s). Un tel dispositif fonctionne comme un interverrouillage.
Leveson [Lev91] définit l’interverrouillage comme un mécanisme qui permet de s’assurer qu’une séquence d’opérations se produit dans le bon ordre. L’auteur a donné des exemples d’interverrouillages qui permettent de s’assurer qu’un évé-nement A ne se produira pas :
– par inadvertance : par exemple obliger l’occurrence d’un événement B avant que l’événement A ne puisse se produire,
– tant qu’une condition C est vérifiée : par exemple une porte d’accès est placée en amont d’un équipement à haute tension de telle sorte que, tant que la porte est ouverte, l’équipement est mis hors tension,
– avant un événement D : par exemple la cuve ne se remplit que lorsque la sou-pape d’aération est ouverte.
Un interverrouillage peut faire partie intégrale du système fonctionnel, en ayant par exemple recours à des techniques de synthèse de contrôleurs [RW89, ACMR03, PI04a, BDSG+10], ou bien il peut être externe au système en utilisant des moyens électriques, électroniques ou mécaniques. Les interverrouillages externes au sys-tème permettent une protection de bout en bout, ce qui permet d’assurer la sécurité du système contre des fautes internes au système. Néanmoins, implé-menter un tel mécanisme peut être coûteux, notamment lorsque cela nécessite une modification du système physique.
2. Action de mise en sécurité : le dispositif de surveillance observe que le système est dans un état dangereux mais non catastrophique, il doit alors enclencher une action qui consiste à remettre le système dans un état sûr. Nous réservons le terme moniteur de sécurité à cette sorte de dispositif de surveillance.
Nous concrétisons cette distinction par les définitions suivantes :
Définition 1. Un interverrouillage de sécurité est un mécanisme qui a pour objectif d’empêcher que le système atteigne un état catastrophique en inhibant les événements qui peuvent mener à un tel état à partir de l’état actuel du système.
Définition 2. Un moniteur de sécurité est un mécanisme qui a pour objectif d’empê-cher que le système atteigne un état catastrophique, en détectant les états non-sûrs et en enclenchant les actions appropriées afin de remettre le système surveillé dans un état sûr.

Table des matières

1 Dispositifs de surveillance des systèmes autonomes 
1.1 L’autonomie
1.1.1 Définitions
1.1.2 Illustrations
1.1.3 Fragilité des systèmes autonomes
1.2 Principes généraux de la sûreté de fonctionnement informatique
1.2.1 Les attributs
1.2.2 Les entraves
1.2.3 Les moyens de la sûreté de fonctionnement
1.3 La sécurité des systèmes autonomes
1.3.1 Méthodes de sécurité hors-ligne
1.3.1.1 La vérification basée modèle
1.3.1.2 La preuve de théorème
1.3.1.3 Le test
1.3.2 Méthodes de sécurité en-ligne
1.3.2.1 La vérification à l’exécution
1.3.2.2 Les dispositifs de surveillance pour la sécurité
1.4 Exemples de dispositifs de sécurité et analyse
1.4.1 Ranger
1.4.2 Elektra
1.4.3 R2C (Request & Resource Checker)
1.4.4 MARAE
1.4.5 DLR Co-Worker
1.4.6 Discussion
1.5 Conclusion
2 Identification de contraintes de sécurité 
2.1 La gestion du risque
2.1.1 Le risque
2.1.2 Les étapes de la gestion du risque
2.2 Techniques d’analyse de risque
2.2.1 Analyse par Arbre de Fautes (AdF)
2.2.2 Analyse des Modes de Défaillance, de leurs Effets et leur Criticité (AMDEC)
2.2.3 Étude de danger et d’opérabilité (HazOp)
2.2.4 Discussion
2.3 L’analyse de risque HazOp/UML
2.4 Expression de contraintes de sécurité à partir de l’analyse HazOp/UML
2.4.1 Expression des contraintes de sécurité en langage naturel
2.4.2 Expression des contraintes de sécurité en langage formel
2.5 Conclusion
3 Spécification des règles de sécurité 
3.1 Concepts de base
3.2 Invariants de sécurité et conditions de déclenchement de sécurité
3.3 Identification des conditions de déclenchement de sécurité
3.3.1 Identification des états d’alerte
3.3.2 Impossibilité de définir les états d’alerte
3.3.3 Calcul des marges de sécurité pour les variables continues
3.4 Actions de sécurité et dimensionnement des marges
3.5 Identification des actions de sécurité potentiellement concomitantes
3.6 Récapitulatif de la méthode proposée
3.7 Conclusion
4 Validation de l’approche 
4.1 Le cas d’étude MIRAS
4.1.1 Présentation
4.1.2 Structure du robot
4.1.3 Environnement d’utilisation
4.1.4 Description des utilisateurs
4.1.5 Scénario nominal de l’utilisation
4.1.6 Cas d’utilisation et diagrammes de séquences
4.2 HazOp/UML appliquée à MIRAS
4.3 Elicitation des règles de sécurité
4.3.1 Génération des contraintes de sécurité
4.3.2 Spécification des règles de sécurité
4.3.3 Identification des actions de sécurité concomitantes
4.4 Conclusion
5 Conclusion et Perspectives 
5.1 Démarche globale
5.2 Leçons apprises
5.3 Perspectives
Bibliographie 

Télécharger le rapport complet