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

点击翻译按钮获取中文摘要

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.