Presented at ISC 2024
Emulation makes dynamic analysis easier, but emulation of Android kernels is rarely supported. We proposed a tool (LiLi) that makes it eaiser to emulate Android kernel images. We then fuzzed some kernels, and found 4 zero-day vulnerabilities (some high-severity).
Presented at VSTTE 2025
Amazon has convened a set of challenges to verify the Rust standard library. In this paper, we discuss the lessons learned thus far from this verification effort, from both our work on it, as well as that of the broader community.
Presented at HATRA 2024
We explore what it means to do Rust verification. Specifically, we explore which properties are worth verifying for Rust; what techniques exist to verify them; and which code is worth verifying. In doing so, we motivate an effort to verify safety properties of the Rust standard library, presenting the relevant challenges along with ideas to address them.