End-to-End Data Reliability with Runtime Verification

几项研究表明，由于软件缺陷导致的故障占系统总停机时间的25-35%，仅在美国每年就造成600亿美元的损失。当软件错误导致磁盘上的数据损坏时，会发生一种特别严重的故障。与瞬时内存故障不同，数据损坏不能通过重新启动系统或使用硬件可靠性技术（如存储冗余）来解决。相反，需要复杂的恢复过程，而且它们往往容易出错。例如，从备份中恢复数据很耗时，而且有丢失最近工作的风险。

Several studies have shown that failures due to software bugs account for 25-35% of the total system downtime and cost $60 billion annually in the US alone. A particularly severe type of failure occurs when a software bug causes corruption of data on disk. Unlike transient memory failures, data corruption cannot be resolved by restarting the system, or by using hardware reliability techniques, such as storage redundancy. Instead, complex recovery procedures are needed, and they tend to be error-prone. For instance, restoring data from a backup is time-taking and risks loss of recent work. The goal of the proposed research is to prevent data corruption on disk in the face of arbitrary application bugs and vulnerabilities, thereby minimizing the need for expensive and error-prone disaster recovery solutions. We plan to address this challenging problem by using a technique based on runtime verification. The key idea is to detect faults by observing disk input/output behavior, and then verifying that disk updates satisfy an application's consistency requirements. Unlike traditional formal verification techniques, such as model checking, that statically verify a simplified model of the target system, runtime verification is performed continuously on the real system, thereby providing assurance that the implementation matches its specification. We expect that this research will have a significant impact on the design of reliable software systems, especially storage-based applications.