Lattice-linearity was introduced as modelling problems using predicates that induce a lattice among the global states (Garg, SPAA 2020). Such modelling enables permitting asynchronous execution in multiprocessor systems. A key property of the predicate representing such problems is that it induces one lattice in the state space. Such representation guarantees the execution to be correct even if nodes execute asynchronously. However, many interesting problems do not exhibit lattice-linearity. This issue was alleviated with the introduction of eventually lattice-linear algorithms (Gupta and Kulkarni, SSS 2021). They induce single or multiple lattices in a subset of the state space even when the problem cannot be defined by a predicate under which the states form a lattice. In this paper, we focus on analyzing and differentiating between lattice-linear problems and algorithms. We introduce a new class of algorithms called fully lattice-linear algorithms. These algorithms partition the entire reachable state space into one or more lattices. For illustration, we present lattice-linear self-stabilizing algorithms for minimal dominating set (MDS) and graph colouring (GC) problems, and a parallel processing lattice-linear 2-approximation algorithm for vertex cover (VC). The algorithms for MDS and GC converge in$n$moves and$n+2m$moves respectively. These algorithms preserve this time complexity while allowing the nodes to execute asynchronously, where these nodes may execute based on old or inconsistent information about their neighbours. The algorithm for VC is the first lattice-linear approximation algorithm for an NP-Hard problem; it converges in$n$moves.

In this paper, we evaluate and compare the performance of two approaches, namely self-stabilization and rollback, to handling consistency violating faults (cυf) that occur when a self-stabilizing distributed graph-based program is executed on an eventually consistent key-value store. Consistency violating faults are caused by reading wrong values due to weaker level of consistency provided by the key-value store. One way to deal with these faults is to utilize rollback whereas another way is to rely on the property of self-stabilization that is expected to provide recovery from arbitrary states. We evaluate both these approaches in different case studies -planar graph coloring, arbitrary graph coloring, and maximal matching-as well as for different problem dimensions such as input data characteristics, workload partition, and network latency. We also consider the effect of executing non-stabilizing algorithm with rollback with a similar stabilizing algorithm that does not utilize rollback.

Monitoring distributed systems to ensure their correctness is a challenging and expensive but essential problem. It is challenging because while execution of a distributed system creates a partial order among events, the monitor will typically observe only one serialization of that partial order. This means that even if the observed serialization is consistent with the system specifications, the monitor cannot assume that the system is correct because some other unobserved serialization can be inconsistent with the system specifications. Existing solutions that guarantee identification of all such unobserved violations require some combination of lots of time and large clocks, e.g. O(n) sized Vector Clocks.We present a new, efficient two-layered monitoring approach that overcomes both the time and space limitations of earlier monitors. The first layer is imprecise but efficient and the second layer is precise but (relatively) inefficient. We show that the combination of these two layers reduces the cost of monitoring by 85-95%. Furthermore, the two-layered monitor permits the use of O(1) sized Hybrid Logical Clocks.

Retroscope is a comprehensive lightweight distributed monitoring tool that enables users to query and reconstruct past consistent global states of the system. Retroscope achieves this by augmenting the system with Hybrid Logical Clocks (HLC) and by streaming HLC-stamped event logs for storage and processing; these HLC timestamps are then used for constructing global (or nonlocal) snapshots upon request. Retroscope provides a rich querying language (RQL) to facilitate searching for global predicates across past consistent states. The search is performed by advancing through global states in small incremental steps, greatly reducing the amount of computation needed to construct consistent states. The Retroscope search algorithm is embarrassingly-parallel and can employ many worker processes (each processing up to 150,000 consistent snapshots per second) to handle a single query. We evaluate Retroscope's monitoring capabilities in two case studies: Chord and Apache ZooKeeper.

We present our framework DKVF that enables one to quickly prototype and evaluate new consistency protocols for key-value stores. DKVF is designed based on the separation of concerns in creating distributed data stores. This separation of concerns allows the designers of consistency protocols to only focus on the high-level consistency protocols which gives them the opportunity to quickly deploy a consistency protocol and evaluate its performance. Moreover, the loose coupling of the different components allows us to easily change different components (e.g. storage engine) of an implementation. We demonstrate DKVF by implementing four existing protocols --eventual consistency, COPS, GentleRain and CausalSpartan-- with it. The implementation of these protocols was very convenient with DKVF, as it only required to write a piece of code for the consistency component that is very close to the pseudocode of the original papers. Hence, it was possible to achieve this in just 1-2 days per protocol. DKVF also comes with a toolset that facilitates running clusters and performing experiments. Tutorial video: https://www.youtube.com/watch?v=MFJQzsJkwfc&list=PLErtSVEHsnBJvoQQI6iqGn61oNrUVVuST

Broadcast authentication is an important problem in several network settings such as wireless sensor networks and ad-hoc networks. We focus on the problem of independent key distribution protocols, which use efficient symmetric key signatures in distributed systems to permit (local) broadcast authentication. We focus on five types of communication graphs: (1) star, (2) acyclic, (3) planar, (4) complete bipartite, and (5) fully connected graphs. A star graph is the simplest network topology where a central node is transmitting authenticated broadcast messages to several satellite nodes. For star graphs, we show that as n, the number of satellite nodes in the star network, tends to infinity, it suffices to maintain logn+1/2loglogn + 1 keys at the center node, but logn+1/2loglogn keys do not suffice. We establish that this is the optimal lower bound on the number of keys for a star graph. Building on this result, we describe storage efficient key distribution for acyclic, planar, and complete bipartite graphs, when compared to existing key distribution schemes. We extend our scheme for fully connected graphs and show that it is sufficient to store O(c log2 N) keys per node where c<1. We perform a detailed analysis of collusion resistance of our protocols and show the trade-offs against internal and external attacks depending on the size of storage. Finally, we demonstrate the practical applicability of our protocols for wireless sensor networks.

