Software and services
Graduated PhD students
It is too hard to build trustworthy software systems
using conventional systems APIs. I work on higher-level,
language-based abstractions for programming that better
address important cross-cutting concerns:
Selected recent publications
SecVerilog: a security-typed hardware design language for building hardware without
leaks or timing channels
Using information flow control with quorum replication
to enforce confidentiality, integrity, and availability.
Distributed transactions can be sped up by giving clients time-limited
invariants on state and computation.
Diagnosing maximum-likelihood program error locations from constraint
Pattern matching that verifies exhaustiveness and redundancy can
coexist with data abstraction and subtyping.
Fabric: A federated system for securely storing, sharing, and computing information.
- SHErrLoc: The Static Holistic Error Locator
identifies the most likely locations of program errors by analyzing the program constraint graph.
- Controlling timing channels by static analysis and dynamic mitigation
- Jif: an extended
version of Java that protects privacy by controlling information flow.
Civitas: A practical, secure, remote voting system.
- JMatch: a
Java extension with pattern matching and interruptible iterators
a widely used, extensible Java compiler front end framework for rapid
experimentation with new language extensions.
- PLDI 2014 Tutorial: The Polyglot Extensible Compiler Framework (June 2014)
- Program committees:
POST '15 (PC Co-Chair),
- Editorial Boards:
Journal of Computer Security (Co-Editor-in-Chief),
ACM Transactions on Computer Systems (Assoc. Editor)
▸Undergraduate and MEng research opportunities
[Show older projects]
[Show courses taught]
- Program Committees:
Computer Security Foundations 2010,
IEEE Symposium on Security & Privacy (Oakland) '09;
IEEE S&P (Oakland) '01, '04, '07, '08,
CSF/CSFW '04, '06,
ASPLOS '13, '14 (ERC),
USENIX Security 2006,
OSDI '00, '04,
European Workshop '04,
Swift: Making web applications secure by construction.
language features for extensible, composable, adaptable software
J\Mask: Java extended with masked types for safe, flexible object initialization.
SIF: Servlets with secure information flow.
STONESOUP: an IARPA-funded study on how to certify and run software of uncertain provenance securely
- DARPA Information Science and Technology Study Group (ISAT), 2005–2008
- Jif/split: a version of Jif that automatically partitions programs
to run securely on a distributed system.
J0: Java for novice programmers
- PolyJ: an extended
version of Java that supports parametric polymorphism, freely
available for both Windows and Unix.
- Thor, a
distributed object-oriented database, and Theta,
the internal programming language of Thor. This work provided scalable
techniques for efficiently implementing distributed, persistent
objects and language features such as methods and parametric polymorphism.
Dagstuhl seminar on Mobility, Ubiquity, and Security (Feb.'07)
- Invited and keynote talks: