Online services are commonly implemented with a scalable microservice architecture, where isomorphic workers process client requests, recording persistent state in a backend data store. To maintain service, modifications to service functionality must be made on the fly - i.e., as the service continues to process client requests - but doing so is challenging. The central difficulty is that of avoiding inconsistencies from mixed-mode operation, caused by workers of current and new versions interacting via the data store. Some update methods avoid mixed-mode altogether, but only at the cost of substantial inefficiency - by doubling resources (memory and compute), or by halving throughput. The alternative is an uncontrolled “rolling” update, which runs the risk of serious service failures arising from inconsistent mixed-mode behavior. Ideally, it should appear to every client that a service update takes effect atomically; this ensures that a client is not exposed to inconsistent mixed-mode behavior. In this paper, we introduce a framework that formalizes this intuition and develop foundational theory for reasoning about update consistency. We apply this theory to derive the first algorithms that guarantee consistency for mixed-mode updates. The algorithms rely on semantic properties of service actions, such as commutativity. We show that this is unavoidable, by proving that any semantically oblivious mixed-mode update method must allow inconsistencies.

Network configurations are regularly updated in response to issues such as congestion, failures, network changes, and modifications to security policies. We present a simple distributed algorithm for network update that operates on the fly and in place, and guarantees strong route-consistency. Existing methods are either weakly consistent, or do not operate in place and require excessive memory.

Abstract In multi-agent settings, such as IoT and robotics, it is necessary to coordinate the actions of independent agents in order to achieve a joint behavior. While it is often easy to specify the desired joint behavior, programming the necessary coordination can be difficult. In this work, we develop theory and methods to synthesize coordination strategies that are guaranteed not to initiate unnecessary actions. We refer to such strategies as being “compact.” We formalize the intuitive notion of compactness; show that existing methods do not guarantee compactness; and propose a solution. The solution transforms a given temporal logic specification, using automata-theoretic constructions, to incorporate a notion of minimality. The central result is that the winning strategies for the transformed specification are precisely the compact strategies for the original. One can therefore apply known synthesis methods to produce compact strategies. We report on prototype implementations that synthesize compact strategies for temporal logic specifications and for specifications of multi-robot coordination.

This paper describes Resh, a new, statically typed, interpreted programming language and associated runtime for orchestrating multirobot systems. The main features of Resh are: (1) It offloads much of the tedious work of programming such systems away from the programmer and into the language runtime; (2) It is based on a small set of temporal and locational operators; and (3) It is not restricted to specific robot types or tasks. The Resh runtime consists of three engines that collaborate to run a Resh program using the available robots in their current environment. This paper describes both Resh and its runtime and gives examples of its use.

This paper presents a method for synthesizing a reactive program to coordinate the actions of a group of other reactive programs so that the combined system satisfies a temporal specification of its desired long-term behavior. Traditionally, reactive synthesis has been applied to the construction of a stateful hardware circuit. This work is motivated by applications to other domains, such as the IoT (the Internet of Things) and robotics, where it is necessary to coordinate the actions of multiple sensors, devices, and robots to carry out a task. The mathematical model represents each agent as a process in Hoare’s CSP model. Given a network of interacting agents, called an environment , and a temporal specification of long-term behavior, the synthesis method constructs a coordinator process (if one exists) that guides the actions of the environment agents so that the combined system is deadlock-free and satisfies the given specification. The main technical challenge is that a coordinator may have only partial information of the environment state, due to non-determinism within the environment and internal environment actions that are hidden from the coordinator. This is the first method to handle both sources of partial information and to do so for arbitrary linear temporal logic specifications. It is established that the coordination synthesis problem is PSPACE -hard in the size of the environment. A prototype implementation is able to synthesize compact solutions for a number of coordination problems.

