CS Guest Presentation: Automata-based Validator for Control-Flow Transformation, Dr. Cheng Zhang, University College London

Abstract:

Decompilation, the process of converting binary files back into structured high-level programs, is a crucial tool for porting and verifying legacy software, conducting security research, and modernizing infrastructures. However, verifying the correctness of decompilation, particularly in the control-flow structuring phase, poses significant challenges. In this talk, I will present a novel algorithm to validate control-flow transformations, including the control-flow structuring phase of decompilers. This validation algorithm is based on the automata of Guarded Kleene Algebra with Tests and has been mathematically proven correct with respect to trace semantics, ensuring that it produces neither false positives nor false negatives. Our prototype implementation has successfully verified the decompilation output of complex core-util functions in a matter of seconds.

Bio:

Cheng Zhang is a postdoctoral research fellow at University College London, working with Professor Alexandra Silva. He received his Ph.D. from Boston University, where he was advised by Professor Marco Gaboardi. His research focuses on developing practical verification solutions using techniques from algebra, automata theory, and bialgebra theory. His previous work includes the development of practical verification tools for control-flow transformations and the semantic foundations of program logics. 

Faculty, undergraduate, and graduate students, interested in AI are encouraged to attend!