Solutions to most practical numerical optimization problems must be evaluated for their performance over a number of different loading or operating conditions, which we refer here as scenarios. Therefore, a meaningful and resilient optimal solution must be such that it remains feasible under all scenarios and performs close to an individual optimal solution corresponding to each scenario. Despite its practical importance, multiscenario consideration has received a lukewarm attention, particularly in the context of multiobjective optimization. The usual practice is to optimize for the worst-case scenario. In this paper, we review existing methodologies in this direction and set our goal to suggest a new and potential population-based method for handling multiple scenarios by defining scenario-wise domination principle and scenario-wise diversity-preserving operators. To evaluate, the proposed method is applied to a number of numerical test problems and engineering design problems with a detail explanation of the obtained results and compared with an existing method. This first systematic evolutionary-based multiscenario, multiobjective optimization study on numerical problems indicates that multiple scenarios can be handled in an integrated manner using an evolutionary multiobjective optimization framework to find a well-balanced compromise set of solutions to multiple scenarios and maintain a tradeoff among multiple objectives. In comparison to an existing serial multiple optimization approach, the proposed approach finds a set of compromised tradeoff solutions simultaneously. An achievement of multiobjective tradeoff and multiscenario tradeoff is algorithmically challenging, but due to its practical appeal, further research and application must be spent.

Hybrid vector clock(s) (HVC) provide a mechanism to combine the theory and practice of distributed systems. Improving on traditional vector clock(s) (VC), HVC utilizes synchronized physical clocks to reduce the size by focusing only on causality where the physical time associated with two events is within a given uncertainty window ε and letting physical clock alone determine the order of events that are outside the uncertainty window. In this paper, we develop a model for determining the bounds on the size of HVC. Our model uses four parameters, ε: uncertainty window, 8: message delay, a: communication frequency and n: number of nodes in the system. We derive the size of HVC in terms of a delay differential equation, and show that the size predicted by our model is almost identical to the results obtained by simulation. We also identify closed form solutions that provide tight lower and upper bounds for useful special cases. We show that for many practical applications and deployment environments in Amazon EC2, the size of HVC remains only as a couple entries and substantially less than n. Finally, although the analytical results rely on a specific communication pattern they are useful in evaluating size of HVC in different communication scenarios.

In order to take a consistent snapshot of a distributed system, it is necessary to collate and align local logs from each node to construct a pairwise concurrent cut. By leveraging NTP synchronized clocks, and augmenting them with logical clock causality information, Retroscope provides a lightweight solution for taking unplanned retrospective snapshots of past distributed system states. Instead of storing a multiversion copy of the entire system data, this is achieved efficiently by maintaining a configurable-size sliding window-log at each node to capture recent operations. In addition to retrospective snapshots, Retroscope also provides incremental and rolling snapshots that utilize an existing snapshot to reduce the cost of constructing a new snapshot in proximity. This capability is useful for performing stepwise debugging and root-cause analysis, and supporting data integrity monitoring and checkpoint-recovery. We implement Retroscope for the Voldemort distributed datastore and evaluate its performance under varying workloads.

Practical algorithms for determining causality by assigning timestamps to events have focused on online algorithms, where a permanent timestamp is assigned to an event as soon as it is created. We address the problem of reducing size of the timestamp by utilizing the underlying topology (which is often not fully connected since not all processes talk to each other) and deferring the assignment of a timestamp to an event for a suitably chosen period of time after the event occurs. Specifically, we focus on inline timestamps, which are a generalization of offline timestamps that are assigned after the computation terminates. We show that for a graph with vertex cover VC, it is possible to assign inline timestamps which contains only 2|VC|+2 elements.

Causal consistency is an intermediate consistency model that can be achieved together with high availability and high-performance requirements even in presence of network partitions. In the context of partitioned data stores, it has been shown that implicit dependency tracking using clocks is more efficient than explicit dependency tracking by sending dependency check messages. Existing clock-based solutions depend on monotonic psychical clocks that are closely synchronized. These requirements make current protocols vulnerable to clock anomalies. In this paper, we propose a new clock-based algorithm, CausalSpartan, that instead of physical clocks, utilizes Hybrid Logical Clocks (HLCs). We show that using HLCs, without any overhead, we make the system robust on physical clock anomalies. This improvement is more significant in the context of query amplification, where a single query results in multiple GET/PUT operations. We also show that CausalSpartan decreases the visibility latency for a given data item comparing to existing clock-based approaches. In turn, this reduces the completion time of collaborative applications where two clients accessing two different replicas edit same items of the data store. Like previous protocols, CausalSpartan assumes that a given client does not access more than one replica. We show that in presence of network partitions, this assumption (made in several other works) is essential if one were to provide causal consistency as well as immediate availability to local updates.

We focus on protocols for auditable restoration of distributed systems. The need for such protocols arises due to conflicting requirements (e.g., access to the system should be restricted but emergency access should be provided). One can design such systems with a tamper detection approach (based on the intuition of In-case-of-emergency-break-glass). However, in a distributed system, such tampering, which are denoted as auditable events, is visible only for a single node. This is unacceptable since the actions they take in these situations can be different than those in the normal mode. Moreover, eventually, the auditable event needs to be cleared so that system resumes the normal operation. With this motivation, in this paper, we present two protocols for auditable restoration, where any process can potentially identify an auditable event. The first protocol has an unbounded state space while the second protocol uses bounded state space that does not increase with the length of the computation. In both protocols, whenever a new auditable event occurs, the system must reach an auditable state where every process is aware of the auditable event. Only after the system reaches an auditable state, it can begin the operation of restoration. Although any process can observe an auditable event, we require that only authorized processes can begin the task of restoration. Moreover, these processes can begin the restoration only when the system is in an auditable state. Our protocols are self-stabilizing and can effectively handle the case where faults or auditable events occur during the restoration protocol. Moreover, they can be used to provide auditable restoration to other distributed protocols.

In this paper, we evaluate the effectiveness of model slicing to provide assurance about correctness of SystemC TLM programs. The need for such assurance is important since SystemC has become a de-facto standard for building systems with hardware/software co-design. Existing approaches that enable one to transform the given SystemC TLM program into an UPPAAL model that can be verified suffer from models that result in state space explosion. This problem becomes even more complex when verifying fault-tolerance. Model slicing has the potential to provide a solution to this problem. Therefore, we focus on developing a model slicer that extends existing work on model slicing and combines it with tools to generate UPPAAL models from SystemC TLM programs and tools to add the impact of faults to those UPPAAL models. The experimental results show that with the proposed framework, the designer is capable of verifying even very complex SystemC TLM models, which would have been impossible without the proposed approach.

