Exploits and insecure compilation§

The field of secure compilation studies when and how security properties are preserved by a compiler. My recent research has examined how concepts and techniques from the study of secure compilation can be applied to the problem of understanding vulnerabilities, exploits, and security mitigations.

Software Contracts for Security§

Component-based software engineering is an approach for building complex systems from seperate components that interact via clearly defined interfaces. "Design by Contract" is a programming methodology that facilitates this approach by attaching executable specifications, called software contracts, to components to ensure that each component correctly interacts with the rest of the system.

Existing work on software contracts has focused almost exclusively on contracts for functional correctness. In my work, I explore how software contracts are also an effective mechanism for specifying and enforcing security properties.

Information-flow security§

By tracking and controlling the flow of information within an entire system, information-flow security can express and enforce strong and precise security policies with high assurance. My research on information flow has ranged from designing new type systems and enforcement mechanisms for policies like assured information erasure and progress-sensitive security to developing static analyses that make it easier to apply information-flow security to existing programs.

Logic programming§

Logic programming is a programming paradigm where computations are declaratively specified as collections of logical relations. Logic programming excels at clearly defining search and inference problems. In my work, I have applied logic programming to simplify the development of programs for model-checking security properties and synthesizing disparate sources of provenance data.