Graduated Ph.D. Students

  • Ryan Bernstein, Abstractions for Probabilistic Programming to Support Model Development, April 2023.
  • Michael Tschantz, Formalizing and Enforcing Purpose Restrictions, May 2012, International Computer Science Institute, UC Berkeley, Berkeley, CA.
  • Pratyusa Manadhata, An Attack Surface Metric, August 2008, Hewlett Packard Enterprise, Princeton, NJ.
  • Oleg Sheyner, Scenario Graphs and Attack Graphs, May 2004, MarketSight,Cambridge, MA. 2004 SCS Dissertation Award. Nominated for 2004 ACM Dissertation Award.
  • Theodore Wong, Decentralized Recovery for Survivable Storage Systems, May 2004, Human Longevity, Mountain View, CA.
  • Rob O'Callahan (joint with D. Jackson), Generalized Aliasing as a Basis for Program Analysis Tools, November 2000, Mozilla. ACM Dissertation Award Honorable Mention.
  • Hao-Chi Wong, Protecting Individuals' Interests in Electronic Commerce Protocols, October 2000, Intel, Santa Clara, CA.
  • Craig Damon (joint with D. Jackson), Selective Enumeration, August 2000, Vermont Technical College, Burlington, VT.
  • Darrell Kindred, Theory Generation for Security Protocols, April 1999, Sparta, Baltimore MD.
  • Amy Moormann Zaremski, Signature and Specification Matching, January 1996. Xerox, Rochester, NY.
  • Scott Nettles, Safe and Efficient Persistent Heaps, December 1995. University of Texas, Austin, TX.
  • J. Gregory Morrisett (joint with R. Harper), Compiling With Types, December 1995. Cornell University, Ithaca, NY.
  • Fritz Knabe, Language Support for Mobile Agents, December 1995, Tamr, Inc., Boston, MA.
  • Bruce L. Horn (joint with J. Morris), Constrained Objects, December 1993. Independent consultant, Mountain View, CA 94043.
  • Richard A. Lerner, Specifying Objects in Concurrent Programs, May 1991, Clickshare, Springfield, MA.
  • David L. Detlefs, Concurrent, Atomic Garbage Collection, October 1990. Facebook, Seattle, WA.

    • Graduated M.S. Students

  • Oren Dobzinski, ECE, Alert Abstration Using Attack Graphs, May 2006.
  • E. Chaos Golubitsky, Information Networking Institute, Measuring Attack Surfaces of Open Source IMAP Servers, May 2005.
  • Meera Sridhar, CS Fifth Year Scholar, Experiments with an Attack Graph Toolkit, August 2004.

    • Postdocs and Visitors

  • Dilsun Kaynar, postdoc, 2006-07.
  • Michael Loui, Professor of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign, visiting faculty, 2000-01.
  • Kiyotaka Kuroda, Mitsubishi Electric Co., Japan, visiting engineer, 1994-95.
  • Morten Soerensen, Technical University of Denmark, Lyngby, Denmark, visiting student, 1994-95.
  • Chun Gong, Academia Sinica, Beijing, China, visiting student, 1988-90.

    • Past Research Projects

  • Center for Computational Thinking. Sponsored by Microsoft Research.
  • Specification and Verification Center: Specification and verification tools, languages, and methods for hardware and software systems. Co-PIs: Ed Clarke, David Garlan, Bruce Krogh, Reid Simmons. Sponsored by the Army Research Office (David Hislop, program manager), National Science Foundation, and NASA/Ames.
  • Foundations of Privacy
  • Purpose Restrictions in Privacy Policies, with Michael Tschantz and Anupam Datta
  • Science of Security
  • Compositional Security, with Limin Jia and Anupam Datta
  • Trust in Networks of Humans and Computers, with Virgil Gligor
  • Attack Surface Measurement: People, publications, related articles.
  • Scenario and Attack Graphs: People, publications, tools.
  • Secure Storage Systems: Protocols for verifiable secret redistribution.
  • TOM Consortium: The TOM server automatically converts documents and files of one type to another. Great for reading e-mail attachments, creating web pages from powerpoint slides, excel spreadsheets, latex documents, etc.
  • Composable Software Systems. Putting components and connectors together in a principled way. Tractable software design and code analyses.
  • TinkerTeach. Software infrastructure for education. The TOM server.
  • Venari. Specification and language support for transactions; search and retrieval using signatures and specifications.
  • Miro. Visual specification of security constraints.
  • Avalon Extensions to C++ to support distributed transactions.
  • Larch. A two-tiered approach to the formal specification of program modules.