CN: A separation-logic refinement type system for production systems code verification

Add to your list(s) Download to your calendar using vCal

• Neel Krishnaswami (University of Cambridge)
• Friday 08 July 2022, 16:00-17:00
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

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).  

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.