Master’s Thesis Presentation • Cryptography, Security, and Privacy (CrySP) • Finding False Assurance in Formal Verification of Software Systems

Please note: This master’s thesis presentation will take place online.

Ru Ji, Master’s candidate
David R. Cheriton School of Computer Science

Supervisor: Professor Meng Xu

Formal verification plays a crucial role in enhancing the reliability of computing systems by mathematically checking the correctness of a program. Although recent years have witnessed lots of research and applications that optimize the formal verification process, the issue of false assurance persists in certain stages of the formal verification pipeline. The false assurance problem is critical since they can easily undermine months if not years of verification efforts.

In this thesis, we firstly generalized the formal verification process. We then identify and analyze specific stages susceptible to false assurance. Subsequently, a systematization of knowledge pertaining to the false assurance issues observed at these stages is provided, accompanied by a discussion on the existing defense mechanisms that are currently available. Specifically, we focused on the problem of formal specification incompleteness.

We presented FAST in this thesis, which is short for Fuzzing-Assisted Specification Testing. FAST examines the spec for incompleteness issues in an automated way: it first locates spec gaps via mutation testing. i.e., by checking whether a code variant conforms to the original spec. If so, FAST further leverages the test suites to infer whether the gap is introduced by intention or by mistake. Depending on the codebase size, FAST may choose to generate code variants in either an enumerative or evolutionary way. FAST is applied to two open-source codebases that feature formal verification and helps to confirm 13 and 21 blind spots in their spec respectively. This highlights the prevalence of spec incompleteness in real-world applications.

To attend this master’s thesis presentation on Zoom, please go to https://uwaterloo.zoom.us/j/8639195783.