Cerise: program verification on a capability machine in the presence of untrusted code

DOI10.1145/3623510MaRDI QIDQ7031994zbMATH OpenFDO

Authors A. Georges, Armaël Guéneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

Publication date 5 February 2025

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3623510

zbMATH Keywords

capability machinescapability safetyCHERIprogram logicseparation logicuniversal contracts

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A bisimulation for dynamic sealing
• Hardware-Based Trusted Computing Architectures for Isolation and Attestation
• Interactive proofs in higher-order concurrent separation logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Programming semantics for multiprogrammed computations
• Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
• The impact of higher-order state and control effects on local relational reasoning

Cited in

(1)

• Bialgebraic reasoning on higher-order program equivalence

This page was built for publication: Cerise: program verification on a capability machine in the presence of untrusted code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7031994)