Future filesystems: mechanized specification, validation, implementation and verification of filesystems

未来的文件系统：文件系统的机械化规范、验证、实现和验证

• 批准号: EP/K022741/1
• 负责人: Tom Ridge
• 金额: $ 11.69万
• 依托单位: University of Leicester
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2013
• 资助国家: 英国
• 起止时间: 2013 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FK022741%2F1
• 关键词: Future; filesystems; mechanized; specification; validation

Filesystems are extremely important. Users depend on filesystems to store their files whenever they hit "save". Businesses rely on databases to store their data safely, and these databases in turn rely on the filesystem.Modern filesystems are designed to satisfy many complicated requirements. As a result, implementations are beset with problems. The implementation code is extremely complex, and almost inevitably contains bugs. These bugs can and do lead to data corruption and loss. Development time is very lengthy. Testing is also very lengthy and costly, and does not guarantee to eliminate all bugs. It is often unclear to application developers what guarantees a filesystem provides, so that it becomes extremely difficult to write correct applications for a given filesystem, let alone applications that are portable across different filesystems.Even NASA was adversely affected by poor filesystem design. On January 21 2004, mission control lost contact with the Mars Exploration Rover (MER) Spirit. Fortunately Spirit had been equipped with a "crippled mode capability" to cope with unforeseen errors, and together with extensive efforts by the operations team, Spirit was returned to operational status 16 days later on February 6. The official report states: "the root cause of the anomaly was a design error in the software module that provides file system services". Without crippled mode capability, "the MER mission may well have been lost". The cost of the mission was estimated at over US$ 800 million.What can be done to tackle these problems? For many decades, computer scientists have been developing techniques for producing dependable systems. One approach that is receiving much current interest is verification and correctness i.e. mathematical proof that software is correct according to its specification. The widespread need in the digital economy for reliable and dependable systems means that research in this area is increasingly important.In 2003, Tony Hoare proposed a verification grand challenge for the following 15 years: a verified compiler. Following the NASA MER anomaly, two NASA research scientists, Rajeev Joshi and Gerard Holzmann, proposed a more tractable challenge: to build a verifiable filesystem. We will take up this challenge, and specify and build a verified filesystem.This work is foundational in nature, but tackles the complexities of real-world systems. We will use very sophisticated and high-level logical techniques combined with state-of-the-art software development techniques to address the full complexity of real-world systems. The verified filesystem has the potential to impact both technologically highly sophisticated organizations such as NASA and internet giants such as Google, Amazon and Facebook, whilst also delivering benefits to end users. A verified filesystem can have a significant impact on many areas of the digital economy. For example, an ultra-reliable filesystem is a key part of the quest for ultra-reliable computing infrastructure, which in turn contributes to the goal of delivering information technology as a utility. Finally, in addition to real-world impact, this research will provide a solid mathematical foundation for further research and verification of critical applications that make use of filesystem functionality, such as databases and persistent message queues.

文件系统非常重要。用户依赖于文件系统来存储他们的文件，每当他们点击“保存”。企业依靠数据库来安全地存储数据，而这些数据库又依赖于文件系统。现代文件系统被设计为满足许多复杂的需求。因此，实施过程中遇到了很多问题。实现代码非常复杂，几乎不可避免地包含bug。这些错误可能并且确实会导致数据损坏和丢失。开发时间非常漫长。测试也是非常漫长和昂贵的，并不能保证消除所有的错误。应用程序开发人员通常不清楚文件系统提供了什么保证，因此为给定的文件系统编写正确的应用程序变得非常困难，更不用说跨不同文件系统的可移植应用程序了。2004年1月21日，使命控制中心与火星探测漫游车（MER）精神号失去联系。幸运的是，勇气号已经配备了一种“残废模式能力”，以科普不可预见的错误，在运营团队的广泛努力下，勇气号在16天后的2月6日恢复了运营状态。官方报告指出：“异常的根本原因是提供文件系统服务的软件模块中的设计错误”。如果没有残废模式能力，“MER使命很可能已经失败”。这项使命的费用估计超过8亿美元，如何解决这些问题？几十年来，计算机科学家一直在开发生产可靠系统的技术。一种方法，是接收当前的兴趣是验证和正确性，即数学证明，软件是正确的，根据其规格。数字经济对可靠和可依赖系统的广泛需求意味着这一领域的研究越来越重要。2003年，Tony Hoare提出了一个验证的大挑战，为随后的15年：验证编译器。在NASA MER异常之后，两位NASA研究科学家Rajeev Joshi和Gerard Holzmann提出了一个更容易处理的挑战：构建一个可验证的文件系统。我们将接受这一挑战，并指定和构建一个经过验证的文件系统。这项工作本质上是基础性的，但要解决现实世界系统的复杂性。我们将使用非常复杂和高级的逻辑技术与最先进的软件开发技术相结合，以解决现实世界系统的全部复杂性。经过验证的文件系统有可能影响技术高度复杂的组织，如NASA和互联网巨头，如谷歌，亚马逊和Facebook，同时也为最终用户带来好处。经过验证的文件系统可以对数字经济的许多领域产生重大影响。例如，超可靠的文件系统是寻求超可靠的计算基础设施的关键部分，这反过来又有助于实现将信息技术作为一种实用工具提供的目标。最后，除了现实世界的影响，这项研究将提供一个坚实的数学基础，进一步研究和验证的关键应用程序，利用文件系统的功能，如数据库和持久的消息队列。

项目成果

SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems

• DOI: 10.1145/2815400.2815411
• 发表时间: 2015-10
• 期刊: Proceedings of the 25th Symposium on Operating Systems Principles
• 作者: T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell