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 Carnegie Mellon-Microsoft Research 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 interested in the technical challenges of privacy, e.g., how to specify and reason about privacy policies, how to determine whether a 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 projects:

- Understanding Use and Purpose in Privacy Policies: An email service provider might assert that it will not use email for serving ads, but is will for spam filtering.  A hospital might assert that a patient's health information may be used for research purposes, but not for marketing by pharmaceutical companies.  My Ph.D. student, Michael Tschantz, and I, along with Anupam Datta of CyLab, are interested in formalizing these notions of "use" and "purpose" which commonly arise in privacy policies.  We would like eventually to come up with methods, models, and tools to automate determining whether an organization abides by its asserted policies or detecting when it does not.

- 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.

- 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
9. Attack Surface Security Metric, a method for measuring the "attack surface" of a software system, useful for comparing whether one version of a system is "more secure" than another (the thesis topic of my former student, Pratyusa Manadhata)