Jeannette Wing

My general research interests lie in distributed systems, programming languages, and software engineering. I especially enjoy integrating approaches from these different areas and applying results from more theoretical work on languages to practical problems found in real systems. A long-term goal that drives my research is to provide, where appropriate, as rigorous as possible a foundation to the design and implementation of software.

My specific interest is the application of formal methods to reason about complex software systems. Formal methods play an important role in all aspects of software development and can be used to state a system's properties precisely and unambiguously. To give a flavor of the kinds of problems I like to tackle, here are some case studies in the application of formal methods that I have recently done with fellow students and colleagues:

• authentication and electronic cash protocols
• cache coherence in distributed file systems
• error recovery for families of RAID architectures
• dynamic sets used for search through the Web
• mobile internetworking protocols

My newest line of research is in exploring the use of tractable techniques like model checking to analyze finite abstractions of software systems. I am focusing my attention on protocols designed for distributed systems, and most recently those from the security domain, such as authentication and electronic commerce protocols. There are two independent threads of research I am pursuing:

1. A logic-based approach where the logic plus the protocol defines a finite represtenation of a theory; checking the property of the protocol is a simple membership test.

   This is a completely new approach to checking authentication protocols. It is fast and completely automatic. The speed in checking protocol designs is on the order of recompiling the protocol specification.

   An elegant aspect of our approach is that it is modularized (exploiting the SML modules feature) in such a way that our system allows users to generate automatically a checker given a particular logic. In essence, we have a checker generator, which can be instantiated to produce individual logic checkers. An expected contribution of all this work is the provision of ``little checkers'' for ``little logics.''

2. A model-based approach where a finite state machine model is defined for the protocol; properties stated are checked of the finite model.

   We are applying this approach to reasoning about electronic commerce protocols and with a completely new focus on the kinds of properties to reason about (atomicity properties, not ``standard'' properties like non-interference or trust, which are less relevant in this domain).

   We have used existing model checkers like FDR and SMV to do our checks. However, upon realizing the limitations of both with respect to expressibility (both of the properties to check and of the protocols themselves), we are now studying from first principles what a better mathematical model of computation for electronic commerce protocols should be and how atomicity properties can be asserted and proved of them.

Finally, I am also interested in the integration of model checking and proof checking technologies into one verification and debugging system.

Brought to you by the Composable Software Systems research group at Carnegie Mellon University's School of Computer Science. Last updated Wed Apr 23, 1997.