Formal verification approach to security requirements for communicating embedded systems

La maîtrise de la sécurité dans les systèmes embarqués communicants se heurte àun certain nombre de difficultés, dues à leur nature qui est le plus souvent complexe. Adopter une approche basée sur les modèles pour la vérification des exigences du système dès la phase de conception peut apporter un gain important en matière de coût et de temps.Dans ce travail de thèse, nous proposons une approche centrée sur les modèlespour la vérification formelle de la satisfaisabilité d’un scénario d’attaque pour un système embarqué communicant. L’approche proposée est composée de trois étapes : i) la modélisation conceptuelle du système, ii) la modélisation conceptuelle de l’attaque, iii) la transformation des modèles conceptuels en modèles formels en vue de vérification. Le langage SysML a été choisi pour la modélisation structurelle et comportementale du système en raison de son adaptabilité et son extensibilité par profilage. Afin de personnaliser la modélisation des flux de données, nous avons stéréotypé les ports et les connecteurs suivant les technologies et leurs propriétés. Cettepersonnalisation nous a permis de suivre les traces de la circulation des flux entre les différents sous-systèmes communicants. Une ébauche de la documentation du profil de connectivité a été proposée. Pour la structuration de l’attaque, un profil de l’arbre d’attaque étendu nommé ExtAttTree a été proposé. À la différence des arbres d’attaque classiques, ce profil parvient à assurer l’aspect formel et temporel de l’attaque, grâce à l’insertion des opérateurs de la logique temporelle dans ses nœuds.Dans le cadre ainsi défini, la conduite d’une étude de transformation de modèlesest introduite dans la troisième partie. Elle a pu se dérouler d’une manière assez optimale en s’appuyant sur le paradigme Model-Drivent Architecture. Nous avons engagé deux processus de transformation, le premier visant à générer du code NuSMV à partir des modèles SysML en utilisant une transformation par template (Acceleo). Le second assure le passage de l’attaque ExtAttTree vers la formule Computational Tree Logic en utilisant une transformation par programmation (Java). Les modèles générés sont simulés sur le model checker NuSMV. Le système est caractérisé par des attributs ; pour faire des tests de satisfaisabilité, une variation de la valeur de vérité des attributs est effectuée. À cet effet, nous pouvons détecter avec exactitude les conditions qui ont mené à une attaque. En complément de cette approche, deux cas d’étude de voitures connectées ont été proposés (la Jeep Cherokee et la Tesla model S). Des scénarios d’attaque inspirés du réel ont été analysés afin de valider l’approche.Due to their most often complex nature, the control of the security in commu-nicating embedded systems comes up against major difficulties. The adoption of amodel-based approach for verifying system requirements at the earliest stage, i.e. in the design phase, may bring about substantial cost cutting and time saving. In this doctoral thesis, we propose a design-centric approach for the formal verification of an attack scenario satisfiability for embedded communicating systems. Thus, we propose a three-stage approach : i) conceptual modelling of the system, ii) conceptual modelling of the attack, iii) transformation of conceptual models into formal models for verification. For the structural and behavioural modelling of the system, we opted for the SysML language as it offers the best adaptability and extensibility by profiling. In order to personalize the modelling of data flows, we stereotyped ports and connectors according to their technologies and properties. This extension allowed us to monitor the circulation traces of flows between the differentcommunicating subsystems. A documentation of the connectivity profile was pro-posed. For structuring the attack, we put forward an extended attack tree profile termed ExtAttTree. Unlike conventional attack trees, this profile manages to ensure both formal and temporal aspects of the attack, through the insertion of operators of temporal logic in its nodes.We introduce, in the third part, a study of models’ transformation, carried outwithin this predefined framework. The transformation proceeded in a substantially optimized way, based on the Model-Driven Architecture paradigm. We implemented two transformation processes. The first aimed to generate NuSMV code from SysML models by using a transformation by template paradigm with Acceleo. The second ensures the transition from the ExtAttTree attack to the Computational Tree Logic formula using a programming language transformation paradigm with Java. The generated models are simulated on the NuSMV model checker. The system is characterized by attributes ; to achieve satisfiability tests, a variation in the attributes truth-value is carried out. This scheme allows to accurately detect the conditions that led to an attack. As a complement to this approach, we proposed two case studies of connected cars remote attacks (the Jeep Cherokee and the Tesla Model S). The attack scenarios inspired from real-life are analyzed in order to validate the approach