### 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

- Computer science/Semantics and reasoning

### Related publications

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

### Session CHERI-C_Memory_Model

- Preliminary_Library
- CHERI_C_Concrete_Memory_Model
- CHERI_C_Global_Environment

### Depends on

- Light-weight Containers
- Separation Algebra
- Finite Machine Word Library

## Cite

×

CHERI-C_Memory_Model-AFP

    @article{CHERI-C_Memory_Model-AFP,
      author  = {Seung Hoon Park},
      title   = {A Formal CHERI-C Memory Model},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/CHERI-C_Memory_Model.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Nov 28, 2022 : Isabelle2022