Asynchronous interactions are ubiquitous in computing systems and complicate design and programming. Automatic construction of asynchronous programs from specifications (“synthesis”) could ease the difficulty, but known methods are complex, and intractable in practice. This work develops substantially simpler synthesis methods. A direct, exponentially more compact automaton construction is formulated for the reduction of asynchronous to synchronous synthesis. Experiments with a prototype implementation of the new method demonstrate feasibility. Furthermore, it is shown that for several useful classes of temporal properties, automaton-based methods can be avoided altogether and replaced with simpler Boolean constraint solving.

Memory errors such as buffer overruns are notorious security vulnerabilities. There has been considerable interest in having a compiler to ensure the safety of compiled code either through static verification or through instrumented runtime checks. While certifying compilation has shown much promise, it has not been practical, leaving code instrumentation as the next best strategy for compilation. We term such compilers Memory Error Sanitization Compilers (MESCs). MESCs are available as part of GCC, LLVM and MSVC suites. Due to practical limitations, MESCs typically apply instrumentation indiscriminately to every memory access, and are consequently prohibitively expensive and practical to only small code bases. This work proposes a methodology that applies state-of-the-art static analysis techniques to eliminate unnecessary runtime checks, resulting in more efficient and scalable defenses. The methodology was implemented on LLVM's Safecode, Integer Overflow, and Address Sanitizer passes, using static analysis of Frama-C and Codesurfer. The benchmarks demonstrate an improvement in runtime performance that makes incorporation of runtime checks a viable option for defenses.

We show that existing methods for primary-backup replication may disrupt the timing behavior of an underlying service to the extent of making it unusable. We prove that the problem is inherent to the primary-backup model.

Locks are used to ensure exclusive access to shared memory locations. Unfortunately, lock operations are expensive, so much work has been done on optimizing their performance for common access patterns. One such pattern is found in networking applications, where there is a single thread dominating lock accesses. An important special case arises when a single-threaded program calls a thread-safe library that uses locks.

The rule language of an Intrusion Detection System (IDS) plays a critical role in its effectiveness. A rule language must be expressive, in order to describe attack patterns as precisely as possible. It must also allow for a matching algorithm with predictable and low complexity, in order to ensure robustness against denial-of-service attacks. Unfortunately, these requirements often conflict. We show, for instance, that a single rule, when coupled with a backtracking matching algorithm, can bring the processing rate down to nearly ONE packet per second. Performance vulnerabilities of this type are known for patterns described using regular expressions, and can be avoided by using a deterministic matching algorithm. Increasingly, however, rules are being written using the more powerful regex syntax, which includes non-regular features such as back-references. The matching algorithm for general regex's is based on backtracking, and is thus vulnerable to attacks. The main contribution of this paper is a deterministic algorithm for the full regex syntax, which builds upon the deterministic algorithm for regular expressions. We provide a (rough) complexity bound on the worst-case performance, and show that this bound can be tightened through compile-time analysis of the regex structure. These bounds can be used as an admissibility check, to isolate expressions that require further analysis. Finally, we present an implementation of these algorithms in the context of the Snort IDS, and experimental results on several packet traces which show substantial improvement over the backtracking algorithm.

Hardware systems and reactive software systems can be described as the composition of several concurrently active processes. Automated reasoning based on model checking algorithms can substantially increase confidence in the overall reliability of a system. Direct methods for model checking a concurrent composition, however, usually suffer from the explosion in the number of program states that arises from concurrency. Reasoning compositionally about individual processes helps mitigate this problem. A number of rules have been proposed for compositional reasoning, typically based on an assume-guarantee reasoning paradigm. Reasoning with these rules can be delicate, as some are syntactically circular in nature, in that assumptions and guarantees are mutually dependent. This is known to be a source of unsoundness. In this article, we investigate rules for compositional reasoning from the viewpoint of completeness . We show that several rules are incomplete: that is, there are properties whose validity cannot be established using (only) these rules. We derive a new, circular, reasoning rule and show it to be sound and complete. We show that the auxiliary assertions needed for completeness need be defined only on the interface of the component processes. We also show that the two main paradigms of circular and noncircular reasoning are closely related, in that a proof of one type can be transformed in a straightforward manner to one of the other type. These results give some insight into the applicability of compositional reasoning methods.

