To cater for the scenario of coordinated transportation of multiple trucks on the highway, a platoon system for autonomous driving has been extensively explored in the industry. Before such a platoon is deployed, it is necessary to ensure the safety of its driving behavior, whereby each vehicle’s behavior is commanded by the decision-making function whose decision is based on the observed driving scenario. However, there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system. In this paper, we focus on the platoon driving scenario, whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways. We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’ cooperative driving behaviors. The existing Multi-Lane Spatial Logic (MLSL) with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective. To cater for the platoon system’s multi-vehicle perspective, we modify the existing abstract model and propose a Multi-Agent Spatial Logic (MASL) that extends MLSL by relative orientation and multi-agent observation. We then utilize a timed automata type supporting MASL formulas to model vehicles’ decision controllers for platoon driving. Taking the behavior of a human-driven vehicle (HDV) joining the platoon as a case study, we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.

Allocation, dereferencing, and freeing of memory data in kernels are coherently linked. There widely exist real cases where the correctness of memory is compromised. This incorrectness in kernel memory brings about significant security issues, e.g., information leaking. Though memory allocation, dereferencing, and freeing are closely related, previous work failed to realize they are closely related. In this paper, we study the life-cycle of kernel memory, which consists of allocation, dereferencing, and freeing. Errors in them are called memory life-cycle (MLC) bugs. We propose an in-depth study of MLC bugs and implement a memory life-cycle bug sanitizer (MEBS) for MLC bug detection. Utilizing an interprocedural global call graph and novel identification approaches, MEBS can reveal memory allocation, dereferencing, and freeing sites in kernels. By constructing a modified define-use chain and examining the errors in the life-cycle, MLC bugs can be identified. Moreover, the experimental results on the latest kernels demonstrate that MEBS can effectively detect MLC bugs, and MEBS can be scaled to different kernels. More than 100 new bugs are exposed in Linux and FreeBSD, and 12 common vulnerabilities and exposures (CVE) are assigned.

Modern multiprocessors deploy a variety of weak memory models (WMMs). Total Store Order (TSO) is a widely-used weak memory model in SPARC implementations and x86 architecture. It omits the store-load constraint by allowing each core to employ a write buffer. In this paper, we apply Unifying Theories of Programming (abbreviated as UTP) in investigating the trace semantics for TSO, acting in the denotational semantics style. A trace is expressed as a sequence of snapshots, which records the changes in registers, write buffers and the shared memory. All the valid execution results containing reorderings can be described after kicking out those that do not satisfy program order and modification order. This paper also presents a set of algebraic laws for TSO. We study the concept of head normal form, and every program can be expressed in the head normal form of the guarded choice which is able to model the execution of a program with reorderings. Then the linearizability of the TSO model is supported. Furthermore, we consider the linking between trace semantics and algebraic semantics. The linking is achieved through deriving trace semantics from algebraic semantics, and the derivation strategy under the TSO model is provided.

A quantum circuit is a computational unit that transforms an input quantum state to an output state. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

Programmable logic controllers (PLCs) play a critical role in many industrial control systems, yet face increasingly serious cyber threats. In this paper, we propose a novel PLC-compatible software-based defense mechanism, called Heterogeneous Redundant Proactive Defense Framework (HRPDF). We propose a heterogeneous PLC architecture in HRPDF, including multiple heterogeneous, equivalent, and synchronous runtimes, which can thwart multiple types of attacks against PLC without the need of external devices. To ensure the availability of PLC, we also design an inter-process communication algorithm that minimizes the overhead of HRPDF. We implement a prototype system of HRPDF and test it in a real-world PLC and an OpenPLC-based device, respectively. The results show that HRPDF can defend against multiple types of attacks with 10.22% additional CPU and 5.56% additional memory overhead, and about 0.6 ms additional time overhead.

The Linux kernel adopts a large number of security checks to prevent security-sensitive operations from being executed under unsafe conditions. If a security-sensitive operation is unchecked, a missing-check issue arises. Missing check is a class of severe bugs in software programs especially in operating system kernels, which may cause a variety of security issues, such as out-of-bound accesses, permission bypasses, and privilege escalations. Due to the lack of security specifications, how to automatically identify security-sensitive operations and their required security checks in the Linux kernel becomes a challenge for missing-check analysis. In this paper, we present an accurate missing-check analysis method for Linux kernel, which can automatically infer possible security-sensitive operations. Particularly, we first automatically identify all possible security check functions of Linux. Then according to their callsites, a two-direction analysis method is leveraged to identify possible security-sensitive operations. A missing-check bug is reported when the security-sensitive operation is not protected by its corresponding security check. We have implemented our method as a tool, named AMCheX, on top of the LLVM (Low Level Virtual Machine) framework and evaluated it on the Linux kernel. AMCheX reported 12 new missing-check bugs which can cause security issues. Five of them have been confirmed by Linux maintainers.

Contextual refinement is a compositional approach to compositional verification of concurrent objects. There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification. However, these program logics for contextual refinement verification cannot support objects with resource ownership transfer, which is a common pattern in many concurrent objects, such as the memory management module in OS kernels, which transfers the allocated memory block between the object and clients. In this paper, we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer. We also design a program logic to verify contextual refinement of concurrent objects w.r.t. their abstract specifications. We have successfully applied our logic to verifying an implementation of the memory management module, where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

