JEANNETTE WING
President's Professor of Computer Science, Computer Science Department
www

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 specification and analysis techniques to reason about complex software systems. I direct the Carnegie Mellon Specification and Verification Center and the newly formed Center on Computational Thinking.

My current research interests focus on trustworthy computing: reliability, security, privacy, and usability.  For many years, I have worked on reliable software; in recent years, I have worked on security.  I am now starting an interest in the technical challenges of privacy, e.g., how to specify and reason about privacy policies, how to determine whether software system is compliant with a given privacy policy.  I am particularly keen on investigating formal logics for reasoning about privacy and game theory for modeling processes for preserving privacy.  Here is a sample of some current security projects:

- Automatic Extraction of Confidentiality Policies: Rather than assume the specification of a security policy exists, suppose we were able to extract what policy is actually implemented and then determine whether that is what is desired?  My Ph.D. student, Michael Tschantz, and I are addressing the challenge of automatically extracting from source code a particular kind of confidentiality policy which we call incident-insensitive non-interference.  This property is weaker than Goguen and Meseguer's original notion of non-interference, allowing certain real-world behaviors that Goguen and Meseguer's notion would disallow.  For example, it would allow a secretary access to a patient's file for billing after the doctor has updated the file upon treating the patient.  We are exploring the use of Sheyner's all-counterexamples model checking algorithm to do this extraction automatically.

- Tamper-resistant Embedded Systems:  Layers of tamper resistance, either through hardware or software, are added to embedded devices, to make it more difficult for attackers to gain access to secret data, e.g., encryption keys.  My Ph.D. student, Chris Szilagyi, and I are investigating how to determine the effect of adding different tamper-resistance measures.  We are using model checking as a way to model the system and its environment and looking at how the state space grows or shrinks as different measures are added, modified, or removed.

- Security Metrics: As developers change the functionality of their system, how do they know whether they are making their system more or less secure? My Ph.D. student, Pratyusa Manadhata, and I are working on a formal definition of a system's "attack surface" with the goal of measuring how exposed a system is to attack. With relative measurements, for example, we could say that one system is more secure than another if its attack surface is less than the other's. I started this project while on sabbatical at Microsoft Research, working with Mike Howard and Jon Pincus, where we applied our ideas to seven different versions of Windows.  Pratyusa has since applied this idea to FTP daemons, IMAP servers, and now in an industrial-sized case study with SAP.

- Game Theory and Trustworthy Computing: A former student, Kong-wei Lye, and I did some preliminary work to show how to apply game theory to analyze the security of networked systems. We view the interactions between an attacker and the administrator as a two-player stochastic game and construct a model for the game. Using a non-linear program, we compute Nash equilibria or best-response strategies for the players (attacker and administrator). I would be interested in continuing this work on applying game theory in the context of not just security, but also privacy.

My past research projects include:

1. Larch, a family of specification languages noted for its two-tiered approach to specifying program modules;
2. Miro, a visual specification language for specifying file system security constraints;
3. Avalon, extensions to C and CommonLisp to support distributed transactions;
4. Venari, extensions to Standard ML to support concurrent multi-threaded transactions; and signature and specification matching of software components.
5. TinkerTeach, software infrastructure for electronic delivery of courseware, but best known for providing the TOM conversion service which is in heavy daily use worldwide;
6. Revere, invention of a fully automatic analysis technique called "theory generation," as applied to authentication protocols and simple electronic commerce protocols (the thesis topic of my former student, Darrell Kindred);
7. Verifiable Secret Redistribution, a protocol for recovering shared secrets in a survivable storage system (the thesis topic of my former student, Ted Wong).
8. Attack Graphs, tools for generating attack graphs automatically through an all-counterexamples extension of model checking