log in  |  register  |  feedback?  |  help  |  web accessibility
RefinedC: An Extensible Refinement Type System for C Based on Separation Logic Programming
Liyi Li - University of Maryland, College Park
Tuesday, December 8, 2020, 4:15-5:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)

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.

Paper: https://plv.mpi-sws.org/refinedc/paper.pdf
Zoom: https://umd.zoom.us/j/98723227318?pwd=K0RJZVZZM1Jhd2laMlg1ajgvUjltQT09


Liyi Li is a Basili Postdoctoral Fellow at UMD.

This talk is organized by Ian Sweet