A Formal CHERI-C Memory Model (Q7361858)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry CHERI-C_Memory_Model
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Formal CHERI-C Memory Model |
AFP entry CHERI-C_Memory_Model |
Statements
25 November 2022
0 references
Seung Hoon Park
0 references
A Formal CHERI-C Memory Model (English)
0 references
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.
0 references
0 references
