We identify 13 problems whose solutions can significantly enhance our ability to design and analyze firewalls and other packet classifiers. These problems include the firewall equivalence problem, the firewall redundancy problem, the firewall verification problem, and the firewall completeness problem. The main result of this paper is to prove that every one of these problems is NP-hard. Our proof of this result is interesting in the following way. Only one of the 13 problems, the so called slice probing problem, is shown to be NP-hard by a reduction from the well-known 3-SAT problem. Then, the remaining 12 problems are shown to be NP-hard by reductions from the slice probing problem. This proof suggests that the slice probing problem plays an important role in the design and analysis of firewalls. The negative results of this paper suggest that firewalls designers may need to rely on SAT solvers to solve instances of these 13 problems or may be content with probabilistic solutions of these problems. On the positive side, we show that each of the 13 firewall analysis problems presented in this paper is polynomially reducible to the slice probing problem. Thus any algorithm, that can effectively solve the slice probing problem, can also be employed to effectively solve any of these 13 problems.

Most networks require that their users have "identities", i.e. have names that are fixed for a relatively long time, unique, and have been approved by a central authority (in order to guarantee their uniqueness). Unfortunately, this requirement, which was introduced to simplify the design of networks, has its own drawbacks. First, this requirement can lead to the loss of anonymity of communicating users. Second, it can allow the possibility of identity theft. Third, it can lead some users to trust other users who may not be trustworthy. In this paper, we argue that networks can be designed without user identities and their drawbacks. Our argument consists of providing answers to the following three questions. (1) How can one design a practical network where users do not have identities? (2) What does it mean for a user to authenticate another user in a network without identities? (3) How can one design a secure authentication protocol in a network without identities?

The need for secure communication in the Internet has led to the widespread deployment of secure application-level protocols. The current state- of-the-art is to use TLS, in conjunction with a password protocol. The password protocol, which we call a one-way password protocol (OPP), authenticates a user to a server, using a particular secret called the password. TLS has two functions: (1) It ensures secure communication between a client and a server (2) It allows a user to authenticate a server. The first function effectively provides a secure channel for end-to- end communication between a client and a server. However, the second function is frequently compromised by a variety of Phishing attacks. In this paper, we address this problem by developing a password protocol which we name the Two-way Password Protocol (TPP). TPP, when used in conjunction with TLS, ensures that users correctly authenticate servers, and are protected from Phishing attacks. The first contribution of this paper is to develop a protocol, called the Universal Password Protocol (UPP), which ensures that a user's password is kept safe even in the case of a successful Phishing attack. However, it may be noted that a user, after logging in, frequently shares other secrets (such as credit card number) over the secure connection, and UPP cannot protect these. Our second contribution is to build on UPP and develop, first, the Two-Way Password Protocol (TPP), and finally an improved version named the Dynamic Two-Way Password Protocol (DTPP), which ensures that both a server and a client are properly authenticated to each other. This ensures the security of all secrets which should be known only to the client and the server, including, of course, the password.

The World Wide Web famously supports two transport protocols: HTTP and HTTPS. These two protocols are at the opposite ends of three dimensions: security guarantees, cost of use, and compatibility with middle boxes (e.g. cache proxies) in the Internet. At one end, HTTP provides no security guarantees, but it is inexpensive to use, and is compatible with middle boxes in the Internet. At the other end, HTTPS provides three security guarantees, but it is expensive to use and is not compatible with middle boxes. Although the three security guarantees provided by HTTPS, namely server authentication, message integrity, and message confidentiality, are important in general, many web servers (e.g. email servers) do not need the message confidentiality guarantee. In this paper, we present a new transport protocol for the Web, named HTTPI. This protocol provides both server authentication and message integrity, but not message confidentiality. Like HTTP, HTTPI is inexpensive to use and is compatible with middle boxes, and like HTTPS, it defends against many cyber attacks (e.g. Pharming attacks) that HTTP cannot defend against. We developed a preliminary implementation of HTTPI and showed through experimentation that the throughput of HTTPI is within 1.2% from that of HTTP and is 37% better than that of HTTPS.

A firewall is a packet filter that is placed at the entrance of a private network. It checks the header fields of each incoming packet into the private network and decides, based on the specified rules in the firewall, whether to accept the packet and allow it to proceed or to discard the packet. To validate the correctness and effectiveness of the rules in a firewall, the firewall rules are usually subjected to two types of analysis: verification and redundancy checking. Verification is used to verify that the rules in a firewall accept all packets that should be accepted and discard all packets that should be discarded. Redundancy checking is used to check that no rule in a firewall is redundant (i.e. can be removed from the firewall without changing the sets of packets accepted and discarded by the firewall). In this paper we show that, contrary to the conventional wisdom, these two types of analysis are in fact equivalent. In particular, we show that (1) every verification algorithm can be also used to check whether a rule in a firewall is redundant, and (2) every redundancy checking algorithm can be also used to verify whether the rules in a firewall accept or discard an intended set of packets.

No abstract available.

Policies defined by a sequence of predicate-decision rules, with first-match semantics, are widely used; a notable example is their use in firewalls, where the rules are used to decide whether to accept or discard each packet. Owing to the critical importance of correctness of such policies, as well as the need for high performance, they have been the subject of considerable analysis. In earlier work, we have demonstrated that the problem of removing redundant rules from firewalls is theoretically equivalent to verifying that a firewall satisfies a property, and proposed that this theorem be used to build a high performance redundancy remover. In this paper, we realize this promise, and build a fast linear-space redundancy remover, one to three orders of magnitude faster than current approaches. Further, we show that our algorithm is easy to parallelize- there exists a natural way to partition a large instance of the problem into independent small ones.

Many sensor networks (especially networks of mobile sensors or networks that are deployed to monitor crisis situations) are deployed in an arbitrary and unplanned fashion. Thus, any sensor in such a network can end up being adjacent to any other sensor in the network. To secure the communications between every pair of adjacent sensors in such a network, each sensor x in the network needs to store n − 1 symmetric keys that sensor x shares with all the other sensors, where n is the number of sensors in the network. This storage requirement of the keying protocol is rather severe, especially when n is large and the available storage in each sensor is modest. Earlier efforts to redesign this keying protocol and reduce the number of keys to be stored in each sensor have produced protocols that are vulnerable to impersonation, eavesdropping, and collusion attacks. In this paper, we present a fully secure keying protocol where each sensor needs to store (n+1)/2 keys, which is much less than the n − 1 keys that need to be stored in each sensor in the original keying protocol. We also show that in any fully secure keying protocol, each sensor needs to store at least (n − 1)/2 keys.

A firewall is a packet filter that is placed at the entrance of a private network. It checks the header fields of each incoming packet into the private network and decides, based on the specified rules in the firewall, whether to accept the packet and allow it to proceed, or to discard the packet. A property of a firewall is a set of packets that the firewall is required to accept or discard. Associated with each firewall is a very large set of properties that the firewall needs to satisfy. The space and time complexity of the best known deterministic algorithm, for verifying that a given firewall satisfies a given property, is 0(nd), where n is the number of rules in the given firewall and d is the number of fields checked by the firewall. Usually, n is around 2000 and d is 5. In this paper, we propose the first deterministic firewall verification algorithm whose space complexity is 0(nd), linear in both n and d. This algorithm consists of three components: a projection pass, a division pass, and a probe algorithm. We applied our verification algorithm to over two million firewall-property pairs, varying n from 100 to 10000 and fixing d at 5. From this experiment, we observed that the algorithm requires (900 + 0.5n) Kilobytes of storage and in the order of 10 seconds execution time.

A firewall is a packet filter placed at an entry point of a network in the Internet. Each packet that goes through this entry point is checked by the firewall to determine whether to accept or discard the packet. The firewall makes this determination based on a specified sequence of overlapping rules. The firewall uses the first-match criterion to determine which rule in the sequence should be applied to which packet. Thus, to compute the set of packets to which a rule is applied, the firewall designer needs to consider all the rules that precede this rule in the sequence. This “rule dependency” complicates the task of designing firewalls (especially those with thousands of rules), and makes firewalls hard to understand. In this paper, we present a metric, called the dependency metric, for measuring the complexity of firewalls. This metric, though accurate, does not seem to suggest ways to design firewalls whose dependency metrics are small. Thus, we present another metric, called the inversion metric, and develop methods for designing firewalls with small inversion metrics. We show that the dependency metric and the inversion metric are correlated for some classes of firewalls. So by aiming to design firewalls with small inversion metrics, the designer may end up with firewalls whose dependency metrics are small as well. We present a method for designing modular firewalls whose inversion metrics are very small. Each modular firewall consists of several components, called firewall modules. The inversion metric of each firewall module is very small - in fact, 1 or 2. Thus, we conclude that modular firewalls are easy to design and easy to understand.