We focus on the issue of realizability constraints in the context of model repair. Model repair focuses on revising a given program to satisfy new properties of interest while satisfying existing properties such as fault-tolerance. An important difficulty in using model repair is that the repaired model must be realizable in the constraints given by the underlying system. It is well-known that these realizability constraints cause an increase in the complexity of model repair (e.g., from P to NP-complete). Hence, existing approaches for adding fault-tolerance to distributed program focuses on cautious repair where in every step, the model being repaired satisfies the realizability constraints. They also utilize heuristics to reduce the complexity of repair. In this work, we focus on using lazy repair while adding fault-tolerance. Specifically, in this work, we utilize a two-step approach. The first step ignores the realizability constraints and performs model repair to add fault-tolerance. This ensures that the resulting program satisfies the desired property of interest (namely, fault-tolerance) although it may not be realizable. The second step attempts to revise this program to ensure that realizability constraints are satisfied without creating new program behaviors. This ensures that the resulting program satisfies both the properties of interest and realizability constraints. We demonstrate that this approach is more efficient than the cautious repair algorithm in the literature. We also note that inherently the lazy repair approach is also applicable in other contexts such as synchronous systems, cyber-physical systems, etc.

In this paper, we present the paradigm of collaborative stabilization that focuses on providing stabilization in the presence of an essential but potentially disruptive environment. By essential, we mean that without the environment actions, stabilization property would be impossible. At the same time, environment actions are not in the control of the program and can be disruptive to the recovery. We demonstrate the need for collaborative stabilization by providing examples where existing paradigms of stabilization are undesirable/insufficient. We compare collaborative stabilization with existing paradigms of stabilization. We identify the complexity of verifying collaborative stabilizing programs and develop theorems that focus on composition of such programs.

Most designs in practice go through a number of different loading or operating conditions. Therefore, a meaningful and resilient design must be such that it performs well under all such scenarios. Despite its practical importance, multi-scenario consideration has not been paid much attention in multi-objective optimization literature. In this paper, we address this challenging issue by suggesting an aggregate based handling of multiple scenarios and contrasts the proposed approach against a recently suggested approach which involves running multi-objective optimization multiple times and a rigid decision-making method. The proposed method is applied to two numerical test problems and two engineering design problems. This first evolutionary based multi-scenario, multi-objective optimization study should spur further interests among EMO researchers.

In most applications using genetic programming (GP), objective functions are obtained by a terminating calculation. However, the terminating calculation cannot evaluate distributed fault-tolerant programs accurately. A key distinction in synthesizing distributed fault-tolerant programs is that they are inherently non-deterministic, potentially having infinite computations and executing in an unpredictable environment. In this study, we apply a model checking technique - Binary Decision Diagrams (BDDs) - to GP, evaluating distributed programs by computing reachable states of the given program and identifying whether it satisfies its specification. We present scenario-based multi-objective approach that each program is evaluated under different scenarios which represent various environments. The computation of the programs are considered in two different semantics respectively: interleaving and maximum-parallelism. In the end, we illustrate our approach with a Byzantine agreement problem, a token ring problem and a consensus protocol using failure detector S. For the first time, this work automatically synthesizes the consensus protocol with S. The results show the proposed method enhances the effectiveness of GP in all studied cases when using maximum-parallelism semantic.

In this paper, we focus on revising a given program so that the average recovery time in the presence of an adversarial scheduler is bounded by a given threshold lambda. Specifically, we consider the scenario where the fault (or other unexpected action) perturbs the program to a state that is outside its set of legitimate states. Starting from this state, the program executes its actions/transitions to recover to legitimate states. However, the adversarial scheduler can force the program to reach one illegitimate state that requires a longer recovery time. To ensure that the average recovery time is less than lambda, we need to remove certain transitions/behaviors. We show that achieving this average response time while removing minimum transitions is NP-hard. In other words, there is a tradeoff between the time taken to synthesize the program and the transitions preserved to reduce the average convergence time. We present six different heuristics and evaluate this tradeoff with case studies. Finally, we note that the average convergence time considered here requires formalization of hyperproperties. Hence, this work also demonstrates feasibility of adding (certain) hyperproperties to an existing program.

Hybrid vector clocks (HVC) implement vector clocks (VC) in a space-efficient manner by exploiting the availability of loosely-synchronized physical clocks at each node. In this paper, we develop a model for determining the bounds on the size of HVC. Our model uses four parameters, epsilon: uncertainty window, delta: minimum message delay, alpha: communication frequency and n: number of nodes in the system. We derive the size of HVC in terms of a differential equation, and show that the size predicted by our model is almost identical to the results obtained by simulation. We also identify closed form solutions that provide tight lower and upper bounds for useful special cases. Our model and simulations show the HVC size is a sigmoid function with respect to increasing epsilon; it has a slow start but it grows exponentially after a phase transition. We present equations to identify the phase transition point and show that for many practical applications and deployment environments, the size of HVC remains only as a couple entries and substantially less than n. We also find that, in a model with random unicast message transmissions, increasing n actually helps for reducing HVC size.

We focus on a protocol for auditable restoration of distributed systems. The need for such protocol arises due to conflicting requirements (e.g., access to the system should be restricted but emergency access should be provided). One can design such systems with a tamper detection approach (based on the intuition of "break the glass door"). However, in a distributed system, such tampering, which are denoted as auditable events, is visible only for a single node. This is unacceptable since the actions they take in these situations can be different than those in the normal mode. Moreover, eventually, the auditable event needs to be cleared so that system resumes the normal operation. With this motivation, in this paper, we present a protocol for auditable restoration, where any process can potentially identify an auditable event. Whenever a new auditable event occurs, the system must reach an "auditable state" where every process is aware of the auditable event. Only after the system reaches an auditable state, it can begin the operation of restoration. Although any process can observe an auditable event, we require that only "authorized" processes can begin the task of restoration. Moreover, these processes can begin the restoration only when the system is in an auditable state. Our protocol is self-stabilizing and can effectively handle the case where faults or auditable events occur during the restoration protocol. Moreover, it can be used to provide auditable restoration to other distributed protocol.

