Runtime Verification for security of 6G based systems H/F

Job description: Future 6G networks will enable high-speed data transmission with very low latency. New applications might present significant risks in terms of security. It will be essential to provide techniques for monitoring communication flows at the network protocol level to detect possible intrusions by malicious actors. We propose to use Runtime Verification (RV). RV consists in observing system executions and analyzing them to verify their conformity to a formal reference object. We will focus on security at the network level, and thus, RV techniques dedicated to distributed systems will be used. These techniques involve identifying executions in a communication flow, that do not conform to the system's communication protocols. The foreseen technique makes use of interaction models as formal reference models (e.g. UML sequence diagrams or message sequence charts). Interaction languages define graphical models used to represent the exchange of information between components. In [1], the authors use such interaction models for the RV of concurrent systems, whose executions are logged as execution traces on a single interface. It was later extended to the case of distributed systems in [2]: rather than analyzing a single execution trace, the RV algorithm analyzes a collection of execution traces, logged on the different interfaces associated with the different hardware resources involved in the system. The RV algorithms work offline, i.e., the execution traces are logged before their analysis. An online approach, i.e., where atomic actions are observed via probes and processed as soon as they are observed, is currently under definition. You will contribute to address the following bottlenecks: 1- In [1,2], the approach is based on a centralized solution. Such a solution would not scale up, considering the foreseen 6G communication frequencies. We plan to consider distributed solutions where several RV processes run on smaller clusters of devices. This implies a loss of observability. You will contribute to identifying the best compromise in terms of cluster definition and principles of distributions.  2- The information exchange rates envisaged will lead us to rethink our algorithms, which impose time constraints that are not compatible with target systems. Beyond trying to decrease the execution time of the RV process, we plan to implement a data loss-tolerant approach: in situations where the frequency of message observations is so high that the RV process cannot treat all of them,the RV process should however remain reliable. [1] E. Mahe, C. Gaston, and P. Le Gall. Revisiting Semantics of Interactions for Trace Validity Analysis. International Conference on Fundamental Approaches to Software Engineering (FASE), 2020. [2] E. Mahe, B. Bannour, C. Gaston, A. Lapitre, and P. Le Gall. A small-step approach to multi-trace checking against interactions. Symposium on Applied Computing (SAC), 2021.

Your profile: VOUS AVEZ ENCORE UN DOUTE ? Les à-côtés de votre mission principale peuvent nous intéresser : Un écosystème de recherche à la pointe, unique en son genre et dédié à des thématiques à fort enjeu sociétal, qui donne du sens à votre mission Des formations pour renforcer vos compétences, en acquérir de nouvelles et booster votre mission Un équilibre vie privée / vie professionnelle reconnu par nos collaborateurs La possibilité de télétravailler pour équilibrer les temps de transport et contribuer à votre qualité de vie Un CE riche en avantages et en activités sociales, culturelles et sportives Un lieu de travail au cœur d’un plateau dynamique, entouré d’écoles et d’entreprises de la tech COMPÉTENCES REQUISES : Vous avez un doctorat en informatique dans le domaine des méthodes formelles, de préférence avec des connaissances en Vérification en Temps d'Exécution ou en Test Basé sur les Modèles. Vous êtes intéressé par l'optimisation des algorithmes en termes de temps d'exécution et d'espace mémoire, et vous avez des connaissances en systèmes distribués. Vous appréciez l'application des méthodes formelles à des cas d'utilisation concrets et l'évaluation de leur mise à l'échelle. Vous aimez développer des outils logiciels et avez de l'expérience en programmation (l'expérience en C++ ou en Rust serait un plus).

Languages: English Fluent