I am a Ph.D student majoring in Computer Science at University of Colorado Boulder, co-advised by Bor-Yuh Evan Chang, Pavol Černý and Ashutosh Trivedi. I am a member of Programming Languages and Verification at the University of Colorado Boulder (CUPLV).
I received my master's degree from University of Colorado Boulder in 2017, and bachelor's degree from Nanjing University (Nanjing, China) in 2015.
My current research topic is applying program analysis and verification techniques into Cyber Security. Specifically, I have a focus on the subarea of resource analysis, as well as adopting a type system approach. Resource analysis is fundamental to Cyber Security problems such as Denial-of-Service and Side Channel. The type system approach is compositional and thus scalable, having the potential to scale to real-world programs.
My latest research focuses on verifying the non-existence of Denial-of-service vulnerabilities in web applications.
I have been participating (and funded by) DARPA STAC program since 2015. I have attended six of the so-called "Engagement" events in STAC program, where our task is to either look for Denial-of-Service or Side channel vulnerabilities in web applications, or prove their non-existence.
I have been designing and implementing scalable program analysis tools mainly in Scala. In my recently submitted paper, I implemented a tool with The Checker Framework and Microsoft Z3 Theorem Prover, analyzing and verifying over 180k lines of Java code. The Checker Framework extends Java type system with more powerful and useful annotations, letting software developers detect and prevent errors in their Java programs.
I love writing code and I am very enthusiastic about developing tools that address real-world problems.
- Type-directed Bounding of Collections in Reactive Programs. Tianhan Lu, Bor-Yuh Evan Chang, Pavol Černý, Ashutosh Trivedi. Under Submission