Abstract We focus on synthesis techniques for transforming existing fault-intolerant real-time programs into fault-tolerant programs that provide phased recovery . A fault-tolerant program is one that satisfies its safety and liveness specifications as well as timing constraints in the presence of faults. We argue that in many commonly considered programs (especially in safety/mission-critical systems), when faults occur, simple recovery to the program’s normal behavior is necessary, but not sufficient. For such programs, it is necessary that recovery is accomplished in a sequence of phases, each ensuring that the program satisfies certain properties. In the simplest case, in the first phase the program recovers to an acceptable behavior within some time θ , and, in the second phase, it recovers to the ideal behavior within time δ . In this article, we introduce four different types of bounded-time 2-phase recovery, namely ordered-strict, strict, relaxed, and graceful, based on how a real-time fault-tolerant program reaches the acceptable and ideal behaviors in the presence of faults. We rigorously analyze the complexity of automated synthesis of each type: we either show that the problem is hard in some class of complexity or we present a sound and complete synthesis algorithm. We argue that such complexity analysis is essential to deal with the highly complex decision procedures of program synthesis.

In this paper, we address solution methodologies of an optimization problem under multiple scenarios. Often in practice, a problem needs to be considered for different scenarios, such as evaluating for different loading conditions, different blocks of data, multi-stage operations, etc. After reviewing various single-objective aggregate methods for handling objectives and constraints under multiple scenarios, we then suggest a multi-objective optimization approach for solving multi-scenario optimization problems. On a Byzantine agreement problem, we demonstrate the usefulness of the proposed multi-objective approach and explain the reasons for their superior behavior. The suggested procedure is generic and now awaits further applications to more challenging problems from engineering and computational fields.

Deadlock-freedom is a major challenge in developing multi-threaded programs, as a deadlock cannot be resolved until one restarts the program (mostly by using manual intervention). To avoid the risk of blocking, a program may use the trylock operations rather than lock operations. In this case, if a thread fails to acquire a lock using trylock, since trylock is non-blocking, the thread can release acquired locks to avoid a deadlock after trylock returns. Although this approach avoids deadlocks, it may also introduce bugs such as livelock and deadlivelock. Moreover, when such bugs are identified in a program, revising the program manually is error-prone.

We focus on the problem of adding multitolerance to an existing fault-intolerant program. A multitolerant program tolerates multiple classes of faults and provides a potentially different level of fault tolerance to each of them. We consider three levels of fault tolerance, namely failsafe (i.e., satisfy safety in the presence of faults), nonmasking (i.e., recover to legitimate states after the occurrence of faults), and masking (both). For the case where the program is subject to two classes of faults, we consider six categories of multitolerant programs—FF, FN, FM, MM, MN, and NN, where F, N, and M represent failsafe, nonmasking, and masking levels of tolerance provided to each class of fault. We show that the problem of adding FF, NN, and MN multitolerance can be solved in polynomial time (in the state space of the program). However, the problem is NP-complete for adding FN, MM, and FM multitolerance. We note that the hardness of adding MM and FM multitolerance is especially atypical given that MM and FM multitolerance can be added efficiently under more restricted scenarios where multiple faults occur simultaneously in the same computation. We also present heuristics for managing the complexity of MM multitolerance. Finally, we present real-world multitolerant programs and discuss the trade-off involved in design decisions while developing such programs.

We focus on the problem of multi-graceful degradation. In multi-graceful degradation, the system provides successively reduced guarantees in the presence of increasingly severe faults. We present an automated technique for generation of a multi-graceful-degraded program from its original fault-intolerant/ideal version. In this algorithm, we begin with (1) an ideal program that satisfies all its specification in the absence of faults, (2) a set of faults that need to be tolerated and (3) reduced requirements in their presence. We subsequently generate several gracefullly degrading programs that only satisfy the reduced requirements. This step also identifies new states to which program needs to recover to satisfy the reduced specification. Subsequently, we utilize the original input program and the generated programs that ensures that (1) in the absence of faults, the entire specification is satisfied and (2) in the presence of faults, the program recovers to states from where the corresponding reduced specification is satisfied. We illustrate our technique with a case study of a system in the fuelcell lab of the Ohio Coal Research Center (OCRC). In this system, it is important to satisfy safety of lab personnel as well as safety of people in the building in which it is located. Moreover, in case of device failures, it is necessary to provide weaker guarantees that capture the best possible protection. In our example, we begin with an ideal model for this system and successively add multi-graceful degradation to obtain the same program (with some abstractions) as the one that was designed manually for this system.

Concurrent execution is a big challenge for distributed systems programming and cloud computing. Using locks is the most common technique for developing distributed applications that require tight synchronization. Unfortunately, locking is manual, error-prone, and unscalable. To address this issue, we propose a scalable automated locking framework called Maestro. Maestro consists of a master and several workers, which can be dynamically instantiated on demand. Maestro examines the program actions of the workers before deployment and automatically decides which worker actions can be executed locally (without contacting the master) and which actions require synchronization through the master. Maestro has applications in graph processing, real-time enterprise analysis, and web-services domains. By enabling the developers to write code at a higher-level of abstraction (shared-memory), Maestro improves productivity and lowers the cost of entry to cloud computing backend development.

Traditionally, (nonmasking and masking) fault tolerance has focused on ensuring that after the occurrence of faults, the program recovers to states from where it continues to satisfy its original specification. However, a problem with this limited notion is that, in some cases, it may be impossible to recover to states from where the entire original specification is satisfied. For this reason, one can consider a fault-tolerant graceful-degradation program that ensures that upon the occurrence of faults, the program recovers to states from where a (given) subset of its specification is satisfied. Typically, the subset of specification satisfied thus would be the critical requirements. In this paper, we focus on automatically revising a given program to obtain a corresponding graceful program, i.e., a program that satisfies a weaker specification. Specifically, this step involves adding new behaviors that satisfy the given subset of specification. Moreover, it ensures that during this process, it does not remove any behavior from the original program. With this motivation, in this paper, we focus on automatic derivation of the graceful program, i.e., a program that contains all behaviors of the original program and some new behaviors that satisfy the weaker conditions. We note that this aspect differentiates this work from previous work on controller synthesis as well as automated addition of fault tolerance in that this work requires that no new behaviors are added in the absence of faults.

In this paper, we concentrate on automated synthesis of fault recovery mechanism for fault-intolerant component-based models that encompass a cyber-physical system. We define the notion of fault recovery for cyber-physical component-based models. We also present synthesis constraints that preserve the correctness and cyber-physical nature of a given fault-intolerant model under which recovery can be added. We show that the corresponding synthesis problem is NP-complete and consequently introduce symbolic heuristics to tackle the exponential complexity. Our experimental results validate effectiveness of our heuristics for relatively large models.

