A CHERI C memory model for verified temporal safety

Vadim Zaliva; Kayvan Memarian; Brian Campbell; Ricardo Almeida; Nathaniel Filardo; Ian Stark; Peter Sewell

doi:10.1145/3703595.3705878

A CHERI C memory model for verified temporal safety

Vadim Zaliva
, Kayvan Memarian
, Brian Campbell
, Ricardo Almeida
, Nathaniel Filardo
, Ian Stark
, Peter Sewell

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Memory safety concerns continue to be a major source of security vulnerabilities. The CHERI architecture, as instantiated in prototype CHERI-RISC-V cores, the Arm Morello system, and Microsoft’s CHERIoT embedded core, provides fine-grained memory access control through unforgeable hardware capabilities. The impact of CHERI on spatial memory safety is well understood. This paper systematically examines temporal memory safety within CHERI C – a dialect of the C programming language for CHERI – and proposes a formal approach to defining and ensuring it. In particular: 1) we examine the impact of five existing capability revocation mechanisms on CHERI C semantics and present a specialised object memory model tailored to CHERI C; 2) we introduce a new CHERI-specific pointer provenance tracking scheme; and 3) we formally define the security guarantees provided by this memory model, supported by a Coq proof of their correctness, expressed as invariants of the memory state.

Original language	English
Title of host publication	Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’25)
Place of Publication	New York, NY, USA
Publisher	ACM
Pages	1-15
Number of pages	15
DOIs	https://doi.org/10.1145/3703595.3705878
Publication status	Accepted/In press - 19 Nov 2024
Event	The 14th ACM SIGPLAN International Conference on Certified Programs and Proofs - Curtis Hotel, Denver, United States Duration: 19 Jan 2025 → 25 Jan 2025 Conference number: 14 https://popl25.sigplan.org/home/CPP-2025

Conference

Conference	The 14th ACM SIGPLAN International Conference on Certified Programs and Proofs
Abbreviated title	CPP 2025
Country/Territory	United States
City	Denver
Period	19/01/25 → 25/01/25
Internet address	https://popl25.sigplan.org/home/CPP-2025

Keywords / Materials (for Non-textual outputs)

CHERI
memory safety
temporal safety
formal verification
memory model
pointer provenance
C language
Coq
capability revocation

Access to Document

10.1145/3703595.3705878

ZalivaEtalCPP2025ACHERICMemoryModelAccepted author manuscript, 564 KBLicence: Creative Commons: Attribution (CC-BY)

1 Finished
1 Active

Copy of Secure Foundations: Verified Systems Software Above Full-Scale Integrated Semantics
Stark, I. (Principal Investigator)
University of Cambridge
1/05/24 → 30/04/29
Project: Research
Digital Security by Design (DSbD) Technology Platform Prototype
Stark, I. (Principal Investigator)
Innovate UK
1/11/19 → 28/02/25
Project: Research

Cite this

@inproceedings{ce4d0dec9f3c461396c6cac337297469,

title = "A CHERI C memory model for verified temporal safety",

abstract = "Memory safety concerns continue to be a major source of security vulnerabilities. The CHERI architecture, as instantiated in prototype CHERI-RISC-V cores, the Arm Morello system, and Microsoft{\textquoteright}s CHERIoT embedded core, provides fine-grained memory access control through unforgeable hardware capabilities. The impact of CHERI on spatial memory safety is well understood. This paper systematically examines temporal memory safety within CHERI C – a dialect of the C programming language for CHERI – and proposes a formal approach to defining and ensuring it. In particular: 1) we examine the impact of five existing capability revocation mechanisms on CHERI C semantics and present a specialised object memory model tailored to CHERI C; 2) we introduce a new CHERI-specific pointer provenance tracking scheme; and 3) we formally define the security guarantees provided by this memory model, supported by a Coq proof of their correctness, expressed as invariants of the memory state. ",

keywords = "CHERI, memory safety, temporal safety, formal verification, memory model, pointer provenance, C language, Coq, capability revocation",

author = "Vadim Zaliva and Kayvan Memarian and Brian Campbell and Ricardo Almeida and Nathaniel Filardo and Ian Stark and Peter Sewell",

year = "2024",

month = nov,

day = "19",

doi = "10.1145/3703595.3705878",

language = "English",

pages = "1--15",

booktitle = "Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP {\textquoteright}25)",

publisher = "ACM",

note = "The 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025 ; Conference date: 19-01-2025 Through 25-01-2025",

url = "https://popl25.sigplan.org/home/CPP-2025",

}

Zaliva, V, Memarian, K, Campbell, B, Almeida, R, Filardo, N, Stark, I & Sewell, P 2024, A CHERI C memory model for verified temporal safety. in Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’25). ACM, New York, NY, USA, pp. 1-15, The 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, Denver, Colorado, United States, 19/01/25. https://doi.org/10.1145/3703595.3705878

TY - GEN

T1 - A CHERI C memory model for verified temporal safety

AU - Zaliva, Vadim

AU - Memarian, Kayvan

AU - Campbell, Brian

AU - Almeida, Ricardo

AU - Filardo, Nathaniel

AU - Stark, Ian

AU - Sewell, Peter

N1 - Conference code: 14

PY - 2024/11/19

Y1 - 2024/11/19

N2 - Memory safety concerns continue to be a major source of security vulnerabilities. The CHERI architecture, as instantiated in prototype CHERI-RISC-V cores, the Arm Morello system, and Microsoft’s CHERIoT embedded core, provides fine-grained memory access control through unforgeable hardware capabilities. The impact of CHERI on spatial memory safety is well understood. This paper systematically examines temporal memory safety within CHERI C – a dialect of the C programming language for CHERI – and proposes a formal approach to defining and ensuring it. In particular: 1) we examine the impact of five existing capability revocation mechanisms on CHERI C semantics and present a specialised object memory model tailored to CHERI C; 2) we introduce a new CHERI-specific pointer provenance tracking scheme; and 3) we formally define the security guarantees provided by this memory model, supported by a Coq proof of their correctness, expressed as invariants of the memory state.

AB - Memory safety concerns continue to be a major source of security vulnerabilities. The CHERI architecture, as instantiated in prototype CHERI-RISC-V cores, the Arm Morello system, and Microsoft’s CHERIoT embedded core, provides fine-grained memory access control through unforgeable hardware capabilities. The impact of CHERI on spatial memory safety is well understood. This paper systematically examines temporal memory safety within CHERI C – a dialect of the C programming language for CHERI – and proposes a formal approach to defining and ensuring it. In particular: 1) we examine the impact of five existing capability revocation mechanisms on CHERI C semantics and present a specialised object memory model tailored to CHERI C; 2) we introduce a new CHERI-specific pointer provenance tracking scheme; and 3) we formally define the security guarantees provided by this memory model, supported by a Coq proof of their correctness, expressed as invariants of the memory state.

KW - CHERI

KW - memory safety

KW - temporal safety

KW - formal verification

KW - memory model

KW - pointer provenance

KW - C language

KW - Coq

KW - capability revocation

U2 - 10.1145/3703595.3705878

DO - 10.1145/3703595.3705878

M3 - Conference contribution

SP - 1

EP - 15

BT - Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’25)

PB - ACM

CY - New York, NY, USA

T2 - The 14th ACM SIGPLAN International Conference on Certified Programs and Proofs

Y2 - 19 January 2025 through 25 January 2025

ER -

A CHERI C memory model for verified temporal safety

Abstract

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Copy of Secure Foundations: Verified Systems Software Above Full-Scale Integrated Semantics

Digital Security by Design (DSbD) Technology Platform Prototype

Cite this