RefinedC: automating the foundational verification of C code with refined ownership types
RefinedC: automating the foundational verification of C code with refined ownership types
复制标题
DOI：
10.1145/3453483.3454036
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
Michael Sammler;Rodolphe Lepigre;R. Krebbers;Kayvan Memarian;Derek Dreyer;D. Garg
中科院分区：
文献类型：
--
作者：
Michael Sammler;Rodolphe Lepigre;R. Krebbers;Kayvan Memarian;Derek Dreyer;D. Garg
鉴于C在系统软件中继续扮演的核心角色以及编写安全和正确的C代码的困难，因此在本文中开发有效的正式方法是一个巨大的挑战。问题：我们称之为精炼的类型系统，将所有权类型（用于共享状态和并发性的模块化推理）与改进类型（用于编码C数据类型上的精确不变式，以及用于C函数的HOARE风格规格）。需要最小的用户干预）和基础（在COQ中产生程序正确性的证明），同时处理一系列低级编程成语，例如指针算术。精制类型系统是通过将基于COQ的IRIS框架解释为高阶并发分离逻辑的合理性锂限制了分离逻辑的仔细选择（但表达性的）片段，锂支持可预测的，自动的，目标定向的证明搜索，而无需进行回溯。
Given the central role that C continues to play in systems software, and the difficulty of writing safe and correct C code, it remains a grand challenge to develop effective formal methods for verifying C programs. In this paper, we propose a new approach to this problem: a type system we call RefinedC, which combines ownership types (for modular reasoning about shared state and concurrency) with refinement types (for encoding precise invariants on C data types and Hoare-style specifications for C functions). RefinedC is both automated (requiring minimal user intervention) and foundational (producing a proof of program correctness in Coq), while at the same time handling a range of low-level programming idioms such as pointer arithmetic. In particular, following the approach of RustBelt, the soundness of the RefinedC type system is justified semantically by interpretation into the Coq-based Iris framework for higher-order concurrent separation logic. However, the typing rules of RefinedC are also designed to be encodable in a new “separation logic programming” language we call Lithium. By restricting to a carefully chosen (yet expressive) fragment of separation logic, Lithium supports predictable, automatic, goal-directed proof search without backtracking. We demonstrate the effectiveness of RefinedC on a range of representative examples of C code.