计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统.

Security and privacy of users’ information in mobile communication networks have drawn increasing attention. The development of 5G system has demanded new protocols to realize authentication and key management service. AKMA (Authentication and Key Management for Application) service aims at establishing authenticated communication between users and application functions. For this purpose, the 3GPP group has standardized 5G AKMA service in Technical Specifications defining the 5G AKMA security architecture and procedures. To ensure security of communication between users and applications, AKMA service should meet strong security properties. In this paper, we apply formal methods to model and analyze the AKMA service. We construct a formal model of AKMA in the Tamarin verification tool, and specify the authentication, secrecy, and privacy properties extracted from informal descriptions given in the Technical Specifications. We identify assumptions for each security property during the modeling process. We prove that some properties are not satisfied, and by analyzing the counterexamples constructed by Tamarin, put forward some potential attacks. Moreover, we propose some suggestions on the 5G AKMA service.

SDN (Software Defined Network) with multiple controllers draws more attention for the increasing scale of the network. The architecture can handle what SDN with single controller is not able to address. In order to understand what this architecture can accomplish and face precisely, we analyze it with formal methods. In this paper, we apply CSP (Communicating Sequential Processes) to model the routing service of SDN under HyperFlow architecture based on OpenFlow protocol. By using model checker PAT (Process Analysis Toolkit), we verify that the models satisfy three properties, covering deadlock freeness, consistency and fault tolerance.

Security and privacy of users' information in mobile communication networks have drawn increasing attention. The development of 5G system has demanded new protocols to realize authentication and key management service. AKMA (Authentication and Key Management for Application) service aims at establishing authenticated communication between users and application functions. For this purpose, the 3GPP group has standardized 5G AKMA service in Technical Specifications defining the 5G AKMA security architecture and procedures. To ensure security of communication between users and applications, AKMA service should meet strong security properties. In this paper, we apply formal methods to model and analyze the AKMA service. We construct a formal model of AKMA in the Tamarin verification tool, and specify the security properties extracted from informal descriptions given in the Technical Specifications. We identify the security assumptions for each security property during the modeling process. We prove that some properties are not satisfied, and by analyzing the counterexamples constructed by Tamarin, put forward some potential attacks. Moreover, we propose some suggestions and fixes for the 5G AKMA service.

Starting with the analysis of the source codes of the Python Software Transactional Memory (PSTM) architecture, this paper applies process algebra CSP to formally verify the architecture at a fine-grained level. We analyze the communication process and components of the architecture from multiple perspectives and establish models describing the communication behaviors of the PSTM architecture. We use model checker PAT to automatically simulate and verify the established model. After adapting the traditional transactional properties to the PSTM architecture, we analyze and verify five properties for the PSTM architecture, including deadlock freeness, atomicity, isolation, consistency and optimism. The verification results indicate that all the properties are valid. Based on the judgement of the execution logic of the communication procedure in the PSTM architecture, we can conclude that the architecture can have a proper communication and can guarantee atomicity, isolation, consistency and optimism. Besides, we also provide a case study with an application scenario and propose a corollary that the value of the shared counter is equal to the number of parallel processes. We verify whether the case study system can satisfy all the conditions of corollary from both positive and negative perspectives. The results show that the corollary is tenable. (C) 2020 Elsevier Inc. All rights reserved.

Software-Defined Networking (SDN) is an emerging paradigm, providing separation of concerns between controllers that manage the network and switches that forward data flow. SDN enables network programmability and reduces the complexity of network control and management. The OpenFlow protocol is a widely accepted interface between SDN controllers and switches. OpenFlow controllers are the core of Software-Defined Networks (SDNs). They collect topology information to build a global and shared view of the network, which is used to provide services for topology-dependent core modules and applications. Therefore, the accuracy of the centralized abstract view of the network is of outermost importance for many essential SDN operations. However, the topology discovery mechanism used in almost all the mainstream OpenFlow controllers suffers from two kinds of topology poisoning attacks: Link Fabrication Attack and Host Hijacking Attack. TopoGuard is a wide-spread secure OpenFlow controller, which improves the standard topology discovery mechanism, providing automatic and real-time detection of these two attacks. However, the mechanism of TopoGuard lacks formal verification, especially in the situation where some hosts are migrating to their new locations. In this paper, we propose a general parameterized framework, including the Communicating Sequential Processes (CSP) models of the network components and the interfaces among them. Two loopholes of TopoGuard are found by implementing and verifying the proposed system model, which is an instance of the framework, in the model checker Process Analysis Toolkit (PAT). Moreover, we propose a new topology discovery mechanism based on TopoGuard, which solves the two loopholes. (C) 2019 Elsevier B.V. All rights reserved.

