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)

zbMATH Keywords

separation logicprogram logiccapability machinescapability safetyCHERIuniversal contracts

Mathematics Subject Classification ID

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

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)