Abstract

CN is a type system for C code, aimed at verifying the safety and functional correctness of systems C code (i.e., the kind found in kernels and hypervisors). Verification of C code is by no means a novel objective, but the aim of CN is to yield a developer experience that is much more like using a conventional type checker (albeit one with rich types) than using a full-fledged proof assistant. The goal (not achieved yet!) is for CN to process moderately-annotated source code and to reliably, predictably, and reasonably quickly return either a confirmation that the code satisfies the specifications, or an error message that gives useful feedback as to why not. This contrasts with the experience of using a proof assistant like Coq, which deliberately sacrifices reliability and predictability in order to permit users to write heuristics and tactics to do proof search.  In our talk, we will discuss the design and implementation of the CN type system, demonstrating some of the tooling we havebuilt (based on the Visual Studio Code Language Server Protocol), by showing what CN code looks like when we are writing specifications for (part of) the pKVM hypervisor which is intended to underlie Android in the future. This will show both the strengths (CN works on actual C systems code we didn’t write ourselves!) and the weaknesses of our approach (C idioms which are hard to capture with our approach, such as offset calculations involving nonlinear arithmetic).