Exception management, as the lowest level function module of the operating system, is responsible for making abrupt changes in the control flow to react to exception events in the system. The correctness of the exception management is crucial to guaranteeing the safety of the whole system. However, existing formal verification projects have not fully considered the issues of exceptions at the assembly level. Especially for real-time operating systems, in addition to basic exception handling, there are nested exceptions and task switching by exceptions service routine. In our previous work, we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer. Building on earlier work, this paper proposes EMS (Exception Management SPARCv8), a practical Hoare-style program framework to verify the exception management based on SPARCv8 (Scalable Processor Architecture Version 8) at the design layer. The framework describes the low-level details of the machine, such as registers and memory stack. It divides the execution logic of the exception management into six phases for comprehensive formal modeling. Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example, we use the EMS framework to verify the exception management. All the formalization and proofs are implemented in the interactive theorem prover Coq.

Many applications need to meet diverse requirements of a large-scale distributed user group. That challenges the current requirements engineering techniques. Crowd-based requirements engineering was proposed as an umbrella term for dealing with the requirements development in the context of the large-scale user group. However, there are still many issues. Among others, a key issue is how to merge these requirements to produce the synthesized requirements description when a set of requirements descriptions from different participants are received. Appropriate techniques are needed for supporting the requirements synthesis. Diagrams are widely used in industry to represent requirements. This paper chooses the activity diagrams and proposes a novel approach for the activity diagram synthesis which adopts the genetic algorithm to repeatedly modify a population of individual solutions toward an optimal solution. As a result, it can automatically generate a resulting diagram which combines the commonalities as many as possible while leveraging the variabilities of a set of input diagrams. The approach is featured by: 1) the labelled graph proposed as the representation of the candidate solutions during the iterative evolution; 2) the generalized entropy proposed and defined as the measurement of the solutions; 3) the genetic algorithm designed for sorting out the high-quality solution. Four cases of different scales are used to evaluate the effectiveness of the approach. The experimental results show that not only the approach gets high precision and recall but also the resulting diagram satisfies the properties of minimization and information preservation and can support the requirements traceability.

Dialogue state tracking (DST) leverages dialogue information to predict dialogues states which are generally represented as slot-value pairs. However, previous work usually has limitations to efficiently predict values due to the lack of a powerful strategy for generating values from both the dialogue history and the predefined values. By predicting values from the predefined value set, previous discriminative DST methods are difficult to handle unknown values. Previous generative DST methods determine values based on mentions in the dialogue history, which makes it difficult for them to handle uncovered and non-pointable mentions. Besides, existing generative DST methods usually ignore the unlabeled instances and suffer from the label noise problem, which limits the generation of mentions and eventually hurts performance. In this paper, we propose a unified shared-private network (USPN) to generate values from both the dialogue history and the predefined values through a unified strategy. Specifically, USPN uses an encoder to construct a complete generative space for each slot and to discern shared information between slots through a shared-private architecture. Then, our model predicts values from the generative space through a shared-private decoder. We further utilize reinforcement learning to alleviate the label noise problem by learning indirect supervision from semantic relations between conversational words and predefined slot-value pairs. Experimental results on three public datasets show the effectiveness of USPN by outperforming state-of-the-art baselines in both supervised and unsupervised DST tasks.

Graph neural networks (GNNs) have shown great power in learning on graphs. However, it is still a challenge for GNNs to model information faraway from the source node. The ability to preserve global information can enhance graph representation and hence improve classification precision. In the paper, we propose a new learning framework named G-GNN (Global information for GNN) to address the challenge. First, the global structure and global attribute features of each node are obtained via unsupervised pre-training, and those global features preserve the global information associated with the node. Then, using the pre-trained global features and the raw attributes of the graph, a set of parallel kernel GNNs is used to learn different aspects from these heterogeneous features. Any general GNN can be used as a kernal and easily obtain the ability of preserving global information, without having to alter their own algorithms. Extensive experiments have shown that state-of-the-art models, e.g., GCN, GAT, Graphsage and APPNP, can achieve improvement with G-GNN on three standard evaluation datasets. Specially, we establish new benchmark precision records on Cora (84.31%) and Pubmed (80.95%) when learning on attributed graphs.

This paper proposes the Content Diffusion Model (CDM) for modeling the content diffusion process in information-centric networking (ICN). CDM is inspired by the epidemic model and it provides a method of theoretical quantitative analysis for the content diffusion process in ICN. Specifically, CDM introduces the key functions to formalize the key factors that influence the content diffusion process, and thus it can construct the model via a simple but efficient way. Further, we derive CDM by using different combinations of those key factors and put them into several typical ICN scenarios, to analyze the characteristics during the diffusion process such as diffusion speed, diffusion scope, average fetching hops, changing and final state, which can greatly help to analyze the network performance and application design. A series of experiments are conducted to evaluate the efficacy and accuracy of CDM. The results show that CDM can accurately illustrate and model the content diffusion process in ICN.