Current Projects
Scalable Information Flow
We're developing a new syntax and logical foundations for secure information flow which makes a number of significant practical and metatheoretic advances over the state of the art. First, we revisit and resolve the tension between non-interference and declassification, recognizing the latter as a consequence of the former under standard type abstraction mechanisms. Second, we simplify information flow specifications by analyzing their interplay with proof-theoretic polarity and designing around common patterns in information flow-typed programs. Finally, we find a powerful generalization of information flow giving way to reasoning about capabilities, resource exhaustion, protocols, and more with only minimal extensions to the surface syntax. The first few pages of our OOPSLA 2025 and POPL 2026 papers introduce the above with lots of examples!
Past Projects
Information Flow for Rust
We're working on a new, simplified theory of information flow control that takes advantage of (1) guarantees made by the Rust type system (particularly statically tracked lifetimes and the borrow checker) and (2) simplifying assumptions about realistic verification scenarios, validated partially by case studies, to make reasoning about IFC easier. Check out our HATRA '22 paper!
Macro Errors
Many popular Rust packages make extensive use of the trait system within macros as an ad-hoc way of validating that syntax given to the macro is well-typed at the level of abstraction presented by the package's APIs. Unfortunately, this often leads to poor error messages and brittle interfaces. I'm working on ways to interleave type checking with macro expansion so that functionality built with macros can produce high-quality errors and integrate more deeply into the host language. You can find a proof-of-concept implementation here.
Gradual Verification
Static verification is a notoriously difficult problem. Dynamic verification is much easier, but comes with a performance cost. Gradual verification tackles both of these by applying established research on gradual typing to the domain of program verification. As part of this project, I modified an existing optimistic static verification toolchain to produce dynamic checks where static information proved insufficient. A pre-print of the paper is available.
Action-Based Test Carving
Writing unit tests is hard, especially when the Android Framework is involved—manually creating mock and shadow objects can get tedious and repetitive, and it's no fun either (well, at least not for me). For this project, we created a toolchain capable of automatically synthesizing Android JUnit tests from execution traces. My part in this project involved automatically creating the necessary mock and shadow objects and inserting them into the test, effectively emulating the parts of the Android Framework necessary for running a unit test. A pdf of the workshop paper is available here.