Using Model Checking to Find Serious File System Errors
by Madanlal Musuvathi, Dawson Engler, Paul Twohey, Junfeng Yang
show details
Details
| url: | http://www.cs.cmu.edu/~15712/papers//yang04.pdf | | abstract: | This paper shows how to use model checking to find serious errors in file systems. Model checking is a for- mal verification technique tuned for finding corner-case errors by comprehensively exploring the state spaces de- fined by a system. File systems have two dynamics that make them attractive for such an approach. First, their errors are some of the most serious, since they can de- stroy persistent data and lead to unrecoverable corrup- tion. Second, traditional testing needs an impractical, exponential number of test cases to check that the sys- tem will recover if it crashes at any point during execu- tion. Model checking employs a variety of state-reducing techniques that allow it to explore such vast state spaces efficiently.
We built a system, FiSC, for model checking file sys- tems. We applied it to three widely-used, heavily-tested file systems: ext3 [13], JFS [21], and ReiserFS [27]. We found serious bugs in all of them, 32 in total. Most have led to patches within a day of diagnosis. For each file system, FiSC found demonstrable events leading to the unrecoverable destruction of metadata and entire direc- tories, including the file system root directory “/”. |
|
|
You need to log in to add tags and post comments.
