[13]   

We are investigating how secure and reliable distributed systems can be constructed and verified through a combination of approaches ranging from systems architectures and programming languages to formal methods. In order to experiment with these approaches, we have developed a group communication toolkit called Ensemble. Groups of application processes use communication protocols provided by Ensemble in order to coordinate distributed actions in a secure and reliable fashion. Ensemble's design combines a flexible, layered protocol architecture and a high-level programming language in order to enable the use of formal methods to verify its security and reliability properties.

Ensemble uses a layered protocol architecture which is important both for providing flexibility in designing survivable systems as well as for decomposing high-level protocols into small protocol layers that are amenable to verification. As with its predecessor system, Horus, Ensemble uses collections of small protocol layers that are composed to provide high-level properties to groups of processes. The exact set of protocols can be chosen by the application at run time, and then can be changed on-the-fly as an application's needs evolve. For instance, various sets of protocols provide different forms of reliability for groups. There are a range of properties that can be provided for message delivery and for the reconfiguration of the system when failures occur. There are also a variety of security protocols from which applications can choose for encrypting messages and controlling admission to groups. The different security protocols support different forms of authentication and privacy. The layered architecture allows these layers to be configured in different ways in order to match the needs of a wide range of applications.

In addition to leveraging off its layered architecture, Ensemble also benefits from the use of a high-level programming language. Ensemble is implemented in a dialect of the ML programming language, Objective Caml, which has many features useful for our work. These include strong static type checking, automatic memory management, and message marshaling. Programs can automatically linearize (or marshal) ML data structures into sequences of bytes to send over communication networks. These features have combined to encourage good system design and to expose the structure of Ensemble protocols. Through this improved structuring, we have been able to decompose protocol layers more thoroughly than in Ensemble's predecessor, Horus, which was written in C. For instance, the group membership protocol in Horus is a single layer of more than 5000 lines of C. In Ensemble, this layer has been decomposed into 7 layers that have a total of less than 1600 lines of ML.

Implementation in a high-level language and the decomposition of protocols into small layers is crucial to our end-goal of "hardening" Ensemble with formal methods. Small protocol layers tend to be easier to verify. In addition, the use of ML supports importing of layers into theorem provers for verification. We are currently experimenting with such verification. Our approach is to import protocol layers into the Nuprl theorem prover along with specifications of the properties of the layers. These properties are then either partially or fully verified using specially written proof programs ("tactics") in Nuprl. This work leverages Ensemble's layered architecture heavily, which allows small protocols to be verified independently and thereby makes the verification feasible.

In addition to the directions described above, we are also investigating other issues in building survivable systems. In work with members of the Transis group at Hebrew University, we are examining implementing new security protocols with stronger properties, such as protecting against Byzantine failures in group members. We are also examining ways to structure communication across multiple groups in order to provide multi-level security. Interestingly, the support we have built into Ensemble for verification also appears to allow optimizations to be carried out by Nuprl. Experiments have shown that these optimizations dramatically improve the performance of Ensemble protocols.

In summary, we are combining approaches based on modular systems architectures, high-level programming languages, and verification tools in order to arrive at flexible, reliable, and secure distributed systems.

This is joint work with Ken Birman, Robert Constable, Jason Hickey, Christoph Kreitz, and Robbert vanRenesse. Ensemble was developed as part of the Horus group at Cornell. Further information about Ensemble, including a freely available software distribution, can be found at:
< http://www.cs.cornell.edu/Info/Projects/HORUS/Overview.html>

Back to the Table of Contents
   [13]