Towards a Formal Specification of the Spread Group Communication System

This work is supported by:
the DARPA FTN Project Composable Formal Models for High-Assurance Fault Tolerant Networks and
the ONR MURI Project CONTESSA.

Keywords: Group Communication System, Spread, Extended Virtual Synchrony Semantics, Failure Atomicity, Formal Specification, Secure Group Communication

The Spread group communication system (see Spread web page) emerged from the work on Transis and Totem and has been designed to cope with node failure and network partitions. To this end the semantics of extended virtual synchrony (also called failure atomicity) has been extended to deal with the case of network partitions. In addition, Spread provides different levels of service with different reliability and ordering gurantees: Messages can be reliable, fifo, causally ordered, totally ordered (also called agreed), or safe, where the later means that messages are only delivered if it is known that everybody in the group has actually received it. Stronger properties such as virtual synchrony and security are achieved at higher layers by Flush Spread and Secure Spread (see Secure Spread web page). The later is built upon the Cliques toolkit (see Cliques web page ) which we have specified as an independent component (see this link).

Our effort to develop a formal specification of Spread is based on the references below, the Spread source code, and discussions with the Spread team. An important goal is to obtain a mathematically satisfactory and conceise description that abstracts from implementation specific aspects and covers the most general behaviour that an application of Spread can observe. All this is done in a modular way so that different layers can be specified independently and composed at the specification level.

The current state of our specification is available below, but please note that it is a snapshot of ongoing work and still incomplete regarding various aspects.

In the CONTESSA project this specification is used as a basis for our work on Adaptive Group Communication.

Relevant References:

1. Yair Amir: Replication Using Group Communication Over a Partitioned Network, Ph.D. thesis, Hebrew University of Jerusalem, 1995. Available here .
2. Louise E. Moser, Yair Amir, P. Michael Melliar-Smith and Deborah A. Agarwal: Extended Virtual Synchrony The 14th IEEE International Conference on Distributed Computing Systems (IC-DCS), pages 56-65, June 1994. Available here .
3. John Schultz: Partitionable Virtual Synchrony Using Extended Virtual Synchrony, Masters Thesis, Masters Thesis, Johns Hopkins University, 2001. Available here .
4. Yair Amir and Jonathan Stanton: The Spread Wide Area Group Communication System, Technical Report CNDS-98-4. Available here .
5. Y. Amir, Y. Kim, C. Nita-Rotaru, J. Schultz, J. Stanton, G. Tsudik: Secure Group Communication Using Robust Contributory Key Agreement. IEEE Transactions on Parallel and Distributed Systems archive, pp. 468 - 480, 15(5), IEEE Press, 2004.
6. S. Gutierrez-Nolasco, N. Venkatasubramanian, M.-O. Stehr, and C. Talcott: Exploring Adaptability of Secure Group Communication using Formal Prototyping Techniques. In Proceedings of the 3rd Workshop on Reflective and Adaptive Middleware (RM2004). October 19, 2004, Toronto, Ontario, Canada. To appear in ACM Digital Library. Paper available in ps and pdf. Extended version available here.

Presentations:

1. Formal Specification of Group Communication Middleware, Workshop on Context Sensitive Systems Assurance (Contessa'03), April 1, 2003, Philadelphia. Slides available here: ps pdf.
2. Composable Formal Models for High-Assurance Fault Tolerance Networks, FTN PI Meeting, July 21-23, 2003, Honolulu, Hawaii. Slides available here: ps pdf.

The Formal Specification in Maude 2.0 (available here) can be found here.
This package contains the following files:

• README: instructions on how to run the examples
• Common data types and operations
  • natutil.maude --- natural number and operations
  • proc.maude --- processes (Spread daemons)
  • agent.maude --- agents (potential clients)
  • group.maude --- logical groups
  • state.maude --- distributed system state
  • mode.maude --- message delivery modes
• Spread configuration layer:
  • conf.maude --- configurations, i.e. instances of process membership in connected component
  • cmessage.maude --- configuration layer messages
  • constraints.maude --- delivery constraints
  • capi.maude --- configurational level API
  • ccommon.maude --- common for the following two modes
  • coperational.maude --- normal operational mode
  • cchange.maude --- transitional mode
  • cspread.maude --- combined configurational layer specification
• Spread group layer:
  • view.maude --- views, i.e instances of agent membership in groups
  • gmessage.maude --- group layer messages
  • gapi.maude --- group layer API (official Spread API)
  • spread.maude --- combined group layer specification (official Spread)
• Flush Spread layer:
  • fmessage.maude --- flush layer messages
  • fapi.maude --- flush layer API
  • flushspread.maude --- combined Flush Spread specification
• Secure Spread layer:
  • cliques.maude --- Cliques toolkit specification
  • smessage.maude --- secure layer messages
  • sapi.maude --- secure layer API
  • groupvar.maude --- group specific variables
  • securespread.maude --- combined Secure Spread specification
• Load all layers (Spread, Flush Spread, and Secure Spread):
  • all.maude
• Controlling the Execution:
  • controller.maude --- a simple controller language
  • test.maude --- prelude for configuration layer testing
  • gtest.maude --- prelude for group layer testing
  • ftest.maude --- prelude for flush layer testing
  • stest.maude --- prelude for secure layer testing
• Examples using Spread configuration layer:
  • test1.maude result: test1.out
  • test2.maude result: test2.out
  • test3.maude result: test3.out
  • test4.maude result: test4.out
  • test5.maude result: test5.out
  • test6.maude result: test6.out
  • test7.maude result: test7.out
  • test8.maude result: test8.out
  • test9.maude result: test9.out
  • test10.maude result: test10.out
  • test11.maude result: test11.out
  • test12.maude result: test12.out
  • test13.maude result: test13.out
  • test14.maude result: test14.out
  • test15.maude result: test15.out
• Examples using Spread group layer:
  • gtest1.maude result: gtest1.out
  • gtest2.maude result: gtest2.out
  • gtest3.maude result: gtest3.out
  • gtest4.maude result: gtest4.out
  • gtest5.maude result: gtest5.out
• Examples using Spread flush layer:
  • ftest1.maude result: ftest1.out
  • ftest2.maude result: ftest2.out
  • ftest3.maude result: ftest3.out
  • ftest4.maude result: ftest4.out
• Examples using Spread secure layer:
  • stest1.maude result: stest1.out
  • stest2.maude result: stest2.out
  • stest3.maude result: stest3.out
  • stest4.maude result: stest4.out

• README2: list of files in this package
• refs.txt: references
• lessons.txt: discussion of the issues raised and lessons learned
• overview.txt: overview of the Spread configuration level model
• conf-layer-ax.txt: properties of the configuration layer
  Auxiliary documents:
  • actions.txt: high-level state diagram for configuration layer and details of the event partial order abstraction
  • prop.txt: properties of reachable states and computation paths
  • conf-layer-extra.txt: argument details for properties stated in conf-layer-ax.txt
• group-layer-ax.txt: properties of the group layer