Current projects
Substructural Information Flow
Leveraging existing mechanisms for parametric polymorphism, we've developed a new syntax for information flow that offers (sometimes significantly) simpler type signatures. This simplified syntax invites an analysis of substructural information flow control, identifying structure analogous to the rules of weakening, contraction, and exchange in most existing theories of information flow. We've shown that reasoning about capabilities and resource exhaustion naturally emerges from an information flow system equipped with substructural reasoning-- not only intuitively, but formally. The latter is substantiated via substructural non-interference, a powerful generalization of non-interference that takes advantage of the substructural properties of our system. Check out the presentation at IWACO 2024! There's a full-length paper coming soon.
Past projects
Simpler Information Flow Control (in 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.