Biblio

Analyzing safety and security requirements remains a difficult task in the development of real-life network protocols. Although numerous modeling and analyzing methods have been proposed in the past decades, most of them handle safety and security requirements separately without considering their interplay. In this work, we propose a collaborative modeling framework that enables co-analysis of safety and security requirements for network protocols. Our modeling framework is based on a well-defined type system and supports modeling of network topology, message flows, protocol behaviors and attacker behaviors. It also supports the specification of safety requirements as temporal logical formulae and typical security requirements as queries, and leverages on the existing verification tools for formal safety and security analysis via model transformations. We have implemented this framework in a prototype tool CMSS, and illustrated the capability of CMSS by using the 5G AKA initialization protocol as a case study.

We present a formal OpenFlow-based network programming language (OF) including various flow rules, which can not only describe the behaviors of an individual switch, but also support to model a network of switches connected in the point-to-point topology. Besides, a topology-oriented operational semantics of the proposed language is explored to specify how the packet is processed and delivered in the OpenFlow-based networks. Based on the formal framework, we also propose an approach to detect potential security threats caused by the conflict of dynamic flow rules imposed by dynamic OpenFlow applications.