The 11 papers in this special issue on mission critical networking are divided into three categories: quality of service issues (three papers); security issues (four papers); and configuration and data collection issues (four papers).

Flood is a communication primitive that can be used by the base station of a sensor network to send a copy of a message to every sensor in the network. When a sensor receives a flood message, the sensor needs to check whether it has received this message for the first time and so this message is fresh, or it has received the same message earlier and so the message is redundant. In this paper, we discuss a family of four flood sequencing protocols that use sequence numbers to distinguish between fresh and redundant flood messages. These four protocols are: a sequencing free protocol, a linear sequencing protocol, a circular sequencing protocol, and a differentiated sequencing protocol. We analyze the self-stabilization properties of these four flood sequencing protocols. We also compare the performance of these flood sequencing protocols, using simulation, over various settings of sensor networks. We conclude that the differentiated sequencing protocol has better stabilization property and provides better performance than those of the other three protocols.

Packet classification is the core mechanism that enables many networking services on the Internet such as firewall packet filtering and traffic accounting. Using ternary content addressable memories (TCAMs) to perform high-speed packet classification has become the de facto standard in the industry. TCAMs classify packets in constant time by comparing a packet with all classification rules of ternary encoding in parallel. Despite their high speed, TCAMs suffer from the well-known interval expansion problem. As packet classification rules usually have fields specified as intervals, converting such rules to TCAM-compatible rules may result in an explosive increase in the number of rules. This is not a problem if TCAMs have large capacities. Unfortunately, TCAMs have very limited capacity, and more rules means more power consumption and more heat generation for TCAMs. Even worse, the number of rules in packet classifiers have been increasing rapidly with the growing number of services deployed on the Internet. In this paper, we propose to address the interval expansion problem of TCAMs by removing redundant rules in classifiers. This equivalent transformation can significantly reduce the number of TCAM entries needed by a classifier. Our experiments on real-life classifiers show an average reduction of 58.2 percent in the number of TCAM entries by removing redundant rules. Given the logical interleaving nature of packet filtering rules, identifying redundant rules in classifiers is by no means trivial, and to achieve the guarantee of no redundant rules in resulting classifiers is even more challenging. In this paper, for the first time, we give a necessary and sufficient condition for identifying all redundant rules in a classifier. Based on this condition, we categorize redundant rules into upward redundant rules and downward redundant rules. Second, we present two algorithms for detecting and removing the two types of redundant rules, respectively. Third, we formally prove that the resulting classifiers have no redundant rules after running the two algorithms. Last, we conduct extensive experiments on both real-life and synthetic classifiers. The experimental results show that our redundancy removal algorithms are both effective and efficient.

In BGP, autonomous systems (ASes) advertise routes. Unfortunately, malicious ASes can advertise false routes that do not exist in the Internet. Many extensions of BGP have been proposed to allow each AS to check whether the received routes are false. It turns out that none of these extensions can defend against collusions among malicious ASes. In this paper, we present an extension of BGP that can defend against collusions. In our extension, each listed AS in an advertised route supplies a certified full list of all its peers, i.e. neighbors. Because full peer lists can be very large, we develop an optimization where each AS in an advertised route supplies a balanced peer list that is much smaller than its full peer list. Using real Internet topology data, we demonstrate that the average, or largest, balanced peer list is 92% smaller than the average, or largest respectively, full peer list.

A firewall is a filter placed at the entrance of a private network. Its function is to examine each packet that is incoming into the private network and decide, based on the specified rules of the firewall, whether to accept the packet and allow it to proceed, or to discard the packet. A property of a firewall is a specified set of packets that is supposed to be accepted or discarded by the firewall. In this paper, we present the first linear time algorithm to verify whether a given firewall satisfies a given property. The time complexity of our algorithm is O(nd), where n is the number of rules in the given firewall and d is the number of fields that are checked by the firewall. Our verification algorithm consists of two passes: a deterministic pass followed by a probabilistic pass. In most cases, the algorithm correctly determines whether the given firewall satisfies the given property. But in some rare cases, the algorithm may erroneously determine that the firewall satisfies the property. Using a combination of analysis and extensive simulation, we show that the probability of an error by the algorithm is of the order of 6 times 10-5.

We discuss the stabilization properties of networks that are composed of ¿displacement elements¿. Each displacement element is defined by an integer K, called the displacement of the element, an input variable x, and an output variable y, where the values of x and y are non-negative integers. An execution step of this element assigns to y the maximum of 0 and K + x. The objective of our discussion is to demonstrate that two principles play an important role in ensuring that a network N is stabilizing, i. e. starting from any global state, network N is guaranteed to reach a global fixed point. Specifically, the principle of consistent fixed points is analogous to the requirement that a control system be free from self-oscillations. And the principle of negative gain is analogous to the requirement that the feedback loop of a sum of displacements along every directed loop in network N is negative.

A widely used mechanism for computing the topology of any network in the Internet is Traceroute. Using Traceroute, one simply needs to choose any two nodes in a network and then obtain the sequence of nodes that occur between these two nodes, as specified by the routing tables in these nodes. Thus, each use of Traceroute in a network produces a trace of nodes that constitute a simple path in this network. In every trace that is produced by Traceroute, each node occurs either by its unique identifier or by the anonymous identifier "*". In this paper, we introduce the first theory aimed at answering the following important question. Is there an algorithm to compute the topology of a network N from a trace set T that is produced by using Traceroute in N, assuming that each edge in N occurs in at least one trace in T, and that each node in N occurs by its unique identifier in at least one trace in T? Our theory shows that the answer to this question is "No" in general. But if N is a tree, or is an odd ring, then the answer is "Yes". On the other hand, if N is an even ring, the answer is "No", but if N is a "mostly regular" even ring, then the answer is "Yes".

