Graduated Ph.D. Students
Formalizing and Enforcing Purpose Restrictions
, May 2012, International Computer Science Institute, UC Berkeley, Berkeley, CA.
An Attack Surface Metric
, August 2008, Hewlett Packard Enterprise, Princeton, NJ.
Scenario Graphs and Attack Graphs
, May 2004, MarketSight,Cambridge, MA. 2004 SCS Dissertation Award. Nominated for 2004 ACM Dissertation Award.
Decentralized Recovery for Survivable Storage Systems
, May 2004, Human Longevity, Mountain View, CA.
(joint with D. Jackson),
Generalized Aliasing as a Basis for Program Analysis Tools
, November 2000, Mozilla. ACM Dissertation Award Honorable Mention.
Protecting Individuals' Interests in Electronic Commerce Protocols
, October 2000, Intel, Santa Clara, CA.
(joint with D. Jackson),
, August 2000, Vermont Technical College, Burlington, VT.
Theory Generation for Security Protocols
, April 1999, Sparta, Baltimore MD.
Amy Moormann Zaremski
Signature and Specification Matching
, January 1996. Xerox, Rochester, NY.
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.
Language Support for Mobile Agents
, December 1995, Tamr, Inc., Boston, MA.
Bruce L. Horn (joint with J. Morris),
, 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.
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.
. Software infrastructure for education. The
. Specification and
language support for transactions
; search and retrieval using
. Visual specification of security constraints.
Extensions to C++ to support distributed transactions.
. A two-tiered approach to the formal specification of program modules.