Academic paper
Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour
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.
Gives a mechanised semantics for CHERI C covering capabilities, pointer provenance, and undefined behaviour.
