Murphi description language and verifier

Warning

Murphi hasn't been maintained at Stanford for a long time, so this web page is quite out-of-date. Prof. Ganesh Gopalakrishnan's research group at the University of Utah is actively doing research based on Murphi, and is distributing several versions of the tool.


Sections:
Overview
State reduction
Algorithmic techniques
Getting Murphi
Applications of Murphi
Participants


Overview

The Murphi description language is based on a collection of guarded commands (condition/action rules), which are executed repeatedly in an infinite loop (this idea is borrowed from Misra and Chandy's Unity model).

The data structures and guarded commands are written in a language that should be fairly familiar to programmers. It includes well-known data types (subranges, enumerated types, arrays, and records), as well as some new types for improving the efficiency of verification. New datatypes include "Multiset", for describing a bounded set of values whose order is irrelevant to the behavior of the description, and "Scalarset" for describing a subrange whose elements can be freely permuted.

Murphi also has a formal verifier based on explicit state enumeration. The verifier performs depth- or breadth-first search in the state graph defined by a Murphi description, storing all the states it encounters in a large hash table. When a state is generated that is already in the hash table, the search algorithm does not expand its successor states (they were expanded whenever the state was originally inserted in the table).

Here is an early paper which overviews Murphi

"Protocol Verification as a Hardware Design Aid," David L. Dill, Andreas J. Drexler, Alan J. Hu and C. Han Yang, 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Computer Society, pp. 522-525.

State reduction

Murphi has several special ways for reducing the number of reachable states while guaranteeing that protocol errors will still be detected.

Symmetry. In some cases, the description has identical elements which can be permuted consistently without changing any important verification properties. The user can indicate this fact by changing a subrange into a datatype we have invented, called Scalarset, indicating that the elements of the subrange can be permuted arbitrarily without affecting verification properties. The Murphi compiler checks that there are no constructs that break the symmetry of the scalarset. The Murphi compiler uses this information to avoid generating redundant states which differ only in how the scalarset is permuted. For some multiprocessor cache coherence protocols, this has reduced the number of states examined by a factor of over 100.

"Better Verification through Symmetry," C. Norris Ip and David L. Dill, International Conference on Computer Hardware Description Languages, April 26-28, 1993, pp 87-100.
"Efficient Verification of Symmetric Concurrent Systems," C. Norris Ip and David L. Dill, 1993 IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Computer Society, pp 230-234.
"Better Verification through Symmetry," C. Norris Ip and David L. Dill, Formal Methods in System Design, Volume 9, Numbers 1/2, pp 41-75, August 1996.

Reversible rules. Sometimes condition/action action rules can be executed "in reverse". Murphi uses this property for state reduction: it checks the states generated via reversible rules from a particular "progenitor" state. After that, it discards all but the progenitor states. Whenever it looks up a state in the state table, it fires reversible rules backwards to get to a progenitor state and looks up only the progenitor.

State Reduction Using Reversible Rules C. Norris Ip and David L. Dill, 33rd Design Automation Conference, June 1996.

Repetition constructors. In some cases, a protocol can be verified by abstracting away from the exact number of processes. Instead, the verifier only keeps track of whether there are zero, one or more than zero processes in a particular state. This drastically reduces the number of states that need to be generated in verification.

Verifying Systems with Replicated Components in Murphi C. Norris Ip and David L. Dill, International Conference on Computer-Aided Verification, 1996

Algorithmic techniques

The algorithmic techniques in Murphi aim at exploring a given state space in the most efficient manner to allow verification of larger protocols.

Probabilistic verification. A great deal of space can be saved if the we are willing to accept a small probability of a missed error. We have included in Murphi "hash compression" algorithms which store small signatures for the states instead of all of the data in a state. The search algorithm hashes into the hash table and checks whether the signature stored there matches the signature of the state being checked. With appropriate attention to the hashing algorithm, signature generation, and search strategy, small signatures can be used to verify large state spaces while still guaranteeing a small upper bound on the probability of missing an error.

Improved probabilistic verification by hash compaction, Ulrich Stern and David L. Dill, Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995
This idea can be combined effectively with state space caching, which replaces entries in the hash table when the table becomes full.
Combining State Space Caching and Hash Compaction, Ulrich Stern and David L. Dill, Methoden des Entwurfs und der Verifikation digitaler Systeme: 4. GI/ITG/GME Workshop Proceedings, Kreischa, March 25-27, 1996
A tighter upper bound on the probability of missing an error can be calculated by reasoning about paths in the reachability graph. When combining this idea with Amble and Knuth's ordered hashing, the bound on the probability can, for typical protocols, be reduced by an exponential factor, which enabled a roughly 50% reduction in the size of the signatures.
A New Scheme for Memory-Efficient Probabilistic Verification, Ulrich Stern and David L. Dill, Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification: IFIP TC6/WG6.1 Joint International Conference, 1996
For example, in the DASH protocol, the number of bits stored can be reduced from 3012 to 20 while still guaranteeing a maximum probability of 0.0008% of missing an error when searching 10675140 states.

Parallel Murphi. With the use of state and memory reduction techniques in Murphi, runtime becomes a major limiting factor. We developed a parallel version of Murphi for distributed memory multiprocessors and networks of workstations that is based on the message passing paradigm. In experiments with three complex cache coherence protocols, parallel Murphi showed close to linear speedups. Since the state table is partitioned over the parallel machine, the algorithm also allows the verification of larger protocols.

Parallelizing the Murphi Verifier, Ulrich Stern and David L. Dill, 9th International Conference on Computer Aided Verification, 1997

Using magnetic disk. With a special algorithm magnetic disk instead of main memory can be used for storing almost all of the state table at the cost of a small runtime penalty, which is typically around 15% when the memory savings factor is between one and two orders of magnitude. The algorithm linearizes the accesses to the state table and amortizes the cost of accessing the whole table over all the states in a level of the breadth-first search.

Using Magnetic Disk instead of Main Memory in the Murphi Verifier, Ulrich Stern and David L. Dill, CAV '98.

Caching Murphi. This is a version of Murphi, not done at Stanford, that implements state space caching. This release was donated by Enrico Tronci. E. Tronci, G. Della Penna, B. Intrigila, M. Venturini Zilli, "Exploiting Transition Locality in Automatic Verification", Proceedings of: 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), 4-7 September 2001, Livingston-Edinburgh (Scotland), LNCS, Springer-Verlag Co-sponsored by the IFIP TC10/WG10.5 Working Group on: Design and Engineering of Electronic Systems


