• Login
    View Item 
    •   SMARTech Home
    • Georgia Tech Theses and Dissertations
    • Georgia Tech Theses and Dissertations
    • View Item
    •   SMARTech Home
    • Georgia Tech Theses and Dissertations
    • Georgia Tech Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Hidden fallacies in formally verified systems

    Thumbnail
    View/Open
    BOBEK-THESIS-2020.pdf (1.019Mb)
    fuse-harness.tar.gz (33.03Kb)
    Date
    2020-04-28
    Author
    Bobek, Jan
    Metadata
    Show full item record
    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.
    URI
    http://hdl.handle.net/1853/62855
    Collections
    • College of Computing Theses and Dissertations [1156]
    • Georgia Tech Theses and Dissertations [23406]

    Browse

    All of SMARTechCommunities & CollectionsDatesAuthorsTitlesSubjectsTypesThis CollectionDatesAuthorsTitlesSubjectsTypes

    My SMARTech

    Login

    Statistics

    View Usage StatisticsView Google Analytics Statistics
    facebook instagram twitter youtube
    • My Account
    • Contact us
    • Directory
    • Campus Map
    • Support/Give
    • Library Accessibility
      • About SMARTech
      • SMARTech Terms of Use
    Georgia Tech Library266 4th Street NW, Atlanta, GA 30332
    404.894.4500
    • Emergency Information
    • Legal and Privacy Information
    • Human Trafficking Notice
    • Accessibility
    • Accountability
    • Accreditation
    • Employment
    © 2020 Georgia Institute of Technology