Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem
Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2016.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2017
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/106390 |
| _version_ | 1826211272198193152 |
|---|---|
| author | Wang, Stephanie, M. Eng Massachusetts Institute of Technology |
| author2 | Frans Kaashoek and Nickolai Zeldovich. |
| author_facet | Frans Kaashoek and Nickolai Zeldovich. Wang, Stephanie, M. Eng Massachusetts Institute of Technology |
| author_sort | Wang, Stephanie, M. Eng Massachusetts Institute of Technology |
| collection | MIT |
| description | Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2016. |
| first_indexed | 2024-09-23T15:03:17Z |
| format | Thesis |
| id | mit-1721.1/106390 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T15:03:17Z |
| publishDate | 2017 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1063902019-04-10T15:59:06Z Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem Wang, Stephanie, M. Eng Massachusetts Institute of Technology Frans Kaashoek and Nickolai Zeldovich. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2016. This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. Cataloged from student-submitted PDF version of thesis. Includes bibliographical references (pages 57-60). As more and more software is written every day, so too are bugs. Formal verification is a way of using mathematical methods to prove that a program has no bugs. However, if formal verification is to see widespread use, it must be able to compete with unverified software in performance. Unfortunately, many of the optimizations that we take for granted in unverified software depend on assumptions that are difficult to verify. One such optimization is data checksums in logging systems, used to improve I/O efficiency while still ensuring data integrity after a crash. This thesis explores a novel method of modeling the probabilistic guarantees of a hash function. This method is then applied to the logging system underlying RapidFSCQ, a certified crash-safe filesystem, to support formally verified checksums. An evaluation of RapidFSCQ shows that it enables end-to-end verification of application and filesystem crash safety, and that RapidFSCQ's optimizations, including checksumming, achieve I/O performance on par with Linux ext4. Thus, this thesis contributes a formal model of hash function behavior with practical application to certified computer systems. by Stephanie Wang. M. Eng. 2017-01-12T18:18:50Z 2017-01-12T18:18:50Z 2016 2016 Thesis http://hdl.handle.net/1721.1/106390 967665009 eng M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission. http://dspace.mit.edu/handle/1721.1/7582 60 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Wang, Stephanie, M. Eng Massachusetts Institute of Technology Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem |
| title | Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem |
| title_full | Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem |
| title_fullStr | Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem |
| title_full_unstemmed | Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem |
| title_short | Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem |
| title_sort | certifying checksum based logging in the rapidfscq crash safe filesystem |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/106390 |
| work_keys_str_mv | AT wangstephaniemengmassachusettsinstituteoftechnology certifyingchecksumbasedloggingintherapidfscqcrashsafefilesystem |