This paper is concerned with reasoning about software running on a capability machine such as CHERI and, in particular, proving that the calling convention ensures proper nesting of function calls no matter how buggy or malicious the function you’re calling may be. It enforces that, if a function returns, it can only return to the return address it was given, with the stack pointer it was given and that it cannot use some other address or stack pointer or even re-use values from some earlier invocation of the function.
The threat model is that neither the caller nor the callee completely trust each other not to be malicious. This requires that the caller and callee respect a new calling convention where the caller is responsible for creating a suitably restricted environment from which to call the callee and the callee is responsible for cleaning up their state before returning to the callee.
The key to implementing this is a new restricted form of capability that can only exist in registers or on the stack (or, more accurately, regions of the memory that have permission to store these capabilities).
The paper explains and motivates the calling convention and then describes proofs that the calling convention achieves the intended goals. It assumes one new hardware primitive that it requires to be efficient: clearing a contiguous region of the stack to prevent capabilities held by a function from leaking into other functions that happen to share the stack.
Notes related to Reasoning about a machine with local capabilities
Capabilities, CHERI architecture
Papers related to Reasoning about a machine with local capabilities
- Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process [nienhuis:secpriv:2020]
- StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities [skorstengaard:popl:2019]
- The CHERI capability model: Revisiting RISC in an age of risk [woodruff:isca:2014]