CN: Verifying Systems C Code with Separation-Logic Refinement Types

on YouTube ↗24m

" summary

CN is a separation-logic refinement type system for ISO C that uses a Cerberus translation to a core language, implements resource types as first-class resources, and reduces refinements to decidable SMT queries via Liquid-type style constraints solved by C3. It is implemented in OCaml, has a formal soundness proof for type checking, and verifies a real pkvm component: the allocator (the verified C is 364 lines C and yields ~5.9× verification overhead), with type checking taking about 155 seconds.

AI-written summary · about

" chapters (9)

1. 0:00Introduction to CN
2. 1:55The PKVM use case
3. 3:04Key challenges and design
4. 4:48Cerberus and C semantics
5. 7:15Refinement types approach
6. 9:26Resource ownership in C
7. 12:04Handling quantifiers
8. 16:03Case study and evaluation
9. 20:04Future work and discussion