Current projects
Information Flow Control 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!
Past projects
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.