Edge computing has emerged as the leading framework for addressing the need for low latency and high reliability in various applications. To achieve efficient completion of tasks in edge computing, considerable efforts have been made to design effective offloading strategies. However, most of these strategies are proposed without undergoing quantitative analysis and verification to ensure their correctness and robustness. Therefore, this paper presents a hybrid offloading strategy framework, encompassing delay-based, energy-efficient, and energy-delay tradeoff strategies, aimed at improving the comprehensibility and verifiability of offloading strategies, and addressing this gap. Additionally, we employ probabilistic model checking, specifically Prism, to quantitatively analyze and validate the reliability of the proposed hybrid framework. Our method addresses the need for rigorous quantitative analysis and verification of edge computing offloading strategies, ensuring the correctness and robustness. The outcomes of this paper provide practical solutions and insights to the field, advancing the development of trustworthy and efficient offloading strategies for edge computing systems.

Industrial edge computing has emerged as a pivotal paradigm to enhance the efficiency and responsiveness of industrial processes through decentralized data processing. Subsequently, ensuring the reliability of resource allocation becomes paramount. This paper presents a novel approach that combines probabilistic model checking and machine learning techniques for conducting reliability analysis of resource allocation in industrial edge computing environments. By leveraging probabilistic model checking, we can formally verify the system's behavior and assess the likelihood of resource allocation failures. Moreover, we integrate machine learning algorithms to predict potential resource allocation issues based on historical data patterns. This hybrid approach named RAVF framework offers a comprehensive perspective on reliability assessment, encompassing both theoretical analysis and data-driven insights. Through experiments and case studies, we demonstrate the effectiveness of our approach in identifying vulnerabilities in resource allocation and providing actionable insights for system optimization. The synergy between probabilistic model checking and machine learning equips industrial edge computing with a robust resource allocation framework that enhances overall system dependability.

Traditional IoT authentication methods, often centralized and reliant on a Trusted Third Party (TTP), face issues like high communication costs and vulnerability to data loss. Blockchain-based Internet of Things (IoT) authentication can effectively solve the problems brought by traditional IoT authentication. Because the authentication schemes are usually deployed on a large number of IoT devices it would be extremely expensive when there are issues to be fixed after the authentication schemes is deployed. Performing verification early at design time can alleviate this problem. To focus on these requirements, this article proposes a formal verification framework for blockchain-based IoT authentication (FVF-BIoT). Specifically, we design data type mapping and the conversion of elements in smart contracts for the authentication. Then we formalize the smart contracts into formal models in the interactive theorem prover Coq. Several algorithms are presented for the conversion of the smart contracts and the generation of examples. Examples and security properties related to contracts are described in the form of theorems, which are also proved by Coq. Through a case study, we not only demonstrate the effectiveness of the FVF-BIoT framework in ensuring the security and reliability of blockchain technology for IoT authentication but also highlight its innovative integration of formal verification processes. This distinctly addresses the previously unmet need for rigorous, mathematically proven security validations in the design and deployment of blockchain-based IoT authentication methods.

Software complexity is the very essence of computer programming. As the complexity increases, the potential risks and defects of software systems will increase. This makes the software correctness analysis and the software quality improvement more difficult. In this paper, we present a quantitative metric to describe the complexity of a hierarchical software and a Complexity-oriented Software Architecture Refactoring (CoSSR) approach to reduce the complexity. The main idea is to identify and then reassemble subcomponents into one hierarchical component, which achieves minimum complexity in terms of the solution algorithm. Moreover, our algorithm can be improved by introducing partition constraint, heuristic search strategy, and spectral clustering. We implement the proposed method as an automated refactoring tool and demonstrate our algorithm through a case study of battery management system (BMS). The results show that our approach is more efficient and effective to reduce the complexity of hierarchical software system.

