The downgrading semantics of memory safety (Extended version)
This paper presents the first formal semantics for the downgrading capabilities in CHERI-C/C++, describing how capabilities lose permissions and bounds during execution, and providing a foundation for reasoning about temporal memory safety properties.