Assuring the Integrity of Highly Decentralized Communications Systems

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

Principal Investigators

Links to assured integrity places of interest

Recent Highlights

Part of our work has been the application of formal methods to the design and verification of adaptive protocols in Ensemble. We have developed and released a new formal tool, the Nuprl Open Logical Programming Environment (LPE), that enables the cooperation of state-of-the-art proof systems. Within the LPE we have created a basic library of facts about Ensemble that are formally stated and proved. These serve as the basis of specification of problems and verification of designs.

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.

General Research and Development Goals and Demonstrations for 2000-2001

General Introduction and Papers

Back to main