Cerise

About

The Cerise project is a family of program logics and logical relations for reasoning on programs running on capability machine, including programs that interact with unknown or potentially malicious code. Cerise implements a capability machine architectures inspired from CHERI, in which the CPU enables fine-grained memory safety and privilege separation through the use of hardware capabilities. The program logics and logical relations of the Cerise family are formalised and mechanised in the Rocq Prover, using the Iris separation logic framework.

Resources

Formalization

Browse the Cerise source and its mechanized proofs.

GitHub repository Open documentation

Exercises

Exercises to learn Cerise.

Exercise sheet
Rocq implementation

Interpreter

Run Cerise examples directly in your browser.

Open the interpreter

Publications

Overview of the published papers, PhD thesis and workshop presentations based on the Cerise framework.

Other Material

Other unpublished material.

Main research groups involved

PLS Group

Department of Computer Science, Aarhus University.

Contact: Lars Birkedal

DistriNet

Department of Computer Science, KU Leuven.

Contact: Dominique Devriese

Grants

The Cerise project has been supported in part by the following grants:

VILLUM Foundation, Villum Investigator grant no. 25804, including the Center for Basic Research in Program Verification (CPV)
Danish Council for Independent Research for the Natural Sciences (DFF/FNU), project 6108-00363
Research Foundation – Flanders (FWO)
Air Force Office of Scientific Research, award FA9550-21-1-0054
Research Fund KU Leuven
Flemish Research Programme Cybersecurity
The European Research Council (UniversalContracts Starting Grant)