In this paper, we focus on trade-offs between storage cost and rekeying cost for secure multicast. Membership in secure multicast groups is dynamic and requires multiple updates in a single time frame. We present a family of algorithms that provide a trade-off between the number of keys maintained by users and the time required for rekeying due to revocation of multiple users. We show that some well-known algorithms in the literature are members of this family. We show that algorithms in this family can be used to reduce the cost of rekeying by 43-79 percent when compared with previous solutions while keeping the number of keys manageable. We also describe a scheme to reduce the number of secrets further when revocations are periodic. Furthermore, we describe techniques to provide preferential treatment for long standing members of the group without affecting the performance of the algorithms. Using our techniques, as the group size increases, long standing members need to store smaller number of keys than short-lived members. This property is useful for adapting to the variable storage requirements of users in current day heterogeneous networks.

The complexity of designing programs that simultaneously tolerate multiple classes of faults, called multitolerant programs, is in part due to the conflicting nature of the fault tolerance requirements that must be met by a multitolerant program when different types of faults occur. To facilitate the design of multitolerant programs, we present sound and (deterministically) complete algorithms for stepwise design of two families of multitolerant programs in a high atomicity program model, where a process can read and write all program variables in an atomic step. We illustrate that if one needs to design failsafe (respectively, nonmasking) fault tolerance for one class of faults and masking fault tolerance for another class of faults, then a multitolerant program can be designed in separate polynomial-time (in the state space of the fault-intolerant program) steps regardless of the order of addition. This result has a significant methodological implication in that designers need not be concerned about unknown fault tolerance requirements that may arise due to unanticipated types of faults. Further, we illustrate that if one needs to design failsafe fault tolerance for one class of faults and nonmasking fault tolerance for a different class of faults, then the resulting problem is NP-complete in program state space. This is a counterintuitive result in that designing failsafe and nonmasking fault tolerance for the same class of faults can be done in polynomial time. We also present sufficient conditions for polynomial-time design of failsafe-nonmasking multitolerance. Finally, we demonstrate the stepwise design of multitolerance for a stable disk storage system, a token ring network protocol and a repetitive agreement protocol that tolerates Byzantine and transient faults. Our automatic approach decreases the design time from days to a few hours for the token ring program that is our largest example with 200 million reachable states and 8 processes.

The Border Gateway Protocol (BGP) is the de facto interdomain routing protocol that connects autonomous systems (ASes). Despite its importance for the Internet infrastructure, BGP is vulnerable to a variety of attacks due to lack of security mechanisms in place. Many BGP security mechanisms have been proposed. However, none of them has been deployed because of either high cost or high complexity. The right trade-off between efficiency and security has been ever challenging. In this paper, we attempt to trade-off between efficiency and security by giving a little dose of trust to BGP routers. We present a new flexible threat model that assumes for any path of length h, at least one BGP router is trustworthy, where h is a parameter that can be tuned according to security requirements. Based on this threat model, we present two new symmetric key approaches to securing BGP: the centralized key distribution approach and the distributed key distribution approach. Comparing our approaches to the previous SBGP scheme, our centralized approach has a 98 percent improvement in signature verification. Our distributed approach has equivalent signature generation cost as in SBGP and an improvement of 98 percent in]signature verification. Comparing our approaches to the previous SPV scheme, our centralized approach has a 42 percent improvement in signature generation and a 96 percent improvement in signature verification. Our distributed approach has a 90 percent improvement on signature generation cost and a 95 percent improvement in signature verification cost. We also describe practical techniques for increasing the long-term security and collusion resistance of our key distribution protocols without increasing the signature generation and verification costs. By combining our approaches with previous public key approaches, it is possible to simultaneously provide an increased level of security and reduced computation cost.

In this paper, we classify multitolerant systems, i.e., systems that tolerate multiple classes of faults and provide potentially different levels of tolerance to them in terms of strong and weak multitolerance. Intuitively, this classification is based upon the guarantees provided by the program when one class of faults occurs while it is recovering from another class of faults. We focus on automated synthesis of weak multitolerant programs. Such weak multitolerance becomes necessary when it is impossible to provide strong multitolerance and/or when the probability of one class of faults occurring while the program is 'recovering' from a fault from another class is negligible. By considering the levels of fault-tolerance provided to each class of faults, we evaluate five possible combinations for weak multitolerance. We find a counterintuitive result that if masking fault-tolerance is desired for one class of faults and masking (or failsafe) fault-tolerance is desired for another class of faults then the problem is NP-hard. This result is surprising since the corresponding problem for strong multitolerance can be solved in polynomial time. Also, we show that the problem of synthesizing weak multitolerance for other combinations is in P. More broadly, this result demonstrates the role of assumptions, e.g., independence of occurrences of faults from different classes, in the complexity of automated synthesis.

A hard-masking real-time program is one that satisfies safety (including timing constraints) and liveness properties in the absence and presence of faults. It has been shown that any hard-masking program can be decomposed into a fault-intolerant version and a set of fault-tolerance components known as detectors and delta-correctors. In this paper, we introduce a set of sufficient conditions for interference-freedom among fault-tolerance components and real-time programs. We demonstrate that such conditions elegantly enable us to compositionally verify the correctness of hard-masking programs. Preliminary model checking experiments show very encouraging results in both achieving speedups and reducing memory usage in verification of embedded systems.

Recently, wireless sensor networks (WSNs) have become increasingly available for data-intensive applications such as micro-climate monitoring, precision agriculture, and audio/video surveillance. A key challenge faced by data-intensive WSNs is to transmit the sheer amount of data generated within an application's lifetime to the base station despite the fact that sensor nodes have limited power supplies such as batteries or small solar panels. In this paper, we propose to use low-cost disposable mobile relays to reduce the energy consumption of data-intensive WSNs. Different from previous work, our approach does not require complex motion planning of mobile nodes, and hence can be implemented on a number of low-cost mobile sensor platforms. Moreover, we integrate the energy consumption due to both mobility and wireless transmissions into a holistic optimization framework. The optimal relay configuration is shown to depend on both the positions of nodes and the amount of data to be sent. We develop two algorithms that iteratively refine the configuration of mobile relays and converge to the optimal solution. These algorithms have efficient distributed implementations that do not require explicit synchronization. Our simulation results based on realistic energy models obtained from existing mobile and static sensor platforms show that our algorithms significantly outperform the best existing solutions.

