Software and services
Graduated PhD students
It is too hard now to build trustworthy software systems. I aim for
simple, high-level abstractions that offer programmers strong
guarantees about cross-cutting concerns:
Selected recent publications
An abstract yet expressive model for reasoning robustly about the
interaction between authorization and information flow.
Effective localization of type errors in the rich type system of Haskell.
(Distinguished paper award)
An expressive, lightweight genericity mechanism with better
code reuse and stronger static checking
LALR parsers can illustrate parsing conflicts with counterexamples
SecVerilog: a security-typed hardware design language for building hardware without
leaks or timing channels
[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: