Physical object
A formal CHERI-C memory model
- Documentation:
- 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.
- Publication status:
- Published
Actions
Authors
- Publication date:
- 2022-11-25
- Language:
-
English
- Keywords:
- Pubs id:
-
1310308
- Local pid:
-
pubs:1310308
- Deposit date:
-
2022-11-29
Terms of use
- Copyright holder:
- Park, SH
- Copyright date:
- 2022
- Rights statement:
- Copyright © 2004, contributing authors (see author notice in individual files) All rights reserved.
- Notes:
- This object is available online from Isabelle AFP at: https://www.isa-afp.org/entries/CHERI-C_Memory_Model.html
If you are the owner of this record, you can report an update to it here: Report update to this record