Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

2 Citations (Scopus)

Abstract

A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities, machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. We use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant. The methodology we present underlies recent work of the authors on formal reasoning about capability machines [15, 33, 37], but was left somewhat implicit in those publications. In this paper we present a pedagogical introduction to the methodology, in a simpler setting (no exotic capabilities), and starting from minimal examples. We work our way up to new results about a heap-based calling convention and implementations of sophisticated object-capability patterns of the kind previously studied for high-level languages with object-capabilities, demonstrating that the methodology scales to such reasoning.
Original languageEnglish
Article number3
JournalJournal of the ACM
Volume71
Issue1
Number of pages59
ISSN0004-5411
DOIs
Publication statusPublished - 12 Feb 2024

Keywords

  • universal contracts
  • capability machines
  • program logic
  • capability safety
  • separation logic
  • CHERI
  • Separation logic
  • Capability safety
  • Program logic
  • Universal contracts
  • Capability machines

Fingerprint

Dive into the research topics of 'Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code'. Together they form a unique fingerprint.

Cite this