Jeannette Wing
Email wing@cs.cmu.edu
Department
Computer Science Department
Research/Teaching Statement
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.
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 mostly interested in the foundations of security and privacy. Much as we have algorithms, impossibility results, and formal methods for building reliable, distributed systems, I am interested in laying similar kinds of foundations for security and privacy. For security, I seek compositional techniques and properties that allow one to reason locally in order to build large systems with clean interfaces and well-defined behavior. I am now also 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 applications in healthcare.
Here is a sample of some current projects:
- Information Flow Experiments: How can one detect what data is being used by a website? To answer this specific question, Michael Tschantz, Anupam Datta, and I formalize information flow analyses where the analyst has neither control nor a complete model of the analyzed system. We prove that generalizations of our specific problem are ones of causal inference. Leveraging this connection, we push beyond traditional information flow analysis to provide a systematic methodology based on experimental science and statistical analysis.
- Science of Security: Rather than the band-aid approach we currently use to patch our systems after we detect an exploit of a security vulnerability, suppose we could build software systems based on theories, laws, and principles with predictable value with respect to security properties? Predictability requires security modeling, e.g., game-theoretic models, and security analysis, including quantitative, not just qualitative analysis. To address scalability, I am interested in understanding when security properties do or do not compose, and how to achieve compositionality. I am also interested in security metrics.
- Trust in Networks of Humans and Computers: The advent of social media gives rise to this fundamental question "How can I (a human) trust the information I receive through the Internet?" Virgil Gligor and I are exploring the combination of trustworthiness from computer science the concept of behavioral trust from economics. Our goal is to build a general theory of trust for networks of humans and computers.
My past research projects include:
- Larch, a family of specification languages noted for its two-tiered approach to specifying program modules;
- Miro, a visual specification language for specifying file system security constraints;
- Avalon, extensions to C and CommonLisp to support distributed transactions;
- Venari, extensions to Standard ML to support concurrent multi-threaded transactions; and signature and specification matching of software components.
- TinkerTeach, software infrastructure for electronic delivery of courseware, but best known for providing the TOM conversion service which is in heavy daily use worldwide;
- 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);
- Verifiable Secret Redistribution, a protocol for recovering shared secrets in a survivable storage system (the thesis topic of my former student, Ted Wong).
- Attack Graphs, tools for generating attack graphs automatically through an all counterexamples extension of model checking
- 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)
- Privacy Specification and Compliance: Formalization "use" and "purpose," notions common in privacy policies, in terms of planning modes from artificial intelligence (the thesis topic of my former student, Michael Tschantz, co-advised with Anupam Datta)