Linear-time Temporal Logic guided Greybox Fuzzing
17/02/2022, 10:30am
Speaker
Abstract
Software model checking is a popular validation and verification method for reactive stateful software systems. It checks temporal logic properties against a finite state transition system. However, model checking usually suffers from the state space explosion problem; this is exacerbated in software systems that are naturally infinite-state. Parallel to the works in software model checking, greybox fuzzing methods have seen substantial recent advances. These methods conduct a biased random search over the domain of program inputs to find bugs or vulnerabilities. The main advantage of greybox fuzzing lies in its scalability to large software systems. However, it is only a testing method and it is mostly useful for finding withness simple oracles such as crashes or overflows.
In this talk, I will introduce our recent work. We take a step forward in understanding the synergies between model checking and greybox fuzzing. We propose a fuzzing-based technique that directs fuzzing to find violations of arbitrary LTL properties. Our work substantially extends directed greybox fuzzing to witness complex event orderings. At the same time, compared to model checkers, our approach finds the counterexamples faster, thereby finding more counterexamples within a given time budget.
Speaker Bio
Ruijie Meng is a PhD student in School of Computing at National University of Singapore. She is advised by Prof. Abhik Roychoudhury and Prof. Ilya Sergey. Her research interests fall in program analysis and testing. The current research focuses on combining fuzzing and verification to expose security vulnerabilities in real-world complex software applications.