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

Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke 0001, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell 0001, Ian Stark, Robert N. M. Watson, Peter Sewell. Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. In Rajiv Gupta 0001, Nael B. Abu-Ghazaleh, Madan Musuvathi, Dan Tsafrir, editors, Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, ASPLOS 2024, La Jolla, CA, USA, 27 April 2024- 1 May 2024. pages 181-196, ACM, 2024. [doi]

Abstract

Abstract is missing.