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

The CHERI research project has shown how one can provide radically improved security for that existing codebase with minimal modification, using unforgeable hardware capabilities in place of machine-word pointers in CHERI dialects of C, implemented as adaptions of Clang/LLVM and GCC.