Search

This paper presents an ontology based on mutation techniques for the modelling of cybersecurity attacks and its application to 5G networks. Main concepts of network protocols, mutation operators, flow of network packets and network traffic are introduced. An ontology is designed based on different mutation operators that allow to design models that can be assimilated with known and unknown attacks. This approach has been implemented in our open source 5G network traffic fuzzer, 5Greplay, and has been applied to three use cases that are representative of attacks against 5G networks: NAS Replay attack, Denial of Service by Sending Malformed NGAP Packets and 5G encapsulation of IoT traffic.

We present a modular framework for model checking parameterized array-based transition systems with explicit access operations on weak memory. Our approach extends the MCMT (Model Checking Modulo Theories) framework of Ghilardi and Ranise with explicit weak memory models. We have implemented this new framework in Cubicle-W, an extension of the Cubicle model checker. The modular architecture of our tool allows us to change the underlying memory model seamlessly (TSO, PSO...). Our first experiments with a TSO-like memory model look promising.