As IoT in a multi-server environment increases resources’ utilization, more and more problems of IoT authentication and key agreement are being revealed. The Authentication and Key Agreement (AKA) protocol plays an important role in solving these problems. Many AKA protocols have been proposed, and some of them support their own verifications. However, a unifying verification framework for multi-server IoT is lacking. In this article, we propose a formal verification framework of AKA protocols for multi-server IoT (FVF-AKA). It supports the construction of CSP models for the AKA protocol, the implementation of the CSP models in PAT with C#, and the verification of formal models. With the help of C#, many complex functions in the AKA protocol can be implemented. We also design an algorithm to support automatic conversion from the CSP model to the PAT model. FVF-AKA can verify four fundamental properties (deadlock freedom, entity legitimacy, timeout delay, and session key consistency). It also supports the verification of security properties for the AKA protocol suffering from four different attacks (relay attacks, denial of service attacks, server spoofing attacks, and session key attacks). Our approach can be applied to most AKA protocols for multi-server IoT generally. By applying FVF-AKA to two AKA protocols, we can verify whether they satisfy the fundamental properties and analyze their security properties in vulnerable environments. Our work would help to analyze the AKA protocol for multi-server IoT and provide the foundation for the analysis of enhancing its security and robustness.

The Internet of Things (IoT) generates vast amounts of data from numerous applications. However, since wireless channels are the primary means of communication, IoT networks are vulnerable to several security threats, which can compromise their security and privacy. To address these issues, various user authentication protocols have been proposed. Thus, it is still a challenge to provide multi-granularity verifications for different authentications of the IoT. In this paper, we propose a multi-granularity formal framework of user authentication for the IoT (MFF-IoT). Our framework builds different formal models (specification language HLPSL models, process algebra CSP models, Timed CSP models, and timed automata) to complete multi-granularity formal verification. By using both coarse-grained and fine-grained modeling, we can balance the tradeoff between model complexity and verification accuracy. Specifically, our fine-grained models provide a more detailed representation of the framework's behavior and enable us to perform timing-related probability analysis. As these formal models can be implemented by model-checking tools (AVISPA, PAT with C#, and UPPAAL), important properties and features can be analyzed and verified. We also propose several algorithms for better formal model building and evaluate our framework with a case study to show its practicality and effectiveness.

As a crucial component of intelligent transportation system, Internet of Vehicles (IoV) plays an important role in the smart and intelligent cities. However, current Internet architectures cannot guarantee efficient data delivery and adequate data security for IoV. Therefore, Named Data Networking (NDN), a leading architecture of Information-Centric Networking (ICN), is introduced into IoV. Although problems about data distribution can be resolved effectively, the combination of NDN and IoV causes some new security issues. In this paper, we apply Communicating Sequential Processes (CSP) to formalize NDN-based IoV. We mainly focus on its data access mechanism and model this mechanism in detail. By feeding the formalized model into the model checker Process Analysis Toolkit (PAT), we verify four vital properties, namely, deadlock freedom, data reliability, PIT deletion faking, and CS caching pollution. According to verification results, the model cannot ensure the security of data with the appearance of intruders. To solve these problems, we construct a blockchain-based mechanism by creating a blockchain-based distribution trusted platform on top of NDN-based IoV. Through the analysis of the improved model, the blockchain-based mechanism can truly guarantee the security of NDN-based IoV.

The combination of D2D (Device to Device) communication and MEC (Mobile Edge Computing) architecture is adopted to reduce the communication delay in 5G. With the extensive use of HPS (high performance switch) as the main medium of data distribution in the device layer, the holistic power consumption and delay can be guaranteed stably, mainly because HPS has the mechanism of Master-Slave scheme to ensure the robustness. However, as far as we know, there are fewer studies to verify the safety validation of the design using formal methods. Hence, we study it through timed automata and model checking. This paper integrates HPS into D2D communication design in MEC, selects the Master-Slave synchronization and switchover scheme in HPS as the research object, describes the scheme based on timed automata, and then verifies seven fundamental but essential properties through the model checker UPPAAL. Through verification, comparison and analysis of possible scenarios in our constructed model, it can be concluded that the design of the HPS in MEC can conform to its required specification. Further, it can not only enhance the safety validation of the combination of D2D communication and MEC architecture, but also provide a guide for the newest subsequent high safety primary-backup design in industry.

Mobile Edge Computing (MEC) is proposed to meet the requirements of mobile users for low latency and response time, and its edge nodes will download data from the cloud server in advance, which arouses researchers to pay attention to the privacy-preserving authentication of mobile users and edge nodes, as well as the data integrity verification of edge nodes. Therefore, it is essential and crucial to integrate the authentication methods into data integrity verification protocol. In this paper, we propose a new integrated protocol AICE, i.e., a uthentication and i ntegrity c hecking on e dges, and then formally analyze and automatically validate the correctness and authentication security of the protocol. We first give the information flows of the AICE protocol by combining the privacy-preserving authentication (PPA) protocol and integrity checking protocol for MEC (ICE) together. According to the features of the AICE protocol, we then select the SVO logic to conduct the formal analysis of the protocol from the perspective of theoretical analysis of modal logic. Furthermore, we employ the AVISPA tool to validate the correctness of the protocol from the perspective of mechanical automatic analysis. The theoretical analysis and mechanical results demonstrate that the integrated protocol AICE satisfies the correctness and authentication.

