Modeling and Analyzing Protocols in Maude and
Real-Time Maude Tutorial

Peter C. Olveczky (Univ. of Illinois at Urbana-Champaign and Univ. of Oslo)

Slides for SBLP 2004 talk, May 27th (pdf)

Slides for Real-Time Maude tutorial, May 31st and June 1st (pdf for day 1, pdf for day 2)

Abstract

Communication protocols are high-level descriptions of distributed computer systems, and include broadcast and multicast protocols, database protocols, and security protocols. Such protocols are notoriously hard to design and understand due to nondeterminism and reactivity. One notable example is the Needham-Schroeder public-key (NSPK) authentication protocol, a security protocol usually described in three lines, which was widely used and cited for almost 20 years before its fatal flaws were discovered.

It is important to understand and analyze protocols, since it is well known that errors in a software system should be discovered as early as possible in the software development process. Protocols are often described informally using plain text or UML- and C-like notation. Such specifications are usually ambiguous, hard to test and reason about, and usually contain crucial unstated assumptions.

Formal (i.e. logic-based) methods have been advocated to ameliorate this situation by providing specification formalisms in which protocols can be described, so that the meaning of the protocol is clear, so that it is possible to reason about the consequences of the protocol, and so that the protocol can be tested and analyzed automatically. Traditionally, formal methods have been met with some skepticism because:

• some specification formalisms can be non-intuitive and mathematically difficult,
• sometimes different formalisms are needed to describe different kinds of protocols, or different protocol parts,
• flaky and ever-changing tool support, and/or
• belief that formal methods are all about program (or protocol) verification, which is arguably a very hard task.

Nevertheless, the acceptance of formal methods in industry has increased lately, because of

• the increasing maturity of formal methods and tools,
• better understanding of where, when, and what kind of formal analysis is feasible,
• an increasing number of success stories in the use of formal methods, and
• the complexity, cost, and criticality of modern computer systems.

Maude is a widely used state-of-the-art formal specification language and tool, and has been shown to be well suited to specify and analyze a wide array of sophisticated communication protocols.

The Maude specification language emphasizes ease and generality of specification. The language is intuitive and flexible, in which many different kinds of systems and system parts can be naturally specified. In particular, distributed systems can be naturally specified in an object-oriented way.

Maude specifications are executable, and the Maude rewrite engine is high-performance tool which can perform millions of rewrites per second. The tool supports a wide range of increasing stronger formal methods for automatically analyzing Maude specifications, including

1. symbolic simulation for prototyping purposes, in which one possible behavior of the system is simulated,
2. search for certain states reachable from the initial state,
3. in case the state space reachable from the initial state is finite, one can use Maude's efficient linear temporal logic model checker to analyze all behaviors from the initial state.

Only when these methods have been applied to eliminate most errors should verification be applied, if at all.

I have used Maude for specifying and analyzing some advanced protocols, including new active network multicast and broadcast protocols, and security protocols, and have started working on wireless sensor network protocols. My Maude analysis of the multicast protocol uncovered serious design flaws in the protocol which was not found during traditional testing and simulation, and the Maude analysis revealed a fundamental flaw in the already published and "proved" broadcast protocol.

This talk will introduce Maude and its capabilities in a high-level way, will give some examples of modeling and analysis of broadcast, database, and/or security protocols in Maude, and will give an overview of other protocols analyzed by Maude. The talk will be quite introductory and reasonable non-technical, and does not assume any prior knowledge of formal methods.