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.

You have a PhD in computer science in the field of formal methods, ideally, with knowledge in Runtime Verification or Model-Based Testing. You are interested in optimizing algorithms in execution time and in memory space, and know about distributed systems. You appreciate applying formal methods on concrete use cases and evaluating their scaling. You enjoy developing software tools and have programming experience (experience in C++ or Rust would be a plus).