In this work, we present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potentially null-terminated arrays. We formalize this model in Coq, and prove that any spatial memory safety errors can be blamed on portions of the program labeled unchecked; this is a Checked C feature that supports incremental porting and backward compatibility. Our model develops an operational semantics that uses fat pointers to guarantee spatial safety. However, we formalize a compilation scheme that can yield thin pointers, with bounds information managed using inserted code. We show that the generated code faithfully simulates the original. Finally, we build an executable version of our model in PLT Redex, and use a custom random generator for well-typed and almost-well-typed terms to find inconsistencies between our model and the Clang Checked C implementation. We find this a useful way to co-develop a language (Checked C is still in development) and a core model of it.

@inproceedings{li22checkedc,
  author = {Liyi Li and Yiyun Liu and Deena L. Postol and Leonidas Lampropoulos and David Van Horn and Michael Hicks},
  title = {A Formal Model of {Checked C}},
  booktitle = {Proceedings of the Computer Security Foundations Symposium (CSF)},
  note = {Conditionally accepted},
  month = jun,
  year = 2022
}

This file was generated by bibtex2html 1.99.