Abstraction is often essential to verify a program with model checking. Typically, a concrete source program with an infinite (or finite, but large) state space is reduced to a small, finite state, abstract program on which a correctness property can be checked. The fundamental question we investigate in this paper is whether such a reduction to finite state programs is always possible, for arbitrary branching time temporal properties. We begin by showing that existing abstraction frameworks are inherently incomplete for verifying purely existential or mixed universal-existential properties. We then propose a new, complete abstraction framework which is based on a class of focused transition systems (FTS's). The key new feature in FTS's is a way of "focusing" an abstract state to a set of more precise abstract states. While focus operators have been defined for specific contexts, this result shows their fundamental usefulness for proving non-universal properties. The constructive completeness proof provides linear size maximal models for properties expressed in logics such as CTL and the mu-calculus. This substantially improves upon known (worst-case) exponential size constructions for their universal fragments.

Large software systems, especially in the telecommunications field, are often specified as a collection of features. We present a formal specification language for describing features, and a method of automatically detecting conflicts ("undesirable interactions") amongst features at the specification stage. Conflict detection at this early stage can help prevent costly and time consuming problem fixes during implementation. Features are specified using temporal logic; two features conflict essentially if their specifications are mutually inconsistent under axioms about the underlying system behavior. We show how this inconsistency check may be performed automatically with existing model checking tools. In addition, the model checking tools can be used to provide witness scenarios, both when two features conflict as well as when the features are mutually consistent. Both types of witnesses are useful for refining the specifications. We have implemented a conflict detection tool, FIX (Feature Interaction eXtractor), which uses the model checker COSPAN for the inconsistency check. We describe our experience in applying this tool to a collection of telecommunications feature specifications obtained from the Telcordia (Bellcore) standards. Using FIX, we were able to detect most known interactions and some new ones, fully automatically, in a few hours processing time.

In this paper we outline a theory for the environment-modeling problem , the problem of abstracting component finite state machines (FSMs)bordering a particular FSM of interest within a network of interacting FSMs. The goal is to lay a theoretical foundation for the automatic state reduction of large FSM networks. We feel this is a prerequisite for the efficient use of many verification techniques. We focus on computing conditions for the safe removal of a component FSM in a FSM network, where removal is safe if it preserves a certain well-defined trace equivalence. We present an optimized algorithm for determining language universality of a FSM, as well as determining independence of a FSM from those of its inputs connected to outputs of neighboring FSMs. These two properties, input independence and language universality, provide the necessary and sufficient conditions for safe removal. In addition, we show how simulation relations can be utilized, both to reduce the cost of computing safe removal and to create an appropriate abstract FSM when safe removal is not possible.

We demonstrate that many known algorithms for model checking infinite-state systems can be derived uniformly from a reachability procedure that generates a "covering graph", a generalization of the Karp-Miller graph for Petri Nets. Each node of the covering graph has an associated non-empty set of reachable states, which makes it possible to model check safety properties of the system on the covering graph. For systems with a well-quasi-ordered simulation relation, each infinite fair computation has a finite witness, which may be detected using the covering graph and combinatorial properties of the specific infinite state system. These results explain many known decidability results in a simple, uniform manner. This is a strong indication that the covering graph construction is appropriate for the analysis of infinite state systems. We also consider the new application domain of parameterized broadcast protocols, and indicate how to apply the construction in this domain. This application is illustrated on an invalidation-based cache coherency protocol, for which many safety properties can be proved fully automatically for an arbitrary number of processes.

The ring is a useful means of structuring concurrent processes. Processes communicate by passing a token in a fixed direction; the process that possesses the token is allowed to make certain moves. Usually, correctness properties are expected to hold irrespective of the size of the ring. We show that the problem of checking many useful correctness properties for rings of all sizes can be reduced to checking them on a ring of small size. The results do not depend on the processes being finite state. We illustrate our results on examples.