Routing protocols are designed under the assumption that each node in a network should be able to reach (i. e. send or forward packets to) every other node in the network. Unfortunately, adopting this assumption in a routing protocol does allow adversary nodes to launch spam or DoS attacks against the other nodes in the network. In this paper, we introduce the "blocking option" in routing protocols; this option allows a node u to block a specified set of nodes {v,..,w} and prevent each of them from reaching node u. It turns out that if node u blocks a large number of nodes, then u may end up blocking other nodes as well. We refer to these unintentionally blocked nodes as blind_to u nodes. Clearly, a node u cannot communicate with its blind nodes in a regular manner. Thus, we extend the routing protocol to allow each node u to communicate with its blind nodes via some special node, called the joint node. To perform its intended function, the joint node needs to be neither blocked by any node nor blind to any node in the network. We give an algorithm for identifying the node that is best suited to be the joint node in a network. Finally, we show, through extensive simulation, that the average number of blind nodes is close to zero when the average number of blocked nodes is small (-3. The path length of using a joint node for communication between a node u and any one of its blind nodes v is around 1.5 the shortest path between u and v.

Firewalls are crucial elements in network security, and have been widely deployed in most businesses and institutions for securing private networks. The function of a firewall is to examine each incoming and outgoing packet and decide whether to accept or to discard the packet based on its policy. Due to the lack of tools for analyzing firewall policies, most firewalls on the Internet have been plagued with policy errors. A firewall policy error either creates security holes that will allow malicious traffic to sneak into a private network or blocks legitimate traffic and disrupts normal business processes, which in turn could lead to irreparable, if not tragic, consequences. Because a firewall may have a large number of rules and the rules often conflict, understanding and analyzing the function of a firewall has been known to be notoriously difficult. An effective way to assist firewall administrators to understand and analyze the function of their firewalls is by issuing queries. An example of a firewall query is "Which computers in the private network can receive packets from a known malicious host in the outside Internet?rdquo Two problems need to be solved in order to make firewall queries practically useful: how to describe a firewall query and how to process a firewall query. In this paper, we first introduce a simple and effective SQL-like query language, called the Structured Firewall Query Language (SFQL), for describing firewall queries. Second, we give a theorem, called the Firewall Query Theorem, as the foundation for developing firewall query processing algorithms. Third, we present an efficient firewall query processing algorithm, which uses decision diagrams as its core data structure. Fourth, we propose methods for optimizing firewall query results. Finally, we present methods for performing the union, intersect, and minus operations on firewall query results. Our experimental results show that our firewall query processing algorithm is very efficient: it takes less than 10 milliseconds to process a query over a firewall that has up to 10,000 rules.

The private computer network of any large enterprise has tens, or even hundreds, of firewalls. These firewalls are placed at the entry points of the network (where the network is connected with the rest of the Internet), and at many chosen points within the network. The result is a complex firewall network that seems hard to understand or analyze. In this paper, we propose a method for verifying the correctness of firewall networks with tree topologies. Our method is based on identifying two types of properties of firewall trees: accept and discard properties. An accept (or discard) property of a firewall tree specifies a class of packets that should be accepted (or discarded, respectively) by the firewall tree. We present two algorithms that can be used to decide whether a given firewall tree satisfies a given, accept or discard, property of that tree.

We present DESALalpha, a realization of the dynamic embedded sensor-actuator language for Telos-based devices. The platform provides native support for: (i) rule-based programming; (ii) synchronized action scheduling; (iii) neighborhood management; and (iv) distributed state sharing. We describe the design and implementation of DESALalpha, present examples that illustrate its use, and summarize the resource requirements of compiled applications. Finally, we present lessons learned based on our use of DESALalphaduring the past year.

In this paper, we introduce an objective model of trust in peer-to-peer networks. Based on this model, we develop protocols that can be used by the peers in a peer-to-peer network to compute the trust values of other peers in these networks. According to our model, the trust value of a peer is the probability that this peer sends correct messages to other peers, provided that this probability is at least 0.6. (A peer whose probability of sending correct messages is less than 0.6 is regarded as a bad peer that cannot be trusted by other peers in the network.) Each peer actively monitors several good peers in the network and accurately estimates the trust values of each of them. The peers then exchange messages about the trust values of the good peers that they have monitored, and each of them ends up accurately computing the trust values of many good peers in the network, even though many of the exchanged messages are arbitrarily wrong. Through analysis and simulation, we show that a peer in a network can compute the trust values of about 100 good peers in the network, while keeping the error in computing these trust values below 10-4.

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.

Firewalls are the mainstay of enterprise security and the most widely adopted technology for protecting private networks. An error in a firewall policy either creates security holes that will allow malicious traffic to sneak into a private network or blocks legitimate traffic and disrupts normal business processes, which in turn could lead to irreparable, if not tragic, consequences. It has been observed that most firewall policies on the Internet are poorly designed and have many errors. Therefore, how to design firewall policies correctly is an important issue. In this paper, we propose the method of diverse firewall design, which consists of three phases: a design phase, a comparison phase, and a resolution phase. In the design phase, the same requirement specification of a firewall policy is given to multiple teams who proceed independently to design different versions of the firewall policy. In the comparison phase, the resulting multiple versions are compared with each other to detect all functional discrepancies between them. In the resolution phase, all discrepancies are resolved and a firewall that is agreed upon by all teams is generated.

We design and evaluate a lightweight route verification mechanism that enables a router to discover route failures and inconsistencies between advertised Internet routes and actual paths taken by the data packets. Our mechanism is accurate, incrementally deployable, and secure against malicious intermediary routers. By carefully avoiding any cryptographic operations in the data path, our prototype implementation achieves the overhead of less than 1% on a 1 Gbps link, demonstrating that our method is suitable even for high-performance networks.

Consider a distributed system that delivers a set of services (such as message routing, maintenance of a global invariant, leader election, mutual exclusion, and so forth) to a distributed application. Such a system often provides its services at all times, regardless of whether or not these services are in demand at any given time. This leads to wasteful use of system resources. In this paper, we propose a novel stabilizing protocol for deactivating the system services in the absence of demand and reactivating the services upon demand. The proposed protocol is simple enough. When a process needs a service, it periodically sends messages that reach every other process in the system and causes every process to reactivate the service. For this purpose, only a single-type message carrying no information is sent in the system. When no process needs the service, the sending of messages is stopped, causing every process to deactivate the service. The proposed system has many applications in mobile and sensor networks.

We consider a network where users can issue certificates that identify the public keys of other users in the network. The issued certificates in a network constitute a set of certificate chains between users. A user u can obtain the public key of another user v from a certificate chain from u to v in the network. For the certificate chain from u to v, u is called the source of the chain and v is called the destination of the chain. Certificates in each chain are dispersed between the source and destination of the chain such that the following condition holds. If any user u needs to securely send messages to any other user v in the network, then u can use the certificates stored in u and v to obtain the public key of v (then u can use the public key of v to set up a shared key with v to securely send messages to v). The cost of dispersing certificates in a set of chains among the source and destination users in a network is measured by the total number of certificates that need to be stored in all users. A dispersal of a set of certificate chains in a network is optimal if no other dispersal of the same chain set has a strictly lower cost. In this paper, we show that the problem of computing optimal dispersal of a given chain set is NP-complete. Thus, minimizing the total number of certificates stored in all users is NP--complete. We identify three special classes of chain sets that are of practical interests and devise three polynomial-time algorithms that compute optimal dispersals for each class. We also present two polynomial-time extensions of these algorithms for more general classes of chain sets.

We discuss several efficient schemes for assigning symmetric keys in a network of small computers (e. g. an ad-hoc or sensor network) such that any two adjacent computers in the network can communicate securely using the keys assigned to both of them. The schemes are efficient because they require that each computer be assigned O(log d) symmetric keys, where d is the network degree, instead of O(d) symmetric keys that one expects in a straightforward scheme

We consider a system where each user has a public key and a private key. In this system, a certificate is a data item that is issued by one user u and contains the public key of another user v. A third user w that knows the public key of u can verify that this certificate has not been corrupted (by an adversary) since it was issued by u, and so can accept the public key in the certificate as the correct public key of v. User w can use this accepted public key of v in two ways. First, w can securely communicate with v. Second, w can obtain more public keys of other users, as it used the public key of u to obtain the public key of v. However, the safety of the second use is questionable if u, the issuer of the certificate, has concluded that it cannot trust v enough to accept a public key merely because v accepts it. To solve this problem, we propose that each certificate should have a "rating". The rating of a certificate describes how much trust the issuer puts on the subject concerning key acceptance. We present an algorithm for computing a subgraph G.dst(src) of a certificate graph G, for a user src to find the correct public key of another user dst in G. The time complexity of this algorithm is 0(e), where e is the number of certificates in the system. This algorithm meets the lower bound of the worst case complexity.

We describe a family of log n protocols for assigning symmetric keys to n processes in a network so that each process can use its assigned keys to communicate securely with every other process. The k-th protocol in our protocol family, where 1 les k les log n, assigns O(k2kradicn) symmetric keys to each process in the network. (Thus, our (log n)-th protocol assigns O(log2n) symmetric keys to each process. This is not far from the lower bound of O(log n) symmetric keyswhichweshowis needed for each process to communicate securely with every other process in the network.) The protocols in our protocol family can be used to assign symmetric keys to the processes in a sensor network, or ad-hoc or mobile network, where each process has a small memory to store its assigned keys. We also discuss the vulnerability of our protocols to "collusion". In particular, we show thatkradicn colluding processes can compromise the security of the k-th protocol in our protocol family.

We propose the first model of stateful firewalls. In this model, each stateful firewall has a variable set called the state of the firewall, which is used to store some packets that the firewall has accepted previously and needs to remember in the near future. Each stateful firewall consists of two sections: a stateful section and a stateless section. Upon receiving a packet, the firewall processes it in two steps. In the first step, the firewall augments the packet with an additional field called the tag, and uses the stateful section to compute the value of this field according to the current state of the firewall. In the second step, the firewall compares the packet together with its tag value against a sequence of rules in the stateless section to identify the first rule that the packet matches: the decision of this rule determines the fate of the packet. Our model of stateful firewalls has several favorable properties. First, despite its simplicity, it can express a variety of state tracking functionalities. Second, it allows us to inherit the rich results in stateless firewall design and analysis. Third, it provides backward compatibility such that a stateless firewall can also be specified using our model. This paper goes beyond proposing this stateful firewall model itself. A significant portion of this paper is devoted to analyzing the properties of stateful firewalls that are specified using our model. We outline a method for verifying whether a firewall is truly stateful. The method is based on the three properties of firewalls: conforming, grounded, and proper. We show that if a firewall satisfies these three properties, then the firewall is truly stateful.

Cookies are the primary means for Web applications to authenticate HTTP requests and to maintain client states. Many Web applications (such as electronic commerce) demand a secure cookie protocol. Such a protocol needs to provide the following four services: authentication, confidentiality, integrity and antireplay. Several secure cookie protocols have been proposed in previous literature; however, none of them are completely satisfactory. In this paper, we propose a secure cookie protocol that is effective, efficient, and easy to deploy. In terms of effectiveness, our protocol provides all of the above four security services. In terms of efficiency, our protocol does not involve any database lookup or public key cryptography. In terms of deployability, our protocol can be easily deployed on an existing Web server, and it does not require any change to the Internet cookie specification. We implemented our secure cookie protocol using PHP, and the experimental results show that our protocol is very efficient.

We address the challenges of bursty convergecast in multi-hop wireless sensor networks, where a large burst of packets from different locations needs to be transported reliably and in real-time to a base station. Via experiments on a 49 MICA2 mote sensor network using a realistic traffic trace, we determine the primary issues in bursty convergecast, and accordingly design a protocol, RBC (for Reliable Bursty Convergecast), to address these issues: To improve channel utilization and to reduce ack-loss, we design a window-less block acknowledgment scheme that guarantees continuous packet forwarding and replicates the acknowledgment for a packet; to alleviate retransmission-incurred channel contention, we introduce differentiated contention control. Moreover, we design mechanisms to handle varying ack-delay and to reduce delay in timer-based re-transmissions. We evaluate RBC, again via experiments, and show that compared to a commonly used implicit-ack scheme, RBC doubles packet delivery ratio and reduces end-to-end delay by an order of magnitude, as a result of which RBC achieves a close-to-optimal goodput.

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.

Firewalls are safety-critical systems that secure most private networks. An error in a firewall either leaks secret information from its network or disrupts legitimate communication between its network and the rest of the Internet. How to design a correct firewall is therefore an important issue. In this paper, we propose the method of diverse firewall design, which is inspired by the well-known method of design diversity for building fault-tolerant software. Our method consists of two phases: a design phase and a comparison phase. In the design phase, the same requirement specification of a firewall is given to multiple teams who proceed independently to design different versions of the firewall. In the comparison phase, the resulting multiple versions are compared with each other to find out all the discrepancies between them, then each discrepancy is further investigated and a correction is applied if necessary. The technical challenge in the method of diverse firewall design is how to discover all the discrepancies between two given firewalls. We present a series of three efficient algorithms for solving this problem: (I) a construction algorithm for constructing an equivalent ordered firewall decision diagram from a sequence of rules, (2) a shaping algorithm for transforming two ordered firewall decision diagrams to become semi-isomorphic without changing their semantics, and (3) a comparison algorithm for detecting all the discrepancies between two semi-isomorphic firewall decision diagrams.

We consider a network where nodes can issue certificates that identify the public keys of other nodes in the network. The issued certificates in a network constitute a directed graph, called the certificate graph of the network. The issued certificates are dispersed among the network nodes such that the following condition holds. If any node, u, needs to send messages to any other node, v, in the network, then u can use the certificates stored in both u and v to obtain the public key of v (then u can securely send messages to v). The cost of a dispersal which assigns certificates to the nodes of a network is measured by the average number of certificates that need to be stored in one node. A dispersal is optimal if its cost is minimum. We present three algorithms and show that each algorithm computes optimal dispersals for a rich class of certificate graphs. The time complexity of each of these algorithms, when one of the algorithms is used to disperse the certificates from a given certificate graph, is O(n/sup 2/), where n is the number of nodes in the input certificate graph.

In this paper, we investigate the security of micropayment protocols that support low-value transactions. We focus on one type of such protocols that are based on hash chains. We present a formal specification of a typical hash chain based micropayment protocol using abstract protocol notation, and discuss how an adversary can attack this protocol using message loss, modification, and replay. We use convergence theory to show that this protocol is secure against these attacks. The specification and verification techniques used in this paper can be applied to other micropayment protocols as well

We investigate how to disperse the certificates, issued in an ad-hoc network, among the network nodes such that the following condition holds. If any node u approaches any other node v in the network, then u can use the certificates stored either in u or in v to obtain the public key of v (so that u can securely send messages to v). We define the cost of certificate dispersal as the average number of certificates stored in one node in the network. We give upper and lower bounds on the dispersability cost of certificates, and show that both bounds are tight. We also present two certificate dispersal algorithms, and show that one of those algorithms is more efficient than the other in several important cases. Finally, we identify a rich class of "certificate graphs" for which the dispersability cost is within a constant factor from the lower bound.

A firewall is often placed at the entrance of each private network in the Internet. The function of a firewall is to examine each packet that passes through the entrance and decide whether to accept the packet and allow it to proceed or to discard the packet. A firewall is usually designed as a sequence of rules. To make a decision concerning some packets, the firewall rules are compared, one by one, with the packet until one rule is found to be satisfied by the packet: this rule determines the fate of the packet. We present the first ever method for designing the sequence of rules in a firewall to be consistent, complete, and compact. Consistency means that the rules are ordered correctly, completeness means that every packet satisfies at least one rule in the firewall, and compactness means that the firewall has no redundant rules. Our method starts by designing a firewall decision diagram (FDD, for short) whose consistency and completeness can be checked systematically (by an algorithm). We then apply a sequence of five algorithms to this FDD to generate, reduce and simplify the target firewall rules while maintaining the consistency and completeness of the original FDD.

An attractive architecture for sensor networks is to have the sensing devices mounted on small computers, called motes. Motes are battery-powered, and can communicate in a wireless fashion by broadcasting messages over radio frequency. In mote networks, the connectivity of a mote u can be defined by those motes that can receive messages from u with high probability and those motes from which u can receive messages with high probability. In this paper, we describe a protocol that can be triggered by any mote in a mote network in order that each mote in the network computes its connectivity. The protocol is simple and has several energy saving features. We implemented this protocol over TinyOS and discuss the results of some execution runs of this implementation.

We present a simple theory for maximizable routing metrics. First, we give a formal definition of routing metrics and identify two important properties: boundedness and monotonicity. We show that these two properties are both necessary and sufficient for a routing metric to be maximizable in any network. We show how to combine two (or more) routing metrics into a single composite metric such that if the original metrics are both bounded and monotonic (and, hence, maximizable), then the composite metric is also bounded and monotonic (and, hence, maximizable). We present several applications of our theory. We show that the composite routing metric used in the inter-gateway routing protocol (IGRP) is not maximizable and we show that enhanced IGRP (EIGRP) does not behave as expected for nonmonotonic metrics. We also show that a technique for scalable link-state routing does not work correctly when applied to composite metrics. A common theme throughout the paper is that the intuitions generated by using distance metrics to produce shortest paths do not carry over to other routing metrics.

A key tree is a distributed data structure of security keys that can be used by a group of users. In this paper we describe how any user in the group can use the different keys in the key tree to securely multicast data to different subgroups within the group. The cost of securely multicasting data to a subgroup whose users are "consecutive" is O(log n) encryptions, where n is the total number of users in the group. The cost of securely multicasting data to an arbitrary subgroup is O(n/2) encryptions. However this cost can be reduced to one encryption by introducing an additional key tree to the group.

A computer network is said to provide hop integrity if, when any router, p, in the network receives a message, m, supposedly from an adjacent router, q, then p can check that m was indeed sent by q, was not modified after it was sent and was not a replay of an old message sent from q to p. We describe three protocols that can be added to the routers in a computer network so that the network can provide hop integrity, and thus overcome most denial-of-service attacks. These three protocols are a secret exchange protocol, a weak integrity protocol and a strong integrity protocol. All three protocols are stateless, require small overhead and do not constrain the network protocol in the routers in any way.

We generalize the concept of stabilization of computing systems. According to this generalization, the actions of a system S are partitioned into n partitions, called phase 1 through phase n. In this case, system S is said to be n-stabilizing to a state predicate Q iff S has state predicates P.0, ..., P.n such that P.0=true, P.n=Q, and the following two conditions hold for every j, 1/spl les/j/spl les/n. First, if S starts at a state satisfying P.(j-1) and if the only actions of S that are allowed to be executed are those of phase j or less, then S will reach a state satisfying P.j. Second, the set of states satisfying P.j is closed under any execution of the actions of phase j or less. By choosing n=1, this generalization degenerates to the traditional definition of stabilization. We discuss three advantages of this generalization over the traditional definition. First, this generalization captures many stabilization properties of systems that are traditionally considered nonstabilizing. Second, verifying stabilization when n>1 is usually easier than when n=1. Third, this generalization suggests a new method of fault recovery, called multiphase recovery.

The anti-replay window protocol is used to secure IP against an adversary that can insert (possibly replayed) messages in the message stream from a source computer to a destination computer in the Internet. We discuss this important protocol and point out a potential problem faced by the protocol, in which severe reordering of messages can cause the protocol to discard a lot of good messages. We then introduce a controlled shift mechanism that can reduce the number of discarded good messages by sacrificing a relatively small number of messages. We use simulation to show that the modified protocol is more effective than the original protocol when a severe reordering of messages occurs. In particular, we show that the modified protocol reduces the number of discarded good messages by up to 70%.

Many emerging web and Internet applications are based on a group communications model. Thus, securing group communications is an important Internet design issue. The key graph approach has been proposed for group key management. Key tree and key star are two important types of key graphs. Previous work has been focused on individual rekeying, i.e., rekeying after each join or leave request. In this paper, we first identify two problems with individual rekeying: inefficiency and an out-of-sync problem between keys and data. We then propose the use of periodic batch rekeying which can improve efficiency and alleviate the out-of-sync problem. We devise a marking algorithm to process a batch of join and leave requests. We then analyze the key server's processing cost for batch rekeying. Our results show that batch rekeying, compared to individual rekeying, saves server cost substantially. We also show that when the number of requests in a batch is not large, the best key tree degree is four; otherwise, key star (a special key tree with root degree equal to group size) outperforms small-degree key trees. Keywords: Secure group communications, group key management, rekeying. 1.

The anti-replay window protocol is used to secure IP against an adversary that can insert (possibly replayed) messages in the message stream from a source computer to a destination computer in the Internet. In this paper, we verify the correctness of this important protocol using standard methods (i.e. auxiliary variables, annotation, and invariants). We show that despite the adversary, the protocol delivers each message at most once, and discards a message only if another copy of this message has already been delivered, or the message has suffered a reorder of degree w or more, where w is the window size. We then develop another variation of this protocol that uses two windows of size w/2 each. This protocol delivers every message at most once, and discards a message only if another copy of this message has already been delivered, or the message has suffered a reorder of degree w+d or more, where d is the sum of current distances between successive windows in the protocol. We argue that the double-window protocol is more effective than the original single-window protocol.

A computer network is said to provide hop integrity iff when any router p in the network receives a message m supposedly from an adjacent router q, then p can check that m was indeed sent by q, was not modified after it was sent, and was not a replay of an old message sent from q to p. We describe three protocols that can be added to the routers in a computer network so that the network can provide hop integrity. These three protocols are a secret exchange protocol, a weak integrity protocol, and a strong integrity protocol. All three protocols are stateless, require small overhead, and do not constrain the network protocol in the routers in any way.

Many emerging network applications are based upon a group communications model. As a result, securing group communications, i.e., providing confidentiality, authenticity, and integrity of messages delivered between group members, will become a critical networking issue. We present, in this paper, a novel solution to the scalability problem of group/multicast key management. We formalize the notion of a secure group as a triple (U,K,R) where U denotes a set of users, K a set of keys held by the users, and R a user-key relation. We then introduce key graphs to specify secure groups. For a special class of key graphs, we present three strategies for securely distributing rekey messages after a join/leave and specify protocols for joining and leaving a secure group. The rekeying strategies and join/leave protocols are implemented in a prototype key server we have built. We present measurement results from experiments and discuss performance comparisons. We show that our group key management service, using any of the three rekeying strategies, is scalable to large groups with frequent joins and leaves. In particular, the average measured processing time per join/leave increases linearly with the logarithm of group size.

Obtaining feedback information regarding the state of receivers in a multicast session is a fundamental problem that often arises in collaborative multimedia systems. In this paper we present a generalized abstraction of the state feedback problem. Then, we present a feedback protocol that addresses some of the special cases that commonly arise. The presented feedback protocol is suitable for application in best-effort unreliable networks such as the Internet. It allows for obtaining the desired state feedback about a group of receivers, where each receiver may be in one of a set of finite states. The efficiency of the proposed protocol in eliminating the reply implosion problem is illustrated by simulation experiments.

Heartbeat protocols are used by distributed programs to ensure that if a process in a program terminates or fails, then the remaining processes in the program terminate. We present a class of heartbeat protocols that tolerate message loss. In these protocols, a root process periodically sends a beat message to every other process then waits to receive a reply beat message from every other process. If the root process does not receive a reply (possibly due to message loss), the root process reduces by half the period for sending beat messages. We show that in practical situations, the parameters of these protocols can be chosen to achieve a good compromise between three contradictory objectives: reduce the rate of sending beat messages, reduce the detection delay, and still keep the probability of premature termination small.

We develop a theory for deciding, for any routing metric and any network, whether the messages in this network can be routed along paths whose metric values are maximum. In order for the messages in a network to be routed along paths whose metric values are maximum, the network needs to have a rooted spanning tree that is maximal with respect to the routing metric. We identify two important properties of routing metrics: boundedness and monotonicity, and show that these two properties are both necessary and sufficient to ensure that any network has a maximal tree with respect to any (bounded and monotonic) metric. We also discuss how to combine two (or more) routing metrics into a single composite metric such that if the original metrics are bounded and monotonic, then the composite metric is bounded and monotonic. Finally we show that the composite routing metrics used in IGRP (inter-gateway routing protocol) and EIGRP (enhanced IGRP) are bounded but not monotonic.

Many emerging applications (e.g., teleconference, real-time information services, pay per view, distributed interactive simulation, and collaborative work) are based upon a group communications model, i.e., they require packet delivery from one or more authorized senders to a very large number of authorized receivers. As a result, securing group communications (i.e., providing confidentiality, integrity, and authenticity of messages delivered between group members) will become a critical networking issue.In this paper, we present a novel solution to the scalability problem of group/multicast key management. We formalize the notion of a secure group as a triple (U,K,R) where U denotes a set of users, K a set of keys held by the users, and R a user-key relation. We then introduce key graphs to specify secure groups. For a special class of key graphs, we present three strategies for securely distributing rekey messages after a join/leave, and specify protocols for joining and leaving a secure group. The rekeying strategies and join/leave protocols are implemented in a prototype group key server we have built. We present measurement results from experiments and discuss performance comparisons. We show that our group key management service, using any of the three rekeying strategies, is scalable to large groups with frequent joins and leaves. In particular, the average measured processing time per join/leave increases linearly with the logarithm of group size.

We present a scheduling protocol, called time-shift scheduling, to forward packets from multiple input flows to a single output channel. Each input flow is guaranteed a predetermined packet rate and an upper bound on packet delay. The protocol is an improvement over existing protocols because it satisfies the properties of rate-proportional delay, fairness, and efficiency, while existing protocols fail to satisfy at least one of these properties. In time-shift scheduling each flow is assigned an increasing timestamp, and the packet chosen for transmission is taken from the flow with the least timestamp. The protocol features the novel technique of time shifting, in which the scheduler's real-time clock is adjusted to prevent flow timestamps from increasing faster than the real-time clock. This bounds the difference between any pair of flow timestamps, thus ensuring the fair scheduling of flows.

The distance vector routing protocol satisfies the following property. If this protocol is used to route a sequence of data messages from a source to a destination, then these data messages will follow the same shortest-distance path from the source to the destination. In this paper, we show how to modify this protocol, without adding new messages, in order to satisfy the following load balancing property. If the modified protocol is used to route a sequence of data messages from a source to a destination, then these messages will be uniformly distributed over all k-monotonic paths from the source to the destination, i.e., over all paths whose distance to the destination never increases at each hop, and may remain constant in at most k hops. In particular, by choosing k to be zero, the modified protocol distributes the data messages over all shortest-distance paths from the source to the destination.

The authors propose replacing the real-time clock, used in scheduling protocols to determine the packet's arrival time to the multiplexor, by an event-driven, discrete clock. The multiplexor advances its discrete clock, at the start of serving any packet, by a value equal to the service time needed to serve that packet. The discrete clock is implemented in three different timestamping protocols. They prove that using discrete clock preserves the bounds on delay. They also illustrate the relations between the valve of the time-stamp based on a real-time clock, and the corresponding value based on discrete clock.

In new collaborative multimedia applications, there is a need for overall control, beyond the level of quality of service (QoS) as pertaining to individual streams in isolation of others. At every instant in time, the quality of the session, as perceived by the end user, depends on the priorities of the on-going streams, according to the application semantics, as well as on the actual QoS offered by the system to each of these streams. We introduce the concept of "Quality of Session" control. This is achieved by employing a monitoring mechanism for measuring the perceived QoS of each stream. In addition, in order to react to existing or potential bottlenecks in the network or end-systems, or skewness in the synchronization of views, an inter-stream adaptation mechanism is applied.

We present a family of group routing protocols for a network of processes. The task of these protocols is to route data messages to each member of a process group. To this end, a tree of processes is constructed in the network, ensuring that each group member is included in the tree. No processing or storage overhead is required for processes not included in the tree. The overhead of processes in the tree consists solely of the periodic exchange of request/reply messages with their parent. To choose the processes that constitute the tree, we take advantage of the existing unicast routing protocol in the network. In addition, our family of group routing protocols distinguishes itself from other group routing protocols in three ways. First, the protocols are proven correct. Second, the protocols preserve the integrity of the group tree as it adapts to changes in the unicast routing tables, even in the presence of temporary unicast routing loops. Third, data messages are propagated along the entire group tree, even while the tree adapts to changes in the unicast routing tables.

We develop a simple theory of flows to study the flow of data in real-time computing networks. Flow theory is based on discrete and nondeterministic mathematics, rather than the customary continuous or probabilistic mathematics. The theory features two types of flows: smooth and uniform, and eight types of flow operators. We prove that, if the input flow to any of these operators is smooth or uniform, then both the internal buffer and delay of that operator are bounded. Linear networks of flow operators are introduced, and their internal buffers and delays are derived from the internal buffers and delays of their constituent operators. We extend flow theory so that it can be used in analyzing cyclic networks and networks of multiflows. Since many rate-reservation protocols can be represented as linear networks of flow operators, we use flow theory to prove that a number of these protocols (stop-and-go, hierarchical round-robin, weighted fair queueing, self-clocking fair queueing, and virtual clock) require bounded buffering and introduce bounded delay.

The sentry of a concurrent program P is a program that executes concurrently with P, periodically takes snapshots of P, and issues a warning if it detects that some snapshot does not satisfy a predefined predicate. The sentry is unique among snapshot-taking systems in its low-overhead. First, the shared storage between the observed program P and the sentry is linear in the number of P variables that are being observed. Second, the observed program P never waits for the sentry. Third, the mutual exclusion between the observed program and the sentry is achieved without using any special hardware or software constructs. In this paper, we present a family of two sentries. One sentry can be used for taking snapshots of scalar variables (and can check whether these snapshots satisfy a given propositional predicate), and the other sentry can be used for taking snapshots of complex variables such as arrays (and can check whether these snapshots satisfy a given first-order predicate). We briefly describe a system prototype for automatically generating sentries for any given concurrent program, and present some encouraging empirical results that we obtained from this prototype.

We present a group routing protocol for a network of processes. The task of the protocol is to route data messages to each member of a process group. To this end, a tree of processes is constructed in the network, ensuring each group member is included in the tree. To build this tree, the group routing protocol relies upon the unicast routing tables of each process. Thus, group routing is a composition of a unicast routing protocol, whose detailed behavior is unknown but its basic properties are given, and a protocol that builds a group tree based upon the unicast routing tables. The design of the group routing protocol is presented in three steps. First, a basic group routing protocol is presented and proven correct. Then, the protocol is refined twice, strengthening its properties with each refinement. The final protocol has the property of adapting the group tree to changes in the unicast routing tables without compromising the integrity of the group tree, even in the presence of unicast routing loops.

We present a scheduling protocol, called time-shift scheduling, to forward data packets from multiple input flows to a single output channel. Each input flow is guaranteed a predetermined forwarding rate and an upper bound on packet delay. The protocol is an improvement over existing protocols because it satisfies the properties of low delay, fairness, and efficiency, while existing protocols fail to satisfy at least one of these properties. In time-shift scheduling, each flow is assigned an increasing timestamp, and the packet chosen for transmission is taken from the flow with the least timestamp. The protocol features the novel technique of time shifting, in which the scheduler's real-time clock is adjusted to prevent flow timestamps from increasing faster than the real-time clock. This bounds the difference between any pair of flow timestamps, thus ensuring the fair scheduling of flows.

A self-stabilizing algorithm is silent if it converges to a glc)bal state after which the values stored in the communication registers are fixed.The silence property of self-stabilizing algorithms is a desirable property in terms of simplicity and communication overhead.In this work we show that no constant memory silent self-stabilizing algorithms exist for identification of the centers of a graph, leader election, and spanning tree construction.Lower bounds of Cl(log n) bits per communication register are obtained for each of the above tasks.The existence of a silent legitimate global state that uses less than log n bits per register is assumed.This legitimate global state is used to construct a silent global state that is illegitimate.

