End-to-End Data Reliability with Runtime Verification

通过运行时验证实现端到端数据可靠性

• 批准号: 298289-2012
• 负责人: Goel, Ashvin
• 金额: $ 1.6万
• 依托单位: University of Toronto
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=571464
• 关键词: End; Data; Reliability; Runtime; Verification

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.

多项研究表明，由于软件错误导致的故障占系统总停机时间的 25-35%，仅在美国每年就造成 600 亿美元的损失。当软件错误导致磁盘上的数据损坏时，就会发生一种特别严重的故障。与瞬时内存故障不同，数据损坏无法通过重新启动系统或使用硬件可靠性技术（例如存储冗余）来解决。相反，需要复杂的恢复过程，并且它们往往容易出错。例如，从备份恢复数据非常耗时，并且有丢失最近工作的风险。 拟议研究的目标是防止磁盘上的数据在任意应用程序错误和漏洞的情况下损坏，从而最大限度地减少对昂贵且容易出错的灾难恢复解决方案的需求。我们计划通过使用基于运行时验证的技术来解决这个具有挑战性的问题。关键思想是通过观察磁盘输入/输出行为来检测故障，然后验证磁盘更新是否满足应用程序的一致性要求。与静态验证目标系统的简化模型的传统形式验证技术（例如模型检查）不同，运行时验证是在真实系统上连续执行的，从而保证实现符合其规范。我们预计这项研究将对可靠软件系统的设计产生重大影响，特别是基于存储的应用程序。