This paper follows on from an earlier paper by the same authors that looked at how mutually distrusting pieces of code could safely call each other. In particular, it was concerned about whether the stack and return address were what the caller expected when they called the function.
The earlier paper relied on capability machines that provided “local capabilities” and a primitive for clearing the stack on function return. This paper relies on capability machines that provide “linear capabilities”. Linear capabilities are interesting because they cannot be duplicated: if you attempt to copy a linear capability then the source copy is erased. A consequence of this is that linear capabilities support two extra operations: “split” to partition the memory region accessible by a capability and “splice” to merge two adjacent capabilities back into a single capability. They make essential use of “splice” as part of enforcing that a callee has returned the entire stack when it returns.
The earlier paper showed how to reason about some example code. This paper develops “fully abstract overlay semantics” which is an alternative semantics for machine code that has an explicit stack and restricts the code to only use the stack in the way that a compiler might expect. By doing this, they define what they mean by “well bracketed control flow” and they explicitly link the property that they prove to the requirements that a compiler might have on the code. Nice!
Notes related to StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
Papers related to StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
- Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process [nienhuis:secpriv:2020]
- Reasoning about a machine with local capabilities [skorstengaard:esop:2018]
- The CHERI capability model: Revisiting RISC in an age of risk [woodruff:isca:2014]