Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour

Gives a mechanised semantics for CHERI C covering capabilities, pointer provenance, and undefined behaviour.

Authors

Vadim ZalivaKayvan MemarianRicardo AlmeidaJessica ClarkeBrooks DavisAlex RichardsonDavid ChisnallBrian CampbellIan StarkRobert WatsonPeter Sewell

Citation

Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell. ACM ASPLOS 2024, 2024.