We develop an asymmetric protocol for wireless communication in a step-by-step manner. We start with a very simple protocol and prove its correctness. Then we relax the assumptions of the simple protocol one by one, verifying the correctness of the protocol at each step as we relax the assumptions. This process is continued in a systematic manner until no assumptions are left. The novelty of the paper lies in the way the assumptions are relaxed without violating the correctness properties of the protocol while at the same time making the protocol efficient. The final result is a provably correct protocol which is also efficient for wireless channels.

In the past decade the United States telecommunications industry has been under much scrutiny as a result of a number of major network outages. These outages, which affected millions of customers, ranged from power and fire related problems to a software error affecting the common channel signaling network. The industry reacted promptly and positively. This paper discusses the actions of the FCC's Network Reliability Council (NRC), including the technical papers produced by this group and its newly re-chartered objectives, as well as the Alliance for Telecommunications Industry Solutions (ATIS) Network Reliability Steering Committee (NRSC) to address this challenge. The NRSC's findings are discussed in detail, including the results of its quarterly and annual reports, which identify trends, areas of concern, and recommended steps to prevent or mitigate outages in the future.

Abstract The sentry of a concurrent program P is a program that observes the execution of P, and issues a warning if P does not behave correctly with respect to a given set of logical properties (owing to a programming error or a failure). The synchronization between the program and sentry is such that the program never waits for the sentry, the shared storage between them is very small (in fact linear in the number of program variables being observed), and the snapshots read by the sentry are consistent. To satisfy these three requirements, some snapshots may be overwritten by the program before being read by the sentry. We develop a family of algorithms that preserve these requirements for properties involving scalar variables, then extend the algorithms to permit the observation of large data structures without additional overhead. We describe in detail the annotation language with which the properties can be expressed, and a prototype system that we have implemented to generate the sentry automatically for any given concurrent C program. Finally, we present experimental results that show that the overhead incurred by the sentry is on average no worse than ten per cent for snapshots of up to six variables, and that the loss of snapshots prevents the sentry's detection of an single violation in less than four per cent of the cases. Recurring errors are detected at a rate of 100 per cent.

