分享至
摘要：麻省理工学院研究人员Nickolai Zeldovich和他的同事们在创建了一个文件系统，他们声称该文件系统在数学上证明不受任何意外的系统崩溃影响。该团队在形式验证的基础上开发了这套文件系统。这本身并不是全新成果，但是他们正式证明了他们编写的最终代码坚不可摧，而不是证明一些高层次的流程图描述系统。
Nickolai Zeldovich表示，确保文件系统可以从系统崩溃中恢复比较棘手，因为有这么多不同的地方需要考虑和处理，你必须考虑每个指令或每个磁盘操作，发现系统崩溃原因，找出处理方式，找出系统崩溃时文件系统中的海量错误，并且随时试图纠正这些错误。因此即使是在非常行之有效的文件系统，确保文件系统可以从系统崩溃中恢复不仅棘手而且耗时。
Nickolai Zeldovich相信他们开发的这套文件系统可应用到其他设计当中，他们这个项目历经了10次改写，他们花费90%的时间来定义组件，以及它们之间的关系和实际的形式证明。他们可能没有太多的时间优化这套文件系统。该小组在开发过程中使用Coq证明助手。
MIT研究小组的工作已经引起行业一些成员关注。 谷歌首席安全经理 lfar Erlingsson表示，说，现有正式设计主要针对特定的文件系统，在重复使用上变化不大。与此相反，MIT的工作可以被用作许多不同应用程序的基础。
该小组将在10月份举行的操作系统原则ACM研讨会上展示他们的研究成果。
本文来源：cnbeta网站
责任编辑：
王晓易_NE0011