Getting Murphi

Source code, some executables, documentation, and extensive verification examples are available for Murphi. All of this is freeware, with very liberal licensing terms.

The primary release at this time is Murphi3.1, which has the basic Murphi verifier, plus symmetry reduction, multisets, hash compaction, and improvements for security protocols as options. Please check the list of recent bug fixes if you downloaded Murphi3.1 some time ago and have encountered a Murphi problem. If you want to be added to the Murphi mailing list, report bugs or make suggestions, please send Email to murphi@verify.stanford.edu.

We have used Murphi on various versions of Unix and Linux. In addition, it worked under Cygnus's Cygwin environment (free release B20.1) running on Windows 95.

"cmurphi" is a version of Murphi that optionally uses state space caching. It was donated by E. Tronci.

For a limited time, the previous release, Murphi3.0, will still be available from this site.

Rel2.70L is an older release without the above features. However, it supports verification of liveness properties. Specifications can be written in a subset of linear-time temporal logic, and various kinds of fairness constraints can be specified. Unfortunately, we don't know how to combine liveness verification efficiently with symmetry reduction, so we haven't put this feature in Murphi3.0. Rel2.71L is a somewhat updated version of Rel2.70L, but it is still missing symmetry reduction.


Applications of Murphi

Murphi has now been used for several different verification tasks. This is a non-exhaustive list of instances where it has been used extensively: An early paper about an executable specification in Murphi of TSO and PSO is:
"Formal Specification of Abstract Memory Models," David L. Dill and Seungjoon Park and Andreas G. Nowatzyk, Research on Integrated Systems: Proceedings of the 1993 Symposium, Gaetano Borriello and Carl Ebeling, Eds. MIT Press, 1993, pp 38-52.
A later specification of RMO is discussed in:
"An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order)," Seungjoon Park and David L. Dill, 7th ACM Symposium on Parallel Algorithms and Architectures, 1995, pp. 34-41.
A discussion of the verification of SCI appears in
"Automatic verification of the SCI cache coherence protocol," Ulrich Stern and David L. Dill, Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995
A methodology to analyze cryptographic protocols using Murphi is described in
"Automated analysis of cryptographic protocols using Murphi," John C. Mitchell, Mark Mitchell, and Ulrich Stern, IEEE Symposium on Security and Privacy, 1997
This methodology has been used to analyze the SSL protocol
"Finite-State Analysis of SSL 3.0," John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern, 7th USENIX Security Symposium, 1998

Participants

This methodology has been used to analyze the SSL protocol The Murphi project has had many participants over the years. Murphi has been totally rewritten two or three times.

The original version was designed and implemented by David L. Dill, Andreas Drexler, Alan J. Hu, and C. Han Yang.

Later, it was rewritten by Ralph Melton. Seungjoon Park added liveness checking and fairness constraints. C. Norris Ip installed symmetry reduction, and rewrote a lot of the code (we did not know how to check liveness while doing symmetry reduction, so his version does not support liveness checking). Then Denis Leroy sped up the code and generally maintained the system for awhile.

Ulrich ("Uli") Stern implemented the hash compression algorithms. C. Norris Ip implemented reversible rules and repetition constructors (not in the distributed version). The code was sped up another time and made more portable by Uli Stern, resulting in release 3.0.

Murphi is currently maintained by Ulrich Stern and Norris Ip.


David L. Dill's home page
Group's home page
Last updated 1/12/2011