Thesis defence of Damiano Zuccalà (CDSI team): Formal faults tolerance analysis of complex digital systems for safety and security applications

Damiano ZUCCALÀ - CDSI team

Thesis director
Katell MORIN-ALLORY - Thesis director - Associate professor - TIMA Lab. - Grenoble INP

Rapporteurs
Alberto BOSIO - Rapporteur - Full professor - LIRMM - Ecole Centrale de Lyon
Graziano PRAVADELLI - Rapporteur - Full professor - Université de Vérone

Composition of the jury
Katell MORIN-ALLORY - Thesis director - Associate professor - TIMA Lab. - Grenoble INP
Alberto BOSIO - Rapporteur - Full professor - LIRMM - Ecole Centrale de Lyon
Graziano PRAVADELLI - Rapporteur - Full professor - Université de Vérone
Laure GONNORD - Examinator - Full professor - Grenoble INP
Kevin MARTIN - Examinator - Full professor - Université de Bretagne-Sud
Jean-Marc DAVEAU - Guest - Engineer - STMicroelectronics

Title: Formal faults tolerance analysis of complex digital systems for safety and security applications
Keywords: Mathematics, Computer Science, Formal Methods, Fault Injection, Hardware Safety, Hardware Security
Abstract: In this thesis, we propose a novel methodology to characterize the tolerance of hardware designs against external faults. The main objective is to construct an efficient process to discover the vulnerable areas of a given digital circuit, when external faults manifest in it. From the simulation that encodes the nominal behavior of the circuit, we extract the associated reference finite state machine. Linear temporal properties are integrated into the environment, restraining it to the expected protocol specification. In our scenario, assertions have the role of error detectors, when faults are injected by model checking. From each initial state of the selected phase of the reference state machine, we launch a formal proof to discover if from that scenario the system can be fatally affected from a SEU fault. This error is injected by the model checker at the most propitious time and node, to violate at least one assertion property. This process is iterated to map the vulnerability of each fault target over time, and results are compared with simulated statistical fault injection, to confront the accuracy and speed gains of the methodology. We apply the methodology on distinct units integrated of a RISC-V bases SoC for aerospace applications, developed by STMicroelectronics for radiative tests. In particular, the SPI, DMA, CPU are assessed with our workflow for safety purposes. Preliminary results are provided on an AES block for security purposes, providing a first useful insight of application in such environment for our methodology. Results are in accordance with what the pure simulation provides, with significant speedups (in the magnitude of hundreds) and improved accuracy in fault detection. Starting from this analysis, we also provide by model checking an estimation of the Architectural Vulnerability Factor. The next problem we address is the automatic generation of LTL assertions, to treat blocks that lack clear specification or protected IPs. Moreover, by mining properties on signals that are hierarchically inside the addressed module, we can estimate the fault masking capacity of the block by model checking. Once we have successfully characterized the fault effect on the single module's functionality, we then focus on a preliminary model of how a fault may propagate from one circuit to the next one. This study provides fist insights on the probability with which a system of SoC-like complexity may be affected by an external fault affecting its functionality. This analysis is performed by treating the different hardware units in their FSM representation. Once we have generated the digraphs, we must reduce their size along with computing the fault propagation probability to reach a failure state. We then conceived a methodology (based on iterative assumption removal) to predict the worst scenario of how the fault can affect the functionality of the next module. By this, we can interconnect the two distinct digraphs, counter-verifying the results by extensive formal fault injection. This analysis allows to small-sized systems, starting from very complex and large dysfunctional models. In particular, the reduced and re-composed models can be further treated by industrial tools to study the safety of critical systems. Finally, we present a preliminary study in the hardware security domain, addressing with our methodology an AES block. This example is also used to verify that after integrating the countermeasures on the flip-flops, we can formally prove that the module is fault immune. This study provides a first glance on how our methodology may be adaptable in totally different contexts, where the objective is not to study how much the circuit is tolerant against external perturbations, but how easy can be to extract from it useful information through fault injection.

Titre : Analyse formelle de la tolérance aux fautes des systèmes numériques complexes pour les applications de sécurité et de sûreté
Mots-clés : Mathématique, Informatique, Méthode Formelle, Injection de fautes, Sécurité matérielle
Résumé : 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.