SHF: Small: Next-Generation, Dependent Type-based Software Model Checking for C

SHF：小型：下一代基于依赖类型的 C 软件模型检查

• 批准号: 1218344
• 负责人: Ranjit Jhala
• 金额: $ 40万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1218344&HistoricalAwards=false
• 关键词: SHF; Small; Next; Generation; Dependent

Static formal verification is a crucial last line of defense at the lowest levels of the systems software stack, as at those levels we cannot fall back on dynamic mechanisms to shield against bugs, crashes, or malicious attacks. The last decade saw significant advances in formal verification research but progress has been hindered by the vexing challenge of precisely inferring invariants of data values that are stored within unbounded heap data structures and manipulated by function pointers, callbacks, and other higher-order constructs. These problems have been elegantly addressed by the machinery of dependent types which exploit a syntactic programming discipline, to compositionally propagate correctness invariants through data structures and higher-order functions, thereby facilitating precise formal verification. However, mainstream adoption of dependent types is blocked as the machinery has been largely developed in the context of interactive proof assistants or purely functional languages.This research will develop the theory, algorithms, and tools required to bring the transformative software engineering benefits of dependent type based software verification to mainstream, systems programming languages like C. To this end the PI will use the framework of Liquid Types which demonstrates how the powerful machinery of abstract interpretation and software model checking can be used to automatically infer dependent types, thereby automating their use in formal verification. If successful, this research will directly benefit software developers, by incorporating verification smoothly within a familiar technology (types), and by providing rich API specifications that will simplify code review and component reuse; program analysis designers, by providing a general framework that can be instantiated to obtain multiple domain- and application- specific verification engines; and ultimately, end users, by providing static guarantees for a variety of critical safety and security and reliability properties.

静态形式验证是系统软件堆栈最低级别的至关重要的最后一道防线，因为在这些级别我们无法依靠动态机制来防范错误、崩溃或恶意攻击。 过去十年，形式验证研究取得了重大进展，但精确推断存储在无界堆数据结构中并由函数指针、回调和其他高阶构造操作的数据值的不变量这一令人烦恼的挑战阻碍了进展。 这些问题已经通过依赖类型机制得到了优雅的解决，依赖类型机制利用句法编程规则，通过数据结构和高阶函数组合地传播正确性不变量，从而促进精确的形式验证。然而，依赖类型的主流采用受到阻碍，因为该机制主要是在交互式证明助手或纯函数语言的背景下开发的。这项研究将开发带来依赖类型的变革性软件工程优势所需的理论、算法和工具基于主流系统编程语言（如 C）的软件验证。为此，PI 将使用 Liquid Types 框架，该框架演示了如何使用强大的抽象解释和软件模型检查机制来自动推断依赖类型，从而自动化它们的使用在形式化验证中。如果成功，这项研究将直接使软件开发人员受益，将验证顺利地融入熟悉的技术（类型）中，并提供丰富的 API 规范来简化代码审查和组件重用；程序分析设计者，通过提供可以实例化以获得多个特定于域和应用程序的验证引擎的通用框架；最终，通过为各种关键的安全性和可靠性属性提供静态保证，最终为最终用户提供服务。