Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management

Lau Skorstengaard; Dominique Devriese; Lars Birkedal

doi:10.1145/3363519

Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management

Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Informatics and Applied Informatics

Research output: Contribution to journal › Article › peer-review

11 Citations (Scopus)

933 Downloads (Pure)

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.

Original language	English
Article number	5
Pages (from-to)	5:1-5:53
Number of pages <span style="color:red"p> <font size="1.5"> ✽ </span> </font>	53
Journal	ACM Trans. Program. Lang. Syst.
Volume	42
Issue number	1
DOIs	https://doi.org/10.1145/3363519
Publication status	Published - 1 Dec 2019

Keywords

well-bracketed control flow
CHERI
logical relations
stack encapsulation
local capabilities
secure compilation
Capability machines

Access to Document

10.1145/3363519

paper-submission-v5Accepted author manuscript, 801 KBLicence: CC BY-NC

https://doi.org/10.1145/3363519

FWOAL910: ERC-Opvangproject: Low-level Object Capabilities, Formally
Devriese, D.
1/02/19 → 1/10/21
Project: Fundamental

Cite this

@article{2bcfe4015025411ba8ecc6a8926d490d,

title = "Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management",

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.",

keywords = "well-bracketed control flow, CHERI, logical relations, stack encapsulation, local capabilities, secure compilation, Capability machines",

author = "Lau Skorstengaard and Dominique Devriese and Lars Birkedal",

year = "2019",

month = dec,

day = "1",

doi = "10.1145/3363519",

language = "English",

volume = "42",

pages = "5:1--5:53",

journal = "ACM Trans. Program. Lang. Syst.",

issn = "0164-0925",

publisher = "Association for Computing Machinery",

number = "1",

}

TY - JOUR

T1 - Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management

AU - Skorstengaard, Lau

AU - Devriese, Dominique

AU - Birkedal, Lars

PY - 2019/12/1

Y1 - 2019/12/1

N2 - 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.

AB - 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.

KW - well-bracketed control flow

KW - CHERI

KW - logical relations

KW - stack encapsulation

KW - local capabilities

KW - secure compilation

KW - Capability machines

U2 - 10.1145/3363519

DO - 10.1145/3363519

M3 - Article

VL - 42

SP - 5:1-5:53

JO - ACM Trans. Program. Lang. Syst.

JF - ACM Trans. Program. Lang. Syst.

SN - 0164-0925

IS - 1

M1 - 5

ER -

Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management

Abstract

Keywords

Access to Document

Fingerprint

Projects

FWOAL910: ERC-Opvangproject: Low-level Object Capabilities, Formally

Cite this