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

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

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.