This second part of our effort is a follow-on to our prior project, the Ensemble System. The Ensemble System is a high performance, reconfigurable, compositional network protocol architecture. Modules from a large collection of micro-protocols can be stacked and restacked in a variety of ways, allowing applications to adapt, at run time, to changes in network bandwidth and latency, to processor and network failures, to changing security requirements, etc. The system is used to support fault-tolerant applications and applications requiring group keys for security. Ensemble is able to dynamically adapt when failures or other environmental problems occur, while continuously guaranteeing the critical properties on which applications depend.
In this effort, we are working on the use of automated theorem proving tools to confirm that Ensemble satisfies the reliability properties needed by its users. For example, suppose that an application depends upon Ensemble to manage a security key, which is updated as membership in the application changes over time. Our confidence in this key depends on the correctness of the Ensemble protocols for dealing with membership changes, failures, recoveries, and refreshing the key at request of the application. All told, the Ensemble protocol stack solving such a problem might consist of 20 to 25 thousand lines of code.
Our project is automating the analysis and correctness proof process for such protocols, and developing a general methodology for proving properties of systems build by composition of layers. We are developing general techniques to solve this problem, applying them to Ensemble and its virtual synchrony tools, and hope to reach the point where we can compile an objective, such as a specialized security rule, directly into executable, provably correct code at the touch of a button, download it dynamically, and start running the protocol in a system that is already in active use.
|
| DARPA Quad Chart |
During the past year we have applied the formal tools to the verification of Ensemble's total order protocol. This work is based on the internal models of Ensemble that have been used in previous results from our group on stack compression to improve performance. We have also built internal models of the automata that are used as specifications. Using these internal models, we have been able to automate a considerable amount of the work needed to verify protocols against their specifications using formal automata. The automated tools are now being used in the design of new adaptive protocols. Ensemble includes several different protocols that provide the same services (such as total ordering). Each protocol is best under some network conditions and we would like to develop adaptive protocols that monitor network traffic and automatically switch to the most efficient implementation of a service.
General switching protocols are complex, but for certain classes of services there are simple, efficient switching protocols. We characterize a service by the property of the network history that it guarantees. We have used our formal tools to define a class of properties that we call memoryless and have proved that memoryless properties that also have certain meta-properties are preserved by any switching protocols that maintain a certain invariant. This work provides a theoretical basis for a rigorous design method for adaptive protocols. We have used the method to create a prototype implementation of a switching protocol that preserves the total ordering property.