Physical object icon

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

Expand documentation
Publication status:
Published

Actions


Access Document


Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
ORCID:
0000-0001-7165-6857
More from this funder
Name:
Engineering and Physical Sciences Research Council
Grant:
EP/V000225/1
Publication date:
2022-11-25
Language:
English
Keywords:
Pubs id:
1310308
Local pid:
pubs:1310308
Deposit date:
2022-11-29

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP