Software and services
Graduated PhD students
It is too hard to build trustworthy software systems. I aim for
simple, high-level abstractions that offer programmers strong
guarantees about cross-cutting concerns:
- Viaduct: Automatically compiling high-level code to secure cryptographic protocols.
- SCIF: a language for building secure smart contracts.
- Gallifrey: A new language for efficient geodistributed programming.
- SecVerilog and ChiselFlow: hardware
description languages for building processors that control timing channels,
such as Hyperflow.
- Reduct, a game for teaching programming.
Fabric: A language and system for secure, distributed computation, sharing, and storage,
built on Jif: an extended
version of Java that enforces security and privacy by controlling information flow.
- SHErrLoc: The Static Holistic Error Locator
identifies the most likely locations of program errors by analyzing graphs of program constraints.
- JLang, an LLVM back end for
a widely used, extensible Java compiler front end framework for rapid
experimentation with new language extensions.
ACM Transactions on Programming Languages and Systems (TOPLAS)
- Current program committees:
▸ Undergraduate and MEng research opportunities
[Show older projects]
[Show courses taught]
- Awards committees:
ACM Doctoral Dissertation Award Committee, 2015-2018 (2017 chair)
Robin Milner Young Researcher Award Committee, 2019
- Editorial Boards:
Journal of Computer Security (Co-Editor in Chief, 2013–2016)
ACM Transactions on Computer Systems (2009–2016),
ACM Transactions on Information and System Security (TISSEC, now TOPS)
- Program Committees:
PC Chair, POPL 2018
[ report ];
Co-chair, CCS 2016
Computer Security Foundations 2010;
IEEE Symposium on Security & Privacy (Oakland) '09;
Co-chair, Principles of Security and Trust (POST) '15;
IEEE S&P (Oakland) '01, '04, '07, '08,
CSF/CSFW '04, '06,
Euro S&P 2016
ASPLOS '13, '14 (ERC),
OOPSLA '06, '19
USENIX Security '06,
OSDI '00, '04,
European Workshop '04,
Heights Elementary School Math Club (5th grade)
Familia and Genus: OO languages that improve generic programming and exception handling.
- JMatch: a
Java extension with pattern matching and interruptible iterators
Civitas: A practical, secure, remote voting system.
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: