Hidden fallacies in formally verified systems

Abstract

Formal verification or formal methods represent a rising trend in approaches to correct software construction, i.e. they help us answer the question of how to build software that contains no errors, colloquially known as “bugs.” They achieve their goal by providing means for stating theorems about the program under test, and for proving such theorems by methods well-known in mathematics, specifically in mathematical logic. Of course, formal methods are no silver bullet and come with their own set of limitations, the most significant of which is extremely difficult scalability with software size. In spite of the limitations, there have been important breakthroughs in their applications over the last 10–15 years, e.g. Leroy’s CompCert (verified C compiler) or Klein’s seL4 (verified implementation of the L4 microkernel). However, how bug-free is verified software in reality? Formal methods make a bold claim that there are indeed no bugs in verified software, or more formally, that the software precisely implements its specification. Unfortunately, as an empirical study from 2017 by Fonseca et al. shows, it may be just too easy to introduce errors into the specification itself, either in form of mistakes (“specification bugs”), or in form of unanticipated assumptions. This thesis aims to take a broader look at formally verified software and formal verification systems, and identify the most common problems in formal methods’ applications, leading to bugs still being present in verified software. In particular, the main contribution of this thesis is an overview of several software projects employing formal methods at their core; an empirical study of “real-world” guarantees that the formal verification systems afford them; and, consequently, showcases of different approaches to verified software, along with their strengths and weaknesses. We believe that understanding how formal methods succeed and fail (or rather, how they can be misused) will be helpful in determining when they become an attractive and worthwhile choice for more ordinary (as opposed to top mission-critical) software. Indeed, we hope that this thesis may serve as an introductory guide for new projects to the guarantees provided by formal verification; correctness guarantees much stronger than those given by software testing. We hope that in long-term, entry barrier to formal verification will become sufficiently low for formal methods to enter mainstream software development, making developers more confident about their programs, and hopefully ridding our world of “buggy” software once and for all.