RefinedC: An Extensible Refinement Type System for C Based on Separation Logic Programming

Although the C and C++ programming languages are by their very nature unsafe, they nevertheless power most of the lower layers of the software stack, including hypervisors and operating systems. As a consequence, many critical systems remain vulnerable to safety and functional correctness issues, which can lead to crashes and security breaches. To improve on this situation, we propose a new approach to verifying the correctness of idiomatic C code, called RefinedC—a type system combining ownership types (to ensure memory safety) with refinement types (to ensure functional correctness). RefinedC is built atop a new “separation logic programming” language we call Lithium, which supports automatic proof search by backchaining, but without the need for backtracking. By virtue of its representation as a Lithium program, RefinedC’s type system is fundamentally extensible, meaning that the set of typing rules is not fixed and can be grown over time by adding new clauses to the Lithium program. We show that this extensibility is key to supporting numerous low-level idioms (e.g., involving pointer manipulations) which C programmers employ in practice. RefinedC and Lithium are embedded in the Iris framework for concurrent separation logic in Coq, allowing us to foundationally certify the result of the RefinedC type checker, including user-defined extensions.