Bounded Verification of Multi-threaded Programs via Lazy Sequentialization

Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.

Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this article, we present and study the logic rLTL, which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula φ, of size at most O(3 |φ |), where |φ | is the length of φ. This result improves upon the previously known bound of O(5|φ |) for rLTL verification and is closer to the LTL bound of O(2|φ |). The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.

Context-bounded verification of thread pools

Thread pooling is a common programming idiom in which a fixed set of worker threads are maintained to execute tasks concurrently. The workers repeatedly pick tasks and execute them to completion. Each task is sequential, with possibly recursive code, and tasks communicate over shared memory. Executing a task can lead to more new tasks being spawned. We consider the safety verification problem for thread-pooled programs. We parameterize the problem with two parameters: the size of the thread pool as well as the number of context switches for each task. The size of the thread pool determines the number of workers running concurrently. The number of context switches determines how many times a worker can be swapped out while executing a single task---like many verification problems for multithreaded recursive programs, the context bounding is important for decidability. We show that the safety verification problem for thread-pooled, context-bounded, Boolean programs is EXPSPACE-complete, even if the size of the thread pool and the context bound are given in binary. Our main result, the EXPSPACE upper bound, is derived using a sequence of new succinct encoding techniques of independent language-theoretic interest. In particular, we show a polynomial-time construction of downward closures of languages accepted by succinct pushdown automata as doubly succinct nondeterministic finite automata. While there are explicit doubly exponential lower bounds on the size of nondeterministic finite automata accepting the downward closure, our result shows these automata can be compressed. We show that thread pooling significantly reduces computational power: in contrast, if only the context bound is provided in binary, but there is no thread pooling, the safety verification problem becomes 3EXPSPACE-complete. Given the high complexity lower bounds of related problems involving binary parameters, the relatively low complexity of safety verification with thread-pooling comes as a surprise.

Broadcast Proxy Reencryption Based on Certificateless Public Key Cryptography for Secure Data Sharing

Broadcast proxy reencryption (BPRE), which combines broadcast encryption (BE) and proxy reencryption (PRE), is a technology used for the redistribution of data uploaded on the cloud to multiple users. BPRE reencrypts data encrypted by the distributor and then uploads it to the cloud into a ciphertext that at a later stage targets multiple recipients. As a result of this, flexible data sharing is possible for multiple recipients. However, various inefficiencies and vulnerabilities of the BE, such as the recipient anonymity problem and the key escrow problem, also creep into BPRE. Our aim in this study was to address this problem of the existing BPRE technology. The partial key verification problem that appeared in the process of solving the key escrow problem was solved, and the computational efficiency was improved by not using bilinear pairing, which requires a lot of computation time.

Formal verification of neural agents in non-deterministic environments

We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNExpTime and PSpace-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.

A rational delegating computation protocol based on reputation and smart contract

The delegating computation has become an irreversible trend, together comes the pressing need for fairness and efficiency issues. To solve this problem, we leverage game theory to propose a smart contract-based solution. First, according to the behavioral preferences of the participants, we design an incentive contract to describe the motivation of the participants. Next, to satisfy the fairness of the rational delegating computation, we propose a rational delegating computation protocol based on reputation and smart contract. More specifically, rational participants are to gain the maximum utility and reach the Nash equilibrium in the protocol. Besides, we design a reputation mechanism with a reputation certificate, which measures the reputation from multiple dimensions. The reputation is used to assure the client’s trust in the computing party to improve the efficiency of the protocol. Then, we conduct a comprehensive experiment to evaluate the proposed protocol. The simulation and analysis results show that the proposed protocol solves the complex traditional verification problem. We also conduct a feasibility study that involves implementing the contracts in Solidity and running them on the official Ethereum network. Meanwhile, we prove the fairness and correctness of the protocol.

Rational Verification for Probabilistic Systems

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).

Towards Scalable Complete Verification of Relu Neural Networks via Dependency-based Branching

We introduce an efficient method for the complete verification of ReLU-based feed-forward neural networks. The method implements branching on the ReLU states on the basis of a notion of dependency between the nodes. This results in dividing the original verification problem into a set of sub-problems whose MILP formulations require fewer integrality constraints. We evaluate the method on all of the ReLU-based fully connected networks from the first competition for neural network verification. The experimental results obtained show 145% performance gains over the present state-of-the-art in complete verification.

A Novel Rescheduling Algorithm for the Airline Recovery with Flight Priorities and Airport Capacity Constraints

Many flights experience delays at the airport due to bad weather, temporary closures of airports, unscheduled maintenance, etc., which emphasizes the urgent need for disruption management. It is widely accepted for Chinese airline companies to determine the flight timetable according to the lexicographic preference of flight priorities. Flight schedulers usually deal with the preceding flights as important as the latter flight of a higher priority. In this paper, we propose a build-in flight feasibility verification algorithm to improve the rescheduling algorithm. A novel model of the feasibility verification problem is given, which is equivalent to the model of a maximum clique problem for networks. Examples and tests show the advantage of our algorithm, and the algorithm runs fairly quickly and can be plugged in other scheduling algorithms easily.