StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

Lau Skorstengaard, Dominique Devriese, Lars Birkedal
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 03 March 2020

Proc. ACM Program. Lang. 3(POPL)
Association for Computing Machinery
New York, NY, USA
January 2019
Topic(s): security verification
Note(s): hardware, CHERI architecture, capabilities
Papers: skorstengaard:esop:2018

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!

Capabilities, CHERI architecture