Research interests

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: security, extensibility, persistence, distribution.

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 system failures.

Pattern matching that verifies exhaustiveness and redundancy can coexist with data abstraction and subtyping.

Current Projects

[Show courses taught]