We present an elegant protocol for reliably transmitting data messages from a sender to a receiver over a highspeed network that may reorder, lose, or corrupt messages. The protocol is based on a new principle that calls for the periodic exchange of state information between the sender and receiver. Our formal definition of the protocol is abstract and does not include explicit timing information such as the rate of sending state information. The abstract definition makes our formal verification of the protocol simple and based solely on well-established concepts: invariants, well-foundedness, and action fairness. We use the formal definition of the protocol and its proof of correctness to deduce the required timing information. In particular, we show that the rate of sending state information is at most (m-1)/2T where m is a measure of the memory size in the sender, and T is an upper bound on the required time for one message to be sent, propagated, and received between the sender and receiver.>

We present a method for the design of nonmasking fault-tolerant programs. In our method, a set of constraints is associated with each program. Each of these constraints is continually satisfied under the execution of program actions, as long as faults do not occur. Whenever some of the constraints are violated, due to certain faults, all constraints are eventually reestablished by subsequent execution of the program actions. To design programs thus, two types of program actions are distinguished: "closure" actions and "convergence" actions. Closure actions are the actions that perform the intended computation of the program when all of the constraints are satisfied. Convergence actions are the actions that reestablish the constraints when they have been violated. Sufficient conditions for the validation of closure and convergence actions are formalized in terms of a "constraint graph". These conditions are illustrated by designing nonmasking fault-tolerant programs for diffusing computations, atomic actions, and token rings.>

We describe a purely declarative method for introducing modularity into forward-chaining, rule-based languages and its embodiment in the Venus rule language. The method is enforced by the syntax of the language and includes the ability to parameterize the rule groups. Drawing from two of three Venus applications developed to date, we illustrate how this form of modularity contributes directly to the resolution of certain software engineering problems associated with rule languages.>

We present a construction of a single-writer, multiple-reader atomic register from single-writer, single-reader atomic registers. The complexity of our construction is asymptotically optimal; O(M 2 + MN) shared single-writer, single-reader safe bits are required to construct a single-writer, M-reader, N-bit atomic register.

A reset subsystem is designed that can be embedded in an arbitrary distributed system in order to allow the system processes to reset the system when necessary. Our design is layered, and comprises three main components: a leader election, a spanning tree construction, and a diffusing computation. Each of these components is self-stabilizing in the following sense: if the coordination between the up-processes in the system is ever lost (due to failures or repairs of processes and channels), then each component eventually reaches a state where coordination is regained. This capability makes our reset subsystem very robust: it can tolerate fail-stop failures and repairs of processes and channels, even when a reset is in progress.>

The authors develop a simple theory of flows and show how to use this theory in verifying rate-reservation protocols in computing networks. The theory is based on discrete and nondeterministic mathematics, rather than the customary continuous or probabilistic mathematics. The theory features two types of flows, smooth and uniform, and four types of flow operators, limiters, compactors, expanders, and filters. Many rate-reservation protocols can be represented as linear networks of these flow operators. It is proved that, if the input flow to any of these networks is smooth or uniform, then the internal buffer and the delay in each operator in the network are bounded. This method is used to prove that a number of rate-reservation protocols (for example, stop-and-go, hierarchical round-robin, fair queuing and virtual clock) require bounded buffering and introduce bounded delay.>

The authors formally define what it means for a system to tolerate a class of faults. The definition consists of two conditions. The first is that if a fault occurs when the system state is within the set of legal states, the resulting state is within some larger set and, if faults continue to occur, the system state remains within that larger set (closure). The second is that if faults stop occurring, the system eventually reaches a state within the legal set (convergence). The applicability of the definition for specifying and verifying the fault-tolerance properties of a variety of digital and computer systems is demonstrated. Using the definition, the authors obtain a simple classification of fault-tolerant systems. Methods for the systematic design of such systems are discussed.>

Unbounded and bounded designs of asynchronous unison systems are discussed. It is shown that both systems are stabilizing in the sense that their steady state behaviors do not depend on their initial states. The systems can therefore tolerate memory and reconfiguration faults that may yield them in arbitrary states. It is also shown that unison systems are useful in designing multiphase systems.>

A system that observes the execution of each loop in any given sequential program and issues a warning if some loop execution does not terminate as expected (due to a programming error or a failure) is proposed. At each iteration of a loop execution, the program writes the current values of some variables into shared storage; these values are read later by another program called the sentry. The sentry uses these values to compute the loop's termination function at the current iteration, and issues a warning if successive values of the termination function are not monotonically decreasing. The shared storage between the program and the sentry is finite, the program never waits for the sentry during execution, and some form of mutual exclusion is achieved between the program and the sentry. Extensions of the system and an implementation of a prototype are described.>

Abstract Most proof methods for reasoning about concurrent programs are based upon the interleaving semantics of concurrent computation: a concurrent program is executed in a stepwise fashion, with only one enabled action being executed at each step. Interleaving semantics, in effect, requires that a concurrent program be executed as a nondeterministic sequential program. This is clearly an abstraction of the way in which concurrent programs are actually executed. To ensure that this is a reasonable abstraction, interleaving semantics should only be used to reason about programs with “simple” actions; we call such programs “atomic”. In this paper, we formally characterise the class of atomic programs. We adopt the criterion that a program is atomic if it can be implemented in a wait-free, serialisable manner by a primitive program. A program is primitive if each of its actions has at most one occurrence of a shared bit, and each shared bit is read by at most one process and written by at most one process. It follows from our results that the traditionally accepted atomicity criterion, which allows each action to have at most one occurrence of a shared variable, can be relaxed, allowing programs to have more powerful actions. For example, according to our criterion, an action can read any finite number of shared variables, provided it writes no shared variable.

A communication protocol is stabilizing if and only if starting from any unsafe state (i.e. one that violates the intended invariant of the protocol), the protocol is guaranteed to converge to a safe state within a finite number of state transitions. Stabilization allows the processes in a protocol to reestablish coordination between one another whenever coordination is lost due to some failure. The authors identify some important characteristics of stabilizing protocols; they show in particular that a stabilizing protocol is nonterminating, has an infinite number of safe states, and has timeout actions. They also propose a formal method for proving protocol stabilization: in order to prove that a given protocol is stabilizing, it is sufficient (and necessary) to exhibit and verify what is called a 'convergence stair' for the protocol. Finally, they discuss how to redesign a number of well-known protocols to make them stabilizing; these include the sliding-window protocol and the two-way handshake.>

A window protocol based on the block acknowledgment method, in which acknowledgment message has two numbers, m and n, to acknowledge the reception of all data messages with sequence numbers ranging from m to n, is discussed. In the window protocol, message sequence numbers are taken from a finite domain and both message disorder and loss can be tolerated. An initial version of the protocol that uses a simplified timeout action and unbounded sequence numbers is presented, the simplified timeout action in the protocol is replaced by a sophisticated one without disturbing the protocol's correctness, and the unbounded sequence numbers are replaced by bounded ones while preserving the protocol's correctness. Remarks concerning other variations of the protocol are also presented.>

An adaptive program is one that changes its behavior base on the current state of its environment. This notion of adaptivity is formalized, and a logic for reasoning about adaptive programs is presented. The logic includes several composition operators that can be used to define an adaptive program in terms of given constituent programs; programs resulting from these compositions retain the adaptive properties of their constituent programs. The authors begin by discussing adaptive sequential programs, then extend the discussion to adaptive distributed programs. The relationship between adaptivity and self-stabilization is discussed. A case study for constructing an adaptive distributed program where a token is circulated in a ring of processes is presented.>

We describe a new version of the window protocol where message sequence numbers are taken from a finite domain and where both message disorder and loss can be tolerated. Most existing window protocols achieve only one of these two goals. Our protocol is based on a new method of acknowledgement, called block acknowledgement, where each acknowledgement message has two numbers m and n to acknowledge the reception of all data messages with sequence numbers ranging from m to n. Using this method of acknowledgement, the proposed protocol achieves the two goals while maintaining the same data transmission capability of the traditional window protocol.

Presents a novel class of mutual exclusion systems, in which processes circulate one token, and each process enters its critical section when it receives the token. Each system in the class is self-stabilizing; i.e. it it starts at any state, possibly one where many tokens exist in the system, it is guaranteed to converge to a good state where exactly one token exists in the system. The systems are better than previous systems in that their state transitions are noninterfering; i.e., if any state transition is enabled at any instant, then it will continue to be enabled until it is executed. This makes the systems easier to implement as delay-insensitive circuits.>

We present two protocols for information exchange between multiple identical senders and a single receiver. At each instant, every sender sends one bit, and the bits from all of senders are or-ed together into one bit before being received by the receiver. If a sender has a data message to send, it sends the message bits one by one; otherwise it sends zero bits. Clearly, if the sending of two messages by two senders overlap, then the resulting “collision” can result in a corrupted message, i.e., one that was not sent by either sender. The function of the protocol is to deliver those and only those messages that are not corrupted by collision. (In other words, the receiver acts as a discriminating seine that catches and delivers only uncorrupted messages; hence the title.) The two protocols presented here are based on Manchester codes and general balanced codes, respectively.

A new construction of a l-writer/m-reader/nbit atomic register using O(m2 + mn) lwriter/l-reader/I-bit atomic registers is presented.This construction is more efficient, i.e, uses less registers, than previous constructions. IntroductionThe currently accepted theory of concurrent computing is deeply rooted in the concept of

Consider a network of communicating finite state machines that exchange messages over unbounded FIFO channels. Each machine in the network can be defined by a directed graph whose nodes represent the machine states and whose edges represent its transitions. In general, for a node in one of the machines to be live (i.e., encountered infinitely often during the course of communication), each machine in the network should progress in some fair fashion. We define three graduated notions of fair progress (namely, node fairness, edge fairness, and network fairness), and on this basis we define three corresponding degrees of node liveness. We discuss techniques to verify that a given node is live under each of these fairness assumptions. These techniques can be automated; and they are effective even if the network under consideration has an infinite number of reachable states. We use our techniques to establish the liveness of some practical communication protocols; these include an unbounded start-stop protocol, an unbounded alternating bit protocol, and a simplified version of the CSMA/CD protocol for local area networks.

We illustrate the usefulness of communicating finite state machines in modeling a number of physical layer protocols that include (i) an asynchronous start-stop protocol and (ii) a protocol for synchronous transmission with modems. Each protocol is modeled as a network of four finite state machines that communicate by exchanging messages over unbounded, FIFO channels. (Two machines are used to model the protocol itself, while the other two are used to model its interface to the upper data link protocol in the protocol hierarchy.) We outline a methodology to verify communication boundedness and progress for each protocol model. The methodology is based on three techniques that were proposed earlier to verify networks of communicating finite state machines; they are network decomposition, machine equivalence, and closed covers.

Consider a network of two communicating finite state machines which exchange messages over two one-directional, unbounded channels, and assume that each machine receives the messages from its input channel based on some fixed (partial) priority relation. We address the problem of whether the communication of such a network is deadlock-free and bounded. We show that the problem is undecidable if the two machines exchange two types of messages. The problem is also undecidable if the two machines exchange three types of messages, and one of the channels is known to be bounded. However, if the two machines exchange two (or less) types of messages, and one channel is known to be bounded, then the problem becomes decidable. The problem is also decidable if one machine sends one type of message and the second machine sends two (or less) types of messages; the problem becomes undecidable if the second machine sends three types of messages. The problem is also decidable if the message priority relation is empty. We also address the problem of whether there is a message priority relation such that the priority network behaves like a FIFO network. We show that the problem is undecidable in general, and present some special cases for which the problem becomes decidable.

We discuss how to model a synchronous protocol (due to Aho, Ullman, and Yannakakis) using communicating finite state machines, and present a proof for its safety and liveness properties. Our proof is based on constructing a labeled finite reachability graph for the protocol. This reachability graph can be viewed as a sequential program whose safety and liveness properties can be stated and verified in a straightforward fashion.

Many communication protocols can be observed to go through different phases performing a distinct function in each phase. A multiphase model for such protocols is presented. A phase is formally defined to be a network of communicating finite-state machines with certain desirable correctness properties; these include proper termination and freedom from deadlocks and unspecified receptions. A multifunction protocol is constructed by first constructing separate phases to perform its different functions. It is shown how to connect these phases together to realize the multifunction protocol so that the resulting network of communicating finite state machines is also a phase (i.e., it possesses the desirable properties defined for phases). The modularity inherent in multiphase protocols facilitates not only their construction but also their understanding and modification. An abundance of protocols have been found in the literature that can be constructed as multiphase protocols. Three examples are presented here: two versions of IBM's BSC protocol for data link control and a token ring network protocol.

We model a systolic array as a network of, mostly identical, communicating finite state machines that exchange messages over one-to-one, unbounded, FIFO channels. Each machine has a cyclic behavior; in each cycle, a machine first receives one message from each of its input channels, then sends one message to each of its output channels. If in a cycle a machine does not have any data message to send to one of its output channels, it sends a null message instead; thus, machines exchange two types of messages, data and null. We characterize the liveness and termination properties for such networks, and discuss two algorithms that can be used to decide these properties for any given network. We apply these algorithms to establish the liveness and termination properties of four systolic array examples. These examples include a linear matrix-vector multiplier, a linear priority queue, and a search tree.

Consider a network of communicating finite state machines that exchange messages over unbounded, FIFO channels. Each machine in this network has a finite number of states (called nodes), and state transitions (called edges), and can be defined by a labelled directed graph. A node in one of the machines is said to be “live” iff it is reached by its machine infinitely often during the course of communication, provided that the machines behave in some “fair” fashion. We discuss a technique to verify that a given node is live in such a network. This technique can be automated, and is effective even if the network under consideration is unbounded (i.e. has an infinite number of reachable states). We use our technique to establish the liveness of three distributed solutions to the mutual exclusion problem.

A multidatabase system provides a logically integrated view of existing, possibly inconsistent, databases. Logical integration is achieved primarily through the use of generalization, which can be modelled algebraically as a sequence of outerjoin and aggregation operations. Conventional distributed query processing techniques are inadequate for processing queries over views defined by outerjoins and aggregates. In a conventional distributed database system, selections and projections are inexpensive to process; hence joins have been the rocus of most previous research. In a multidatabase system, however, even selections and projections can be as expensive as joins. The semiouterjoin operation can potentially reduce query processing costs. In general, there may be many different strategies based on semiouterjoins for processing a given query. The query optimization problem is to choose the most profitable of these strategies. This paper studies the query optimization problem for selection and projection queries. It develops linear-time solutions to the problem, and then extends these solutions to provide heuristics for joins and conjunctive queries.

We discuss an efficient variation of state exploration for two communicating finite state machines. In particular, we propose to divide the task of generating all reachable states into two independent subtasks. In each subtask, only the states reachable by forcing maximal progress for one machine are generated. Since the two subtasks are completely independent, and since in most instances the time and storage requirements for each subtask are less than those for the original task, maximal Progress state exploration can save time and/or storage over conventional state exploration.

We present a methodology to synthesize two communicating finite-state machines which exchange messages over two one-directional, FIFO channels. The methodology consists of two algorithms. The first algorithm takes one machineM, and constructs two communicating machinesM'andN'such that 1)M'is constructed fromMby adding some receiving transitions to it, and 2) the communication betweenM'andN'is bounded and free from deadlocks, unspecified receptions, nonexecutable transitions, and state ambiguities. The second algorithm takes the two machinesM'andN'which result from the first algorithm, and computes the smallest possible capacities for the two channels between them. Both algorithms require anO(st)time, wheresis the number of states in the given machineM, andtis the number of state transitions inM; thus, the methodology is practical to use.

Consider communicating finite state machines which exchange messages over unbounded FIFO channels. We discuss a technique to verify that the communication between a given pair of such machines will progress indefinitely; this implies that the communication is free from deadlocks and unspecified receptions. The technique is based on finding a set of global states for the communicating pair such that the following two conditions (along with other conditions) are satisfied: 1) the initial global state is in that set; and 2) starting from any global state in that set, an ``acyclic version'' of the communicating pair must reach a global state in that set. We call such a set a closed cover, and show that the existence of a closed cover for a communicating pair is sufficient to guarantee indefinite communication progress. We also show that in many practical instances, if the communication is guaranteed to progress indefinitely, then the existence of a closed cover is necessary.

LetMandNbe two communicating finite state machines which exchange one type of message. We develope a polynomial algorithm to detect whether or notMandNcan reach a deadlock. The time complexity of the algorithm isO(m^{3}n^{3}and its space isO(mn)wheremandnare the numbers of states inMandN, respectively. The algorithm can also be used to verify that two communicating machines which exchange many types of messages are deadlock-free.

Semijoin strategies are a technique for query processing in distributed database systems. In the past, methodologies for constructing minimum communication-cost strategies for solving tree queries have been developed. These assume point-to-point communication and ignore local processing costs and the limited communication capacity of the system. In this paper, query processing in bus or loop systems is considered. The definition of strategy is extended to allow for broadcast mode of communication. We then address the problem of finding the minimum response-time schedule for executing a given strategy in an m-bus system taking into account local processing and system capacity. It is shown that the problem is computationally intractable for general tree queries, even in a 1-bus system, and for special classes of tree queries in an m-bus system. However, there is a polynomial-time algorithm for simple queries in a 1-bus system.