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:
My newest line of research is in exploring the use of tractable techniques like theory generation and model checking to analyze finite abstractions of software systems. There are three levels of software analysis I am focusing on:
I am interested in protocols designed for distributed systems, and most recently those from the security domain, such as authentication and electronic commerce protocols. I am pursuing a logic-based approach, called theory generation, 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.''
Relational calculus underlies many computer science application areas including Chen's entity-relationship notation, UML for object-oriented modeling, and the formal specification language Z.
We have developed efficient techniques for solving relational formulae. We use a notation called NP to write the formulae and a checker called Nitpick to do the analysis. Currently Nitpick does a selective form of brute force enumeration to find counterexamples to properties that are claimed to hold of an NP specification. A variety of reduction mechanisms prunes the search space so that flaws can often be found even in huge spaces.
We have used Nitpick on a number of small projects, including to analyze descriptions of architectural styles, and more recently, to discover a flaw in the Mobile IPv6 protocol. We have taught MSE students how to express problems with a combination of diagrammatic object models and Nitpick's textual notation; they have applied this approach successfully in class projects and in their year-long studio.
We have applied well-known results from type theory, in particular a type inference algorithm, to analyzing (untyped) C code for errors. We built a tool called Lackwit that embodies this approach. Lackwit can show where data structures are read and written and how values flow from one to another; it can find candidates for data abstraction and identify representation exposures; and it can show dependences between functions due to shared data, correctly distinguishing incidental use of shared library functions from true architectural connection. The analysis is completely modular and can accommodate missing or incomplete code, handles aliasing and higher order functions smoothly, and seems to scale remarkably well. The prototype tool has been applied successfully to Reid Simmon's Morphin, a robotics application, and is now being used to analyze the source code of the Linux operating system.
We are now extending Lackwit to handle Java code.