Toward Complete Stack Safety for Capability Machines
Capability machines are computers that provide support for fine grained control over memory accesses. Pointers are replaced by capabilities, unforgeable tokens of authority that represent the ability to access a memory location. As such, capability machines are an attractive target for secure compilation, and this interest is further compounded by the recent commitment from Arm to develop an industrial prototype of CHERI-based capability machines. It is thus no surprise that numerous recent works have proposed techniques for enforcing well-bracketed control-flow (WBCF) and local state encapsulation (LSE), temporal stack safety, or temporal heap safety. However, these solutions still fall short of ensuring what we believe to be complete stack safety. In this paper, we review recent propositions from the literature and identify limitations. We further propose a potential solution using a new form of capabilities.