MIT researchers readying ‘crash-tolerant’ computer system th
Source: Andrew Blake
Computer crashes might soon be a lot less catastrophic as scientists at MIT are preparing to release a system they claim will be mathematically guaranteed not to lose data in the event of a crash.
Whether on a Mac, Windows or Linux machine, operating systems of all sorts contain a “file system” where all user data is stored in an (ideally) reliable and accessible manner. When a computer crashes, however, it’s sometimes the case that data that’s being written or retrieved from that system becomes unexpectedly corrupted, potentially causing all sorts of problems for the rest of the computer and its applications, not to mention the user who often cannot recover lost or damaged data.
MIT researchers have reportedly designed a file system that can make these types of issues impossible and claimed to have mathematically verified its reliability.
Those findings won’t be formally unveiled until a symposium at the university later this year. But in an announcement by MIT on Monday, computer-science professors working on the project gave a preview of how they think they’re on the road to revolutionizing the way operating systems write and read digital data.
“Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash. You literally have to consider every instruction or every disk operation and think, ‘Well, what if I crash now? What now? What now?’ And so empirically, people have found lots of bugs in file systems that have to do with crash recovery, and they keep finding them, even in very well-tested file systems, because it’s just so hard to do,” said Nickolai Zeldovich, an associate professor at the school and one-third of the team responsible for the research.
To set the MIT team apart from previous studies, the researchers constructed a proof for the infallible file system, then developed its actual code and tested it using formal verification ― a process of determining the acceptable bounds of operation for a system and mathematically proving that they’ll never be exceeded.
Unlike other recent proposals, the team members said they checked their works against the actual, completed file system, and “not some whiteboard idealization that has no formal connection to the code,” said Adam Chlipala, associate professor of computer science and co-author.
“All these paper proofs about other file systems may actually be correct, but there’s no file system that we can be sure represents what the proof is about,” said Daniel Ziegler, a co-author and undergraduate with MIT’s Department of Electrical Engineering and Computer Science.
Ulfar Erlingsson, a security researcher at Google who has been watching the MIT team said that while “it’s not like people haven’t proven things in the past,” this development looks more promising.
“But usually the methods and technologies, the formalisms that were developed for creating the proofs, were so esoteric and so specific to the problem that there was basically hardly any chance that there would be repeat work that built up on it.”
“[T]his is stuff that’s going to get built on and applied in many different domains ― that’s what’s so exciting,” he said of the MIT research.
The team’s findings are scheduled to be discussed at the ACM Symposium on Operating Systems Principles in October.
| }
|