A Formal CHERI-C Memory Model

Seung Hoon Park 🌐

November 25, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs with uncompressed capabilities in a 'purecap' environment. We present a CHERI-C memory model theory with properties suitable for verification and potentially other types of analyses. Our theory generates an OCaml executable instance of the memory model, which is then used to instantiate the parametric Gillian program analysis framework, enabling concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss.

License

BSD License

Topics

Related publications

  • Park, S. H., Pai, R., & Melham, T. (2022). A Formal CHERI-C Semantics for Verification (Version 2). arXiv. https://doi.org/10.48550/ARXIV.2211.07511

Session CHERI-C_Memory_Model