Mobile Edge Computing (MEC), as an emerging technology, is proposed to solve the time delay problem in 5G era, especially in the field of autonomous driving. The core idea of MEC is to offload the task to the nearest device/server for computation, i.e., sinking the computation, so as to reduce the delay and congestion. Actually, there are lots of researches on MEC offloading strategy, but there is little research on the computation of its offloading characteristics. Therefore, in this paper, we first propose a secure hierarchical calculus SC4MEC to describe the features of MEC. We also give the syntax and operational semantics of this calculus from the process and network levels, and simulate the calculus in Maude. Meanwhile, local ecology is applied to the communication channel to further reduce the authentication delay of the device with the same identity and ensure the security of the transmission data. We also propose to extend the communication radius of MEC server or cloud server by rule Enlarge, in order to ensure the mobile devices's connectivity while the consumption of resources is minimized. Finally, we employ SC4MEC calculus to a small example about device to device communication with automated implementation.

With the popularization and development of 5G, it is vital to guarantee the security of the whole data while transmitting them at high speed. Data Distribution Service (DDS), as the core technology of network data communication, is one of the most significant protocols. The Real Time Publish Subscribe (RTPS) protocol is part of DDS, which emphasizes data publishing and receiving.In this paper, we focus on the Behavior module of the RTPS protocol, where the reliable modes are always to ensure the reliability of data. Thus, we adopt CSP to model eight core components and add corresponding intruders to attack the model in order to verify and detect the potential risks of the design. Specifically, we also improve our model by utilizing digital signature and digital certificate. Five properties abstracted from the specification have been verified through the model checker PAT. The result shows that once adding the digital signature and digital certificate together, there is no situation that publisher and subscriber are unauthorized; in addition, due to multiple encryption, data cannot be faked or intercepted. However, the history-cache still can be faked for it has no identity authentication. That is to say, to be highly trustworthy, developers need to ensure mutual authentication between modules as much as possible. Consequently, we hope this method makes sense for researches on security of data distribution protocol and gives a meaningful guide for DDS middleware development.

As a leading architecture of Information-Centric Networking (ICN), Named Data Networking (NDN) plays an important role in the future network construction. NDN retrieves and identifies a data packet according to the packet's name instead of its IP address. Conventional protocols of TCP/IP Internet are unsuitable for NDN. Therefore, Named-data Link State Routing protocol (NLSR) is proposed as an intra-domain routing protocol for NDN. Although NLSR applies a five-layer trust model to guarantee its data security, there are still a lot of security issues in its data access mechanism, such as the fake and leakage of data. In this paper, we apply Communicating Sequential Processes (CSP) to formalize this mechanism. Using Process Analysis Toolkit (PAT), we verify four properties, including deadlock freedom, data availability, data security and data decryption. According to the verification results, the trust model cannot protect the data from fake and leakage once intruders appear. We adopt a method similar to digital signature in the first improved model. However, the process of obtaining keys still needs to be executed multiple times during the verification of a data packet. To further accelerate the key fetching and verification process, all the keys, needed to validate a data packet, are packaged in a special packet of the second improvement.

Vehicular Ad Hoc Network (VANET) is a subclass of Mobile Ad Hoc Network (MANET) types. As a key part of the Intelligent Transportation Systems (ITSs) framework, it can be used not only to provide value added services, but also to guarantee the security of ITS. Since VANET is extensively applied, its security is of great significance. In this paper, we model the architecture of VANET using process algebra Communicating Sequential Processes (CSP). By utilizing model checker Process Analysis Toolkit (PAT), we verify five properties (deadlock freedom, divergence freedom, data leakage, vehicle faking and RSU faking) of the model and find that the proposed architecture may cause data leakage. Hence, we improve the model by encrypting the messages with receiver’s public key to cope with this problem. The new verification results show that our study can guarantee the security of VANET.

