Abstract
Living in a computer-reliant era, we’re balancing the power of computer systems with the challenges of ensuring their functional correctness and security. Program analysis has proven successful in addressing these issues by predicting the behavior of a system when executed. However, the complexity of conducting program analysis significantly arises as modern applications employ advanced, high-level programming languages and progressively embody the structure of a composite of independent modules that interact in sophisticated manners. In this talk, I will detail how to apply programming language theory to construct refined vulnerability specifications and reduce the complexity of program analysis across computational, conformational, and compositional aspects: My primary focus will be on introducing some formal specifications that I have developed for modeling the common exponential worst-case computational complexity inherent in modern programming languages. These specifications have guided the first worst-case polynomial solution for detecting performance bugs in regexes. I will also briefly discuss why generating inputs with complex conformation to target deep-seated bugs is a significant obstacle for existing techniques, and how I devised strategies to generate more sound input by intentionally satisfying previously unrecognized forms of dependencies. Finally, as part of a vision to enhance security analysis in modern distributed systems, where different operations can be composed in a complex way and may interleave with each other, I will briefly discuss my efforts to establish new security notions to identify non-atomic operations in smart contracts and deter any potential attacks that might exploit their interactions.
Brief Biography
Yinxi Liu is completing her Ph.D. in Computer Science and Engineering at the Chinese University of Hong Kong in July 2024. Her research interests are in the field of computer security, where she constructs refined vulnerability specifications to reduce the complexity of security analysis across computational, conformational, and compositional aspects, as well as develops program analysis techniques that have found hundreds of real-world bugs. Yinxi had research visits at Microsoft Research Asia, Simon Fraser University, and Southern University of Science and Technology. She received Microsoft Research Asia Fellowship Nomination Award in 2022. Her research has been published in prestigious security conferences IEEE S&P and ACM CCS, and has been recognized by Best Software Artifact Nomination Award at ASE 2021.