We focus on constraint based automated addition of nonmasking and stabilizing fault-tolerance to hierarchical programs. We specify legitimate states of the program in terms of constraints that should be satisfied in those states. To deal with faults that may violate these constraints, we add recovery actions while ensuring interference freedom among the recovery actions added for satisfying different constraints. Since the constraint based manual design of fault tolerance is well known to be applicable in the manual design of nonmasking fault tolerance, we expect our approach to have a significant benefit in automation of fault tolerant programs. We illustrate our algorithms with three case studies: stabilizing mutual exclusion, stabilizing diffusing computation, and a data dissemination problem in sensor networks. With experimental results,we show that the complexity of synthesis is reasonable and that it can be reduced using the structure of the hierarchical systems. To our knowledge, this is the first instance where automated synthesis has been successfully used in synthesizing programs that are correct under fairness assumptions. Moreover, in two of the case studies considered in this paper, the structure of the recovery paths is too complex to permit existing heuristic based approaches for adding recovery.

We concentrate on automatic revision of untimed and real-time programs with respect to UNITY properties. The main focus of this article is to identify instances where addition of UNITY properties can be achieved efficiently (in polynomial time) and where the problem of adding UNITY properties is difficult (NP-complete). Regarding efficient revision, we present a sound and complete algorithm that adds a singleleads-toproperty (respectively,bounded-time leads-toproperty) and a conjunction ofunless, stable, andinvariantproperties (respectively,bounded-time unlessandstable) to an existing untimed (respectively, real-time) UNITY program in polynomial-time in the state space (respectively, region graph) of the given program. Regarding hardness results, we show that (1) while oneleads-to(respectively,ensures) property can be added in polynomial-time, the problem of adding two such properties (or any combination ofleads-toandensures) is NP-complete, (2) if maximum non-determinism is desired then the problem of adding even a singleleads-toproperty is NP-complete, and (3) the problem of providing maximum non-determinism while adding a singlebounded-time leads-toproperty to a real-time program is NP-complete (in the size of the program's region graph) even if the original program satisfies the correspondingunbounded leads-toproperty.

Reprogramming of sensor networks is an important and challenging problem, as it is often necessary to reprogram the sensors in place. In this article, we propose MNP, a multihop reprogramming service designed for sensor networks. One of the problems in reprogramming is the issue of message collision. To reduce the problem of collision, we propose a sender selection algorithm that attempts to guarantee that in a given neighborhood there is at most one source transmitting the program at a time. Furthermore, our sender selection is greedy in that it tries to select the sender that is expected to have the most impact. We use pipelining to enable fast data propagation. MNP is energy efficient because it reduces the active radio time of a sensor node by putting the node into “sleep” state when its neighbors are transmitting a segment that is not of interest. We call this type of sleep contention sleep. To further reduce the energy consumption, we add noreq sleep, where sensor node goes to sleep if none of its neighbors is interested in receiving the segment it is advertising. We also introduce an optional init sleep to reduce the energy consumption in the initial phase of reprogramming. Finally, we investigate the performance of MNP in different network settings.

We focus on decomposition of hard-masking real-time fault-tolerant programs (where safety, timing constraints, and liveness are preserved in the presence of faults) that are designed from their fault-intolerant versions. Towards this end, motivated by the concepts of state predicate detection and state predicate correction, we identify three types of fault-tolerance components, namely, detectors, weak S-correctors, and strong S-correctors. We show that any hard-masking program can be decomposed into its fault-intolerant version plus a collection of detectors, and, weak and strong S-correctors. We argue that such decomposition assists in providing assurance about dependability and time-predictability of embedded systems.

Consider a communication network where each process needs to securely exchange messages with its neighboring processes. In this network, each sent message is encrypted using one or more symmetric keys that are shared only between two processes: the process that sends the message and the neighboring process that receives the message. A straightforward scheme for assigning symmetric keys to the different processes in such a network is to assign each process O ( d ) keys, where d is the maximum number of neighbors of any process in the network. In this article, we present a more efficient scheme for assigning symmetric keys to the different processes in a communication network. This scheme, which is referred to as logarithmic keying, assigns O (log d ) symmetric keys to each process in the network. We show that logarithmic keying can be used in rich classes of communication networks that include star networks, acyclic networks, limited-cycle networks, planar networks, and dense bipartite networks. In addition, we present a construction that utilizes efficient keying schemes for general bipartite networks to construct efficient keying schemes for general networks.

Automated formal analysis methods such as program verification and synthesis algorithms often suffer from time complexity of their decision procedures and also high space complexity known as the state explosion problem. Symbolic techniques, in which elements of a problem are represented by Boolean formulae, are desirable in the sense that they often remedy the state explosion problem and time complexity of decision procedures. Although symbolic techniques have successfully been used in program verification, their benefits have not yet been exploited in the context of program synthesis and transformation extensively. In this paper, we present a symbolic method for automatic synthesis of fault-tolerant distributed programs. Our experimental results on synthesis of classical fault-tolerant distributed problems such as Byzantine agreement and token ring show a significant performance improvement by several orders of magnitude in both time and space complexity. To the best of our knowledge, this is the first illustration where programs with large state space (beyond 2100) is handled during synthesis.

Reprogramming is an essential service for wireless sensor networks. Authenticating reprogramming process is important as sensors need to verify that the code image is truly from a trusted source. There are two ways to achieve authentication: public key based and symmetric key based. Although previous work has shown that public key authentication is feasible on sensor nodes if used sparingly, it is still quite expensive compared to symmetric key based approach. In this paper, we propose a symmetric key based protocol for authenticating reprogramming process. Our protocol is based on the secret instantiation algorithm from, which requires only O(log n) keys to be maintained at each sensor. We integrate this algorithm with the existing reprogramming protocol. Through simulation, we show that it is able to authenticate reprogramming process at very low communication cost, and has very short delay.

We present a simple, local protocol, pCover, which provides partial (but high) coverage in sensor networks. Through pCover, we demonstrate that it is feasible to maintain a high coverage (~90%) while significantly increasing coverage duration when compared with protocols that provide full coverage. In particular, we show that we are able to maintain 94% coverage for a duration that is 2.3-7 times the duration for which existing protocols maintain full coverage. Through simulations, we show that our protocol provides load balancing, i.e., the desired level of coverage is maintained (almost) until the point where all sensors deplete their batteries

Reprogramming of sensor networks is an important and challenging problem as it is often necessary to reprogram the sensors in place. In this paper, we propose a multihop reprogramming service designed for Mica-2/XSM motes. One of the problems in reprogramming is the issue of message collision. To reduce the problem of collision and hidden terminal problem, we propose a sender selection algorithm that attempts to guarantee that in a neighborhood there is at most one source transmitting the program at a time. Further, our sender selection is greedy in that it tries to select the sender that is expected to have the most impact. We also use pipelining to enable fast data propagation. MNP is energy efficient because it reduces the active radio time of a sensor node by putting the node into "sleep" state when its neighbors are transmitting a segment that is not of interest. Finally, we argue that it is possible to tune our service according to the remaining battery level of a sensor, i.e., it can be tuned so that the probability that a sensor is given the responsibility of transmitting the code is proportional to its remaining battery life

In this paper, we focus on the problem of identifying a family of collusion resistant protocols that demonstrate a tradeoff between the number of secrets that users maintain and the extent of collusion resistance. Towards this end, we define classes of collusion resistant protocols (modeled along the complexity classes in algorithmic complexity) and evaluate the membership of existing protocols as well as the protocols in the proposed family in these classes. We also show that this family contains existing protocols for instantiating security.

Project ExScal (for extreme scale) fielded a 1000+ node wireless sensor network and a 200+ node peer-to-peer ad hoc network of 802.11 devices in a 13km by 300m remote area in Florida, USA during December 2004. In comparison with previous deployments, the ExScal application is relatively complex and its networks are the largest ones of either type fielded to date. In this paper, we overview the key requirements of ExScal, the corresponding design of the hardware/software platform and application, and some results of our experiments.

We focus on the problem of synthesizing failsafe fault-tolerance where fault-tolerance is added to an existing (fault-intolerant) program. A failsafe fault-tolerant program satisfies its specification (including safety and liveness) in the absence of faults. However, in the presence of faults, it satisfies its safety specification. We present a somewhat unexpected result that, in general, the problem of synthesizing failsafe fault-tolerant distributed programs from their fault-intolerant version is NP-complete in the state space of the program. We also identify a class of specifications, monotonic specifications, and a class of programs, monotonic programs, for which the synthesis of failsafe fault-tolerance can be done in polynomial time (in program state space). As an illustration, we show that the monotonicity restrictions are met for commonly encountered problems, such as Byzantine agreement, distributed consensus, and atomic commitment. Furthermore, we evaluate the role of these restrictions in the complexity of synthesizing failsafe fault-tolerance. Specifically, we prove that if only one of these conditions is satisfied, the synthesis of failsafe fault-tolerance is still NP-complete. Finally, we demonstrate the application of monotonicity property in enhancing the fault-tolerance of (distributed) nonmasking fault-tolerant programs to masking.

In this paper, we investigate the effect of the representation of safety specification on the complexity of adding masking fault tolerance to programs - where, in the presence of faults, the program 1) recovers to states from where it satisfies its (safety and liveness) specification and 2) preserves its safety specification during recovery. Specifically, we concentrate on two approaches for modeling the safety specifications: 1) the bad transition (BT) model, where safety is modeled as a set of bad transitions that should not be executed by the program, and 2) the bad pair (BP) model, where safety is modeled as a set of finite sequences consisting of at most two successive transitions. If the safety specification is specified in the BT model, then it is known that the complexity of automatic addition of masking fault tolerance to high atomicity programs - where processes can read/write all program variables in an atomic step) - is polynomial in the state space of the program. However, for the case where one uses the BP model to specify safety specification, we show that the problem of adding masking fault tolerance to high atomicity programs is NP-complete. Therefore, we argue that automated synthesis of fault-tolerant programs is likely to be more successful if one focuses on problems where safety can be represented in the BT model.

