Verifying Design Properties at Runtime Using an MDE-Based Approach Models @Run.Time Verification-Application to Autonomous Connected Vehicles

• Main Author: Loulou, Hassan
• Other Authors: Université Paris-Saclay (ComUE)
• Language: en
• Published: 2017
• Subjects: [e-mail]; Self-Adaptative; Formal methods; Securité; Véhicules Connectés Autonomes; Model@runtime; Runtime adaptation; Autonomous connected vehicles
• Online Access: http://www.theses.fr/2017SACLS405

Un véhicule autonome et connecté (ACV – pour Autonomous Connected Vehicle ) est un système cyber-physique où le monde réel et l’espace numérique virtuel se fusionnent. Ce type de véhicule requiert un processus de validation rigoureuse commençant à la phase de conception et se poursuivant même après le déploiement du logiciel. Un nouveau paradigme est apparu pour le monitorat continu des exécutions des logiciels afin d'autoriser des adaptations automatiquement en temps réel, systématiquement lors d’une détection de changement dans l'environnement d'exécution, d’une panne ou d’un bug. Ce paradigme s’intitule : « [e-mail] ». Cette thèse s’inscrit dans le cadre des ACVs et plus particulièrement dans le contexte des véhicules qui collaborent et qui partagent leurs données d’une manière sécurisée. Plusieurs approches de modélisation sont déjà utilisées pour exprimer les exigences relatives au contrôle d'accès afin d’imposer des politiques de sécurité. Toutefois, leurs outils de validation ne tiennent pas compte les impacts de l'interaction entre les exigences fonctionnelles et les exigences de sécurité. Cette interaction peut conduire à des violations de sécurité inattendues lors de l'exécution du système ou lors des éventuelles adaptations à l’exécution. En outre, l’estimation en temps réel de l’état de trafic utilisant des données de type crowdsourcing pourrait être utilisée pour les adaptations aux modèles de coopération des AVCs. Cette approche n'a pas encore été suffisamment étudiée dans la littérature. Pour pallier à ces limitations, de nombreuses questions doivent être abordées:• L'évolution des exigences fonctionnelles du système doit être prise en compte lors de la validation des politiques de sécurité ainsi que les scénarios d'attaque doivent être générés automatiquement.• Une approche pour concevoir et détecter automatiquement les anti-patrons (antipatterns) de sécurité doit être développée. En outre, de nouvelles reconfigurations pour les politiques de contrôle d'accès doivent également être identifiées, validées et déployées efficacement à l'exécution.• Les ACVs doivent observer et analyser leur environnement, qui contient plusieurs flux de données dite massives (Big Data) pour proposer de nouveaux modèles de coopération, en temps réel.Dans cette thèse, une approche pour la surveillance de l'environnement des ACVs est proposée. L’approche permet de valider les politiques de contrôle d'accès et de les reconfigurer en toute sécurité. La contribution de cette thèse consiste à:• Guider les Model Checkers de sécurité pour trouver automatiquement les scénarios d'attaque dès la phase de conception.• Concevoir des anti-patterns pour guider le processus de validation, et développer un algorithme pour les détecter automatiquement lors des reconfigurations des modèles.• Construire une approche pour surveiller en temps réel les flux de données dynamiques afin de proposer des adaptations de la politique d'accès lors de l'exécution.L’approche proposée a été validée en utilisant plusieurs exemples liés aux ACVs, et les résultats des expérimentations prouvent la faisabilité de cette approche. === Autonomous Connected Vehicles (ACVs) are Cyber-physical systems (CPS) where the computationalworld and the real one meet. These systems require a rigorous validation processthat starts at design phase and continues after the software deployment. Models@Runtimehas appeared as a new paradigm for continuously monitoring software systems execution inorder to enable adaptations whenever a change, a failure or a bug is introduced in the executionenvironment. In this thesis, we are going to tackle ACVs environment where vehicles tries tocollaborate and share their data in a secure manner.Different modeling approaches are already used for expressing access control requirementsin order to impose security policies. However, their validation tools do not consider the impactsof the interaction between the functional and the security requirements. This interaction canlead to unexpected security breaches during the system execution and its potential runtimeadaptations. Also, the real-time prediction of traffic states using crowd sourcing data could beuseful for proposition adaptations to AVCs cooperation models. Nevertheless, it has not beensufficiently studied yet. To overcome these limitations, many issues should be addressed:• The evolution of the system functional part must be considered during the validation ofthe security policy and attack scenarios must be generated automatically.• An approach for designing and automatically detecting security anti-patterns might bedeveloped. Furthermore, new reconfigurations for access control policies also must befound, validated and deployed efficiently at runtime.• ACVs need to observe and analyze their complex environment, containing big-datastreams to recommend new cooperation models, in near real-time.In this thesis, we build an approach for sensing the ACVs environment, validating its accesscontrol models and securely reconfiguring it on the fly. We cover three aspects:• We propose an approach for guiding security models checkers to find the attack scenariosat design time automatically.• We design anti-patterns to guide the validation process. Then, we develop an algorithmto detect them automatically during models reconfigurations. Also, we design a mechanismfor reconfiguring the access control model and we develop a lightweight modularframework for an efficient deployment of new reconfigurations.• We build an approach for the real-time monitoring of dynamic data streams to proposeadaptations for the access policy at runtime.Our proposed approach was validated using several examples related o ACVs. the results ofour experimentations prove the feasibility of this approach.