Named Data Networking (NDN) is a new promising architecture of information-centric networking. Traditional mechanisms of access control can no longer fit appropriately, because of its caching property. Hamdane et al. propose a new access control solution for both closed and open environments. In this paper, we make the very first attempt to formally analyze this access control solution. Inspired by the basic BAN logic, we adding some new notions to it to propose our BAN-like logic. It can describe the access control solution. In the form of the beliefs of principals, the procedures of the access control solution are idealized. Under several security goals with a set of logical postulates, the idealized procedures are analyzed. We give the modification to make the solution safer. Then we introduce the man-in-the-middle attack into the access control solution and check the insecurity properties. The improvement is given according to the result. Our study helps to improve security and protect against various attacks for the access control solution.

ZooKeeper Atomic Broadcast (Zab) is an atomic broadcast protocol specially designed for ZooKeeper, which supports additional crash recovery. This protocol actually has been widely adopted by famous Internet companies, but there are few studies on the correctness and credibility of the Zab protocol, and thus we utilize formal methods to study the correctness. In this paper, Zab, Paxos and Raft are all analyzed and compared to help better understand the Zab protocol. Then we model the Zab protocol with TLA+ and verify three properties abstracted from the specification by the model checker TLC, including two liveness properties and one safety property. The final experimental results can prove that the design of the protocol conforms to the original requirements. This paper makes up for the analysis of formal methods in the Zab protocol.

Named Data Networking (NDN) is an architecture of Information-Centric Networking (ICN). The application of NDN on wireless networks is an important area. In this paper, we propose a Security Calculus for Wireless Networks of Named Data Networking (SCWN). Security feature is implemented by using different channel symbols to describe wireless network node. The feature of NDN is introduced by using particular sets to express the environment. We introduce the syntax and the operational semantics of SCWN calculus. By a rewriting logic-based language Maude, we support the automatic implementation of our SCWN calculus, which enhances its practicability. Finally, we apply SCWN calculus to LFBL protocol with its automatic implementation. It indicates that SCWN calculus is useful to describe realistic cases.

As a programming model, Spark is popularly and widely used in processing and generating large cluster of data sets distributed on large amounts of machines. With its widespread use, its validity and other major properties need to be analyzed in a formal framework. And unfortunately, there is nearly no research conducted to describe the interactions in Spark on YARN. In this paper, we focus on the dominant parts of Spark on YARN and formalize them using Communicating Sequential Processes (CSP) in detail. In the formal model, the processing and function of each component are clearly described. By feeding the models into the model checker Failures Divergence Refinement (FDR), we have verified some crucial properties, including Deadlock Freedom, Divergence Freedom, Robustness and Load Balancing. Our work demonstrates that Spark on YARN can guarantee important properties in some applications.

The Real Time Publish Subscribe protocol (RTPS), as a Data Distribution Service (DDS) protocol for computer systems, is composed of several modules.We focus on RTPS StatefulWriter Module which has two patterns, reliable pattern and best-effort pattern.As the main module of sending and receiving messages, its security and reliability are of great concern.The formal method can analyze whether it is a highly credible model from the mathematical point of view.Our research pays attention to the reliable pattern.Thus it is of great importance to model and verify whether the pattern is reliable through formal methods.In this paper, we model seven components of the module using Communicating Sequential Processes (CSP).By feeding the models into the model checker Process Analysis Toolkit (PAT), we verify four properties, divergence free, acknowledgement mechanism, data consistency and sequentiality.Consequently, it can be apparently concluded that the pattern of this module is reliable, which totally caters for its specification.

Named Data Networking (NDN) is a new promising architecture of information-centric networking. NDN could not reuse the existing access control solutions designed for the IP architecture due to their fundamental difference of design, as well as NDNs caching property. As a result, several access control solutions have been proposed for NDN. One of them is specially for both closed and open environment. In this paper, we make the very first attempt to model and verify several important properties of NDN access control. We adopt CSP (Communicating Sequential Processes) to model the NDN access control proposed by Hamdane et al., as well as their security properties. By feeding the models into the model checker PAT (Process Analysis Toolkit), we have verified that the NDN access control cannot prevent the NK key pair faking and the data leakage with the appearance of intruders. We introduce a new method to solve these issues. Considering the situation when the entities are invaded, we also improve our method to make the NDN access control strong enough to maintain the property of key authenticity and data security in this vulnerable situation. We hope that our study would help enhancing the adaptability and robustness of the NDN access control.