We concentrate on automated synthesis of multitolerant programs, i.e., programs that tolerate multiple classes of faults and provide a (possibly) different level of fault-tolerance to each class. We consider three levels of fault-tolerance: (1) failsafe, where in the presence of faults, the synthesized program guarantees safety, (2) nonmasking, where in the presence of faults, the synthesized program recovers to states from where its safety and liveness are satisfied, and (3) masking where in the presence of faults the synthesized program satisfies safety and recovers to states from where its safety and liveness are satisfied. We focus on the automated synthesis of finite-state multitolerant programs in high atomicity model where the program can read and write all its variables in an atomic step. We show that if one needs to add failsafe (respectively, nonmasking) fault-tolerance to one class of faults and masking fault-tolerance to another class of faults then such addition can be done in polynomial time in the state space of the fault-intolerant program. However, if one needs to add failsafe fault-tolerance to one class of faults and nonmasking fault-tolerance to another class of faults then the resulting problem is NP-complete. We find this result to be counterintuitive since adding failsafe and nonmasking fault-tolerance to the same class of faults (which is equivalent to adding masking fault-tolerance to that class of faults) can be done in polynomial time, whereas adding failsafe fault-tolerance to one class of faults and nonmasking fault-tolerance to a different class of faults is NP-complete.

In this paper we focus on automated techniques to enhance the fault-tolerance of a nonmasking fault-tolerant program to masking. A masking program continually satisfies its specification even if faults occur. By contrast, a nonmasking program merely guarantees that after faults stop occurring, the program recovers to states from where it continually satisfies its specification. Until the recovery is complete, however a nonmasking program can violate its (safety) specification. Thus, the problem of enhancing fault-tolerance from nonmasking to masking requires that safety be added and recovery be preserved. We focus on this enhancement problem for high atomicity programs-where each process can read all variables-and for distributed programs-where restrictions are imposed on what processes can read and write. We present a sound and complete algorithm for high atomicity programs and a sound algorithm for distributed programs. We also argue that our algorithms are simpler than previous algorithms, where masking fault-tolerance is added to a fault-intolerant program. Hence, these algorithms can partially reap the benefits of automation when the cost of adding masking fault-tolerance to a fault-intolerant program is high. To illustrate these algorithms, we show how the masking fault-tolerant programs for triple modular redundancy and Byzantine agreement can be obtained by enhancing the fault-tolerance of the corresponding nonmasking versions. We also discuss how the derivation of these programs is simplified when we begin with a nonmasking fault-tolerant program.

