formal faults tolerance analysis of complex digital systems for safety and security applications

Dans cette thèse, nous proposons une nouvelle méthodologie pour caractériser la tolérance des conceptions de matériel contre les défauts externes.L'objectif principal est de construire un processus efficace pour découvrir les zones vulnérables d'un circuit numérique donné, lorsque des défauts externes se manifestent en lui.De la simulation qui code le comportement nominal du circuit, nous extrayons la machine à états finis de référence associée.Les propriétés temporelles linéaires sont intégrées dans l'environnement, le limitant aux spécifications du protocole attendu. Dans notre scénario, les assertions ont le rôle de détecteurs d'erreurs, lorsque des défauts sont injectés par la vérification du modèle.À partir de chaque état initial de la phase sélectionnée de la machine d'état de référence, nous lançons une preuve formelle pour découvrir si, dans ce scénario, le système peut être affecté de manière fatale par une défaillance du SEU. Cette erreur est injectée par le vérificateur de modèle au moment et au nœud les plus propices, pour violer au moins une propriété d'assertion.Ce processus est itéré pour cartographier la vulnérabilité de chaque cible de défaut au fil du temps, et les résultats sont comparés avec l'injection statistique simulée de défaut, pour confronter les gains de précision et de vitesse de la méthodologie.Nous appliquons la méthodologie sur des unités distinctes intégrées d'un SoC de base RISC-V pour les applications aérospatiales, développé par STMicroelectronics pour les tests radiatifs.En particulier, le SPI, le DMA, le CPU sont évalués avec notre flux de travail à des fins de sécurité.Les résultats préliminaires sont fournis sur un bloc AES à des fins de sécurité, fournissant ainsi une première idée utile d'application dans un tel environnement pour notre méthodologie.Les résultats sont conformes à ce que la simulation pure fournit, avec des accélérations importantes (de l'ordre de centaines) et une précision améliorée dans la détection des défauts.À partir de cette analyse, nous fournissons également par vérification de modèle une estimation du facteur de vulnérabilité architecturale.Le prochain problème que nous abordons est la génération automatique d'assertions LTL, pour traiter des blocs qui ne possèdent pas de spécification claire ou des IPs protégés. De plus, en exploitant les propriétés des signaux qui sont hiérarchiquement à l'intérieur du module adressé, nous pouvons estimer la capacité de masquage d'erreur du bloc par vérification de modèle.Une fois que nous avons réussi à caractériser l'effet de la panne sur la fonctionnalité du module unique, nous nous concentrons ensuite sur un modèle préliminaire de la façon dont une panne peut se propager d'un circuit à l'autre.Nous avons ensuite conçu une méthodologie (basée sur l'élimination itérative des hypothèses) pour prédire le pire scénario de la façon dont la défaillance peut affecter la fonctionnalité du module suivant.Par ce biais, nous pouvons interconnecter les deux digraphes distincts, contre-vérifiant les résultats par une injection de faute formelle étendue. Cette analyse permet de concevoir des systèmes de petite taille, à partir de modèles dysfonctionnels très complexes et de grande taille. En particulier, les modèles réduits et reconstitués peuvent être traités par des outils industriels pour étudier la sécurité des systèmes critiques.Enfin, nous présentons une étude préliminaire dans le domaine de la sécurité matérielle, abordant avec notre méthodologie un bloc AES.Cette étude donne un premier aperçu de la manière dont notre méthodologie peut être adaptable dans des contextes totalement différents, où l'objectif n'est pas d'étudier la tolérance du circuit aux perturbations externes, mais combien il peut être facile d'en extraire des informations utiles par injection de défauts.