Finding False Assurance in Formal Verification of Software Systems
Loading...
Date
2024-01-15
Authors
Ji, Ru
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
Abstract
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 as it can easily
undermine months if not years of verification efforts.
In this thesis, we first generalized the formal verification process. We
then identified and analyzed 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
underlineFuzzing-underlineAssisted underlineSpecification
underlineTesting. 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.