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