Bounded Model Checking for Hyperproperties with QBF-based Algorithms
- LecturerMs. Tzu-Han Hsu (Dept. of Computer Science Engineering, Michigan State University, USA)
Host: Yu-Fang Chen - Time2023-05-09 (Tue.) 15:00 ~ 17:00
- LocationAuditorium 101 at IIS new Building
Abstract
Hyperproperties is a powerful framework for specifying and reasoning about important classes of requirements that were not possible with trace-based languages such as the classic temporal logics. This talk will introduce a novel bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. Followed by the reduction of BMC for LTL to SAT solving, our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. Our algorithm is sound based on our theory of bounded semantics, which guarantees correct BMC results under finite exploration. A recent extension of our algorithm also supports loop conditions, which incorporate SAT solving; and the asynchronous hyper logic A-HLTL, which utilizes the notion of trajectories to handle traces that advance at different speeds. In this talk, we will also present our implemented tool HyperQB, a push-button QBF-based bounded model checker for hyperproperties, and demonstrate the effectiveness and efficiency of our approach via a rich set of practical applications, including (1) security policies verification for concurrent data structures, path planning for multi-agent systems, secrecy-preserving mapping synthesis, compiler optimization security, cache-based timing attack detection, and program conformance.
BIO
Tzu-Han Hsu is a third-year Ph.D. student in Computer Science and Engineering department at Michigan State University, advised by Dr. Borzoo Bonakdarpour. Her research areas include formal methods, model checking, verification, and synthesis for security/privacy policies. She is recently working on the topic of hyperproperties, a framework that can reason about multiple traces simultaneously, which has rich applications in formal analysis especially for multi-threaded and concurrent programs.
Before MSU, Tzu-Han received her bachelor’s degrees in Computer Science and Music-Piano Performance from Iowa State University in 2020. Tzu-Han can be reached on Twitter (@TzuHanH), LinkedIn (tzuhanhsu), email (tzuhan@msu.edu ), and her personal website (https://tzuhancs.github.io/ ).
Before MSU, Tzu-Han received her bachelor’s degrees in Computer Science and Music-Piano Performance from Iowa State University in 2020. Tzu-Han can be reached on Twitter (@TzuHanH), LinkedIn (tzuhanhsu), email (tzuhan@msu.edu ), and her personal website (https://tzuhancs.github.io/ ).