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

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

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.