The first computer ‘mathematically guaranteed’ not to lose any data has been unveiled by researchers at MIT’s Computer Science and Artificial Intelligence Lab.
The research proves the viability of an entirely new type of file-system which is logically unable to forget information accidentally. The work is founded on a processes known as formal verification, which involves describing the limits of operation for a computer program, and then proving the program can’t break those boundaries.
The computer system is not necessarily unable to crash, but the data contained within it cannot be lost.
“What many people worry about is building these file systems to be reliable, both when they’re operating normally but also in the case of crashes, power failure, software bugs, hardware errors, what have you,” Nickolai Zeldovich, a CSAIL principal investigator who co-authored the new paper, said in a press statement.
“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.”
MIT’s new system, which will be demonstrated in full at a symposium this autumn, is unable to lose track of its data even during a crash.
Previous research has proven on paper that a crash-proof system should be possible — at a high level — but MIT’s work is the first to prove it works with the actual code of the file system itself.
Zeldovich and colleagues used a tool called a “proof assistant”, which is a formal proving environment that includes programming code within it. By starting from first principles with the assistant, known as Coq, they defined within the code everything from ‘what is a disk?’ to ‘what is a bit?’. As the proof developed Coq ensured everything within it was logically consistent.
Using this the team was able to prove their lossless concept works, and did so within the code of the file system itself. The result is a relatively slow system — for now — but one which provides the groundwork for future computers which would be much more resilient against problems or interference.
“It’s not like people haven’t proven things in the past,” said Ulfar Erlingsson, lead manager for security research at Google, in a statement. “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.
“But I can say for certain that Adam’s stuff with Coq, and separation logic, this is stuff that’s going to get built on and applied in many different domains. That’s what’s so exciting.”
It is hoped the work at MIT could lead to more reliable, efficient computers. “It’s not like you could look up a paper that says, ‘This is the way to do it.'” said Frans Kaashoek, the Charles A. Piper Professor at MIT’s Department of Electrical Engineering and Computer Science, who also worked on the paper. “But now you can read our paper and presumably do it a lot faster.”