Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management
The work
| Authors | Lau Skorstengaard; Dominique Devriese; Lars Birkedal |
|---|---|
| Editors | |
| Type | article |
| Year | 2020 |
| Also known as | skorstengaard2019reasoning |
| Citekey | skorstengaard2020reasoning |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 42 |
| Issue | 1 |
| Pages | 1--53 |
Identifiers
| DOI | 10.1145/3363519 |
|---|---|
| OpenAlex | W2995538315 |
Access
| Landing page | https://doi.org/10.1145/3363519 |
|---|
Related
| Distinct from | skorstengaard2018reasoning |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 04:49 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{skorstengaard2020reasoning,
title = {Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management},
author = {Lau Skorstengaard and Dominique Devriese and Lars Birkedal},
year = {2020},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery},
volume = {42},
number = {1},
pages = {1--53},
doi = {10.1145/3363519},
}
This record lives at https://refs.drheap.org/skorstengaard2020reasoning/ and will keep
doing so. It used to be called skorstengaard2019reasoning, and those addresses still resolve to this one.