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.

@article{paperbot695,
  title = {Reasoning about a Machine with Local Capabilities},
  author = {Lau Skorstengaard and Dominique Devriese and Lars Birkedal},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {42},
  number = {1},
  year = {2019},
  doi = {10.1145/3363519}
}