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

静态形式验证是系统软件堆栈最底层的最后一道防线，因为在这些级别上，我们不能依靠动态机制来屏蔽错误、崩溃或恶意攻击。 在过去的十年中，形式验证研究取得了重大进展，但进展受到了精确推断存储在无界堆数据结构中并由函数指针，回调和其他高阶构造操纵的数据值的不变量的棘手挑战的阻碍。 这些问题已经优雅地解决了依赖类型的机器，它利用语法编程纪律，通过数据结构和高阶函数组合传播正确性不变量，从而促进精确的形式验证。然而，依赖类型的主流采用被封锁，因为机器已经在很大程度上开发了交互式证明助手或纯函数式language.This研究的背景下，将开发的理论，算法和所需的工具，使基于依赖类型的软件验证的变革性软件工程的好处，主流的系统编程语言，如C。 为此，PI将使用Liquid Types框架，该框架演示了如何使用强大的抽象解释和软件模型检查来自动推断依赖类型，从而自动化它们在形式验证中的使用。如果成功，这项研究将直接有利于软件开发人员，通过将验证顺利地纳入熟悉的技术（类型），并通过提供丰富的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.