Collaborative Modeling And Analysis Of Functional Safety And Security In Network Protocols

The development of IoT and the emerge of the 5G era have created a variety of network service requirements.The effective method of designing dedicated network protocols for specific network service scenarios also pushes protocol engineering into the vision of relevant researchers and developers.However,the design of a network protocol always needs to consider its correctness,robustness,and ability to resist malicious attacks in a network environment.Today,with the vigorous development of formal verification technology and the increasing computing power,the concerns in the protocol design are gradually abstracted and summarized into the functional safety properties and security properties of the formal model.But model abstraction itself is still a quite difficult task.Even though many network protocol modeling and analysis methods have been proposed over the past few decades,most of these works force the separation of functional safety properties and security properties into different models,without direct considering the association.Therefore,there are still problems such as model equivalence and potential conflicts.Although there have been some works devoted to collaborative modeling and analysis in recent years,these works are mainly applicable to specific industrial control or cyber-physical systems,and they do not perform well when applied to general network protocols with variable and heterogeneous structures.Based on fully researching and understanding relevant formal verification and collaborative modeling work,we combining the characteristics of network protocols such as distribution,message flowability,and configurability.This paper proposes a collaborative modeling and analysis method for functional safety and security in network protocols,which is used to construct a complete methodology of protocol modeling and protocol analysis.Besides,a case study is carried out through implementation tools.Concretely,the main works of this paper includes:1.We design a collaborative modeling framework for functional safety and security elements suitable for general network protocols.The framework can be subdivided into three parts: protocol template modeling,protocol behavior modeling and protocol architecture modeling.Based on this,we give several types of functional safety and security property specifications.The protocol template modeling includes the structured data types involved in the protocol running process,the abstract process in the protocol and its attributes and communication ports,the abstract environment in which the protocol process is located,its attributes and logical channels.And the description of the initial knowledge of the attacker,the axiomatic relationship between the functions in the protocol,etc.Protocol behavior modeling introduces the process graph state machine and various action steps on it to describe the message packaging,extraction,cryptographic operations,and communication operations of the process in detail.The protocol architecture modeling introduces the instantiated topology graph model,and describes the actual execution process in the protocol,the corresponding attribute parameters,and communication relationship.2.Based on the aforementioned unified semantic modeling framework,we design a kind of model transformation methods.Firstly,based on the full investigation of the project structure of the UPPAAL model checking tool and the ProVerif security protocol verification tool,a set of syntax alignment models are respectively constructed,which can express these two models in a structured manner.Then,various modeling elements in the unified semantic modeling framework are mapped to them.To realize the semantic translation from the unified semantic model to the UPPAAL and ProVerif project.3.Based on the modeling and transformation methodology of this paper,we implement a set of full-process tools using C# language and Avalonia framework,which includes graphical modeling and transformation functions to UPPAAL and ProVerif.We also give a case study and analysis based on the implementation tool with the initialization process of the 5G-AKA network protocol.And compare the models before and after translation with the verification results,which support the effectiveness of our methodology and implementation tools in this paper.To sum up,this paper designs a unified semantic model for general network protocols,models functional safety and security elements collaboratively,and converts them to UPPAAL and ProVerif formal verification tools to verify functional safety properties and security properties.With the help of implementation tools and 5G-AKA protocol initialization process to carry out case analysis.The final analysis results are in line with expectations,confirming the effectiveness of this work.