Software-Defined Networking (SDN) is an emerging networking paradigm, which separates the network’s control logic from the underlying routers and switches, providing the ability to program network, simplifying network management and creating an environment for network evolution. NetKAT is a domain-specific language for specifying and verifying packet-processing functions in software-defined networks (SDNs). This paper proposes a more powerful programming language, PDNet, extending NetKAT to specify the behaviors of SDNs that support virtual local area network (VLAN) tags. We present the operational semantics of PDNet in terms of automata and a syntactic derivatives. When comparing PDNet and NetKAT we show that PDNet is strictly more expressive than NetKAT. As expected, we also show that PDNet is as expressive as NetKAT when describing SDNs without VLAN.

Software Defined Networking (SDN) is an emerging networking paradigm, which provides flexible network programmability and eases the complexity of network control and management. The OpenFlow protocol is the best-known southbound interface of SDN. As the core of a software-defined network, a controller collects topology information of the entire network in order to manage the network as well as provide services to topology-dependent applications. The accuracy of topology information gained by a controller is utmost important. However, most of the mainstream OpenFlow controllers suffer from two kinds of topology poisoning attacks: Link Fabrication Attack and Host Hijacking Attack. TopoGuard is the most famous security extension to traditional OpenFlow controllers, providing detection of the two attacks. In this paper, we model TopoGuard, OpenFlow switches, hosts and two kinds of attackers using Communication Sequential Processes (CSP). Moreover, we encode the proposed model into Process Analysis Toolkit (PAT), a model checker. Finally, we use PAT to verify whether TopoGuard is able to detect the two attacks in some specific scenarios.

Software-Defined Networking (SDN) is an emerging networking paradigm that provides flexible network programmability and reduces the complexity of network management and control. OpenFlow Protocol is the best-known southbound interface of SDN. As one of the most popular OpenFlow controllers, Floodlight is famous for its excellent basic modules, which are used by many other mainstream controllers. Due to the popularity and widespread use of the Floodlight’s modules, it is important to analyze them in a formal framework. In this paper, we focus on six modules of Floodlight that are mainly responsible for pushing decisions and discovering topology. In order to verify whether these modules meet two important requirements, including Decision Pushed Correctly and Rule Installed Once, we propose a system model that formalizes these modules as well as hosts and switches using Communicating Sequential Processes (CSP). Moreover, we add two types of attacks: Link Fabrication and Host Hijacking, which aim at poisoning the topology information collected by a controller, to construct a second system model. Finally, we implement these two system models in Process Analysis Toolkit (PAT), a model checker, to verify whether our models cater for four assertions based on two requirements and if Floodlight is vulnerable to these two attacks.

rTiMo is a real-time version of  TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variable tr is introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form of guarded choice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.

rTiMo is a real-time version of TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variable tr is introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form of guarded choice. This enables us to convert every parallel construct to a guarded choice.

The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.

Hadoop Distributed File System (HDFS) is a high fault-tolerant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Since HDFS is widely used, analysis on it in a formal framework is of great significance. In this paper, we use Communicating Sequential Processes (CSP) to model and analyze HDFS. We mainly focus on the dominant parts which include reading files and writing files in HDFS and formalize them in detail. Moreover, we also model the heartbeat mechanism. Finally, we use the model checker Process Analysis Toolkit (PAT) to simulate the model constructed and verify whether it caters for the specification and some important properties, which include Deadlock-freeness, Minimal Distance Scheme, Mutual Exclusion, Write-Once Scheme and Robustness.

Hadoop Distributed File System (HDFS) is a high fault-tolerant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Since HDFS is widely used, analysis on it in a formal framework is of great significance. In this paper, we use Communicating Sequential Processes (CSP) to model and analyze HDFS. We mainly focus on the dominant parts which include reading files and writing files in HDFS and formalize them in detail. Moreover, we use the model checker Process Analysis Toolkit (PAT) to simulate the model constructed and verify whether it caters for the specification and some important properties, including Deadlock-freeness, Minimal Distance Scheme, Mutual Exclusion, Write-Once Scheme and Robustness.