In this paper, we focus our attention on the problem of automating the addition of failsafe fault-tolerance where fault-tolerance is added to an existing (fault-intolerant) program. A failsafe fault-tolerant program satisfies its specification (including safety and liveness) in the absence of faults. And, in the presence of faults, it satisfies its safety specification. We present a somewhat unexpected result that, in general, the problem of adding failsafe fault-tolerance in distributed programs is NP-hard. Towards this end, we reduce the 3-SAT problem to the problem of adding failsafe fault-tolerance. We also identify a class of specifications, monotonic specifications and a class of programs, monotonic programs. Given a (positive) monotonic specification and a (negative) monotonic program, we show that failsafe fault-tolerance can be added in polynomial time. We note that the monotonicity restrictions are met for commonly encountered problems such as Byzantine agreement, distributed consensus, and atomic commitment. Finally, we argue that the restrictions on the specifications and programs are necessary to add failsafe fault-tolerance in polynomial time; we prove that if only one of these conditions is satisfied, the addition of failsafe fault-tolerance is still NP-hard.

Research in system stabilization has traditionally relied on the availability of a complete system implementation. As such, it would appear that the scalability and reusability of stabilization is limited in practice. Towards redressing this perception, the authors show for the first time that system stabilization may be designed knowing only the system specification but not the system implementation. We refer to stabilization designed thus as being "graybox" and identify "local everywhere-eventually specifications" as being amenable to design of graybox stabilization. We illustrate the design of graybox stabilization using timestamp-based distributed mutual exclusion as our example.

We present a polynomial time algorithm for automatic synthesis of fault-tolerant distributed programs, starting from fault-intolerant versions of those programs. Since this synthesis problem is known to be NP-hard, our algorithm relies on heuristics to reduce the complexity. We demonstrate that our algorithm is able to synthesize an agreement program that tolerates a Byzantine fault.

Vector clocks (VC) are an inherent component of a rich class of distributed applications. In this paper, we consider the problem of realistic —more specifically, bounded-space and fault-tolerant— implementation of these client applications. To this end, we generalize the notion of VC to resettable vector clocks (RVC), and provide a realistic implementation of RVC. Further, we identify an interface contract under which our RVC implementation can be substituted for VC in client applications, without affecting the client's correctness. Based on such substitution, we show how to transform the client so that it is itself realistically implemented; we demonstrate our method in the context of Ricart-Agrawala's mutual exclusion program.

Two primitive components, namely detectors and correctors, provide a basis for achieving the different types of fault tolerance properties required in computing systems. We develop the theory of these primitive tolerance components, characterizing precisely their role in achieving the different types of fault tolerance. Also, we illustrate how they can be used to formulate extant design methods and argue that they sometimes offer the potential for better designs than those obtained from extant methods.

We show how fault-tolerance can be effectively added to several types of faults in program computations that use barrier synchronization. We divide the faults that occur in practice into two classes, detectable and undetectable, and design a fully distributed program that tolerates the faults in both classes. Our program guarantees that every barrier is executed correctly even if detectable faults occur, and that eventually every barrier is executed correctly even if undetectable faults occur. Via analytical as well as simulation results we show that the cost of adding fault-tolerance is low, in part by comparing the times required by our program with that required by the corresponding fault-intolerant counterpart.

The concept of multitolerance abstracts problems in system dependability and provides a basis for improved design of dependable systems. In the abstraction, each source of undependability in the system is represented as a class of faults, and the corresponding ability of the system to deal with that undependability source is represented as a type of tolerance. Multitolerance thus refers to the ability of the system to tolerate multiple fault classes, each in a possibly different way. We present a component based method for designing multitolerance. Two types of components are employed by the method, namely detectors and correctors. A theory of detectors, correctors, and their interference free composition with intolerant programs is developed, which enables stepwise addition of components to provide tolerance to a new fault class while preserving the tolerances to the previously added fault classes. We illustrate the method by designing a fully distributed multitolerant program for a token ring.

Masking fault-tolerance guarantees that programs continually satisfy their specification in the presence of faults. By way of contrast, nonmasking fault-tolerance does not guarantee as much: it merely guarantees that when faults stop occurring, program executions converge to states from where programs continually (re)satisfy their specification. We present in this paper a component based method for the design of masking fault-tolerant programs. In this method, components are added to a fault-intolerant program in a stepwise manner, first, to transform the fault-intolerant program into a nonmasking fault-tolerant one and, then, to enhance the fault-tolerance from nonmasking to masking. We illustrate the method by designing programs for agreement in the presence of Byzantine faults, data transfer in the presence of message loss, triple modular redundancy in the presence of input corruption, and mutual exclusion in the presence of process fail-stops. These examples also serve to demonstrate that the method accommodates a variety of fault-classes. It provides alternative designs for programs usually designed with extant design methods, and it offers the potential for improved masking fault-tolerant programs.

OFMP is a hierarchical, network management protocol that enables group operations to be executed on the management information bases of all nodes in the group. As long as no faults occur, OFMP ensures that all nodes execute their local operation exactly once in each group operation. If "immediately-detectable" faults occur, it ensures masking fault-tolerance; i.e., all non-failed nodes execute their local operation exactly once in each group operation. And, if "eventually-detectable" faults occur, it ensures stabilizing fault-tolerance; i.e., it eventually converges to a state from where all non-failed nodes execute their local operation exactly once in each subsequent group operation. Of special note is the ability of OFMP to detect using only a bounded amount of memory whether nodes have executed in same group operation, in a manner that masks immediately-detectable faults and stabilizes from eventually-detectable faults.

Masking fault-tolerance guarantees that programs continually satisfy their specification in the presence of faults. By way of contrast, nonmasking fault-tolerance does not guarantee as much: it merely guarantees that when faults stop occurring, program executions converge to states from where programs continually (re)satisfy their specification. In this paper, we show that a practical method to design masking fault-tolerance is to first design nonmasking fault-tolerance and to then transform the nonmasking fault-tolerant program minimally so as to achieve masking fault-tolerance. We demonstrate this method by designing novel fully distributed programs for termination detection, mutual exclusion, and leader election, that are masking tolerant of any finite number of process fail-stops and/or repairs.