一句话：首个面向可信、不可信与已认证代码的模块化程序逻辑，支持能力机器中 enclave 证明的端到端验证。
可信计算中的 attestation 使封装组件（enclave）能向本地或远程不信任组件证明身份，但验证使用该技术的软件需跟踪信任如何在证明后演化，现有形式化验证技术无法模块化推理 enclave 及其客户端，也难以证明混合可信、不可信与已证明代码的系统端到端性质。本文提出 Cerisier，首个用于模块化推理可信、不可信与已证明代码的程序逻辑，并在 Iris 分离逻辑与 Rocq 证明助手中完全机器化。作者将 CHERI-TrEE 的 enclave 原语形式化为 Cerise 能力机器与程序逻辑的扩展，并为不可信代码提供统一契约，同时刻画能力安全性与本地 enclave attestation；该契约基于定义能力权限的逻辑关系。最后通过安全外包计算、双向 attestation 和可信传感器组件三个应用证明端到端性质。
A key feature in trusted computing is attestation, which allows encapsulated components (enclaves) to prove their identity to (local or remote) distrusting components. Reasoning about software that uses the technique requires tracking how trust evolves after successful attestation. This process is security-critical and non-trivial, but no existing formal verification technique supports modular reasoning about attestation of enclaves and their clients, or proving end-to-end properties for systems combining trusted, untrusted and attested code. We contribute Cerisier, the first program logic for modular reasoning about trusted, untrusted and attested code, fully mechanized in the Iris separation logic and the Rocq Prover. We formalize a recent proposal, CHERI-TrEE, to extend capability machines with enclave primitives, as an extension to the Cerise capability machine and program logic. Our program logic comes with a universal contract for untrusted code, which captures both capability safety and local enclave attestation. Like Cerise, this universal contract is phrased in terms of a logical relation defining capabilities' authority. We demonstrate Cerisier by proving end-to-end properties for three representative applications of trusted computing: secure outsourced computation, mutual attestation and a modeled trusted sensor component.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2604-13638,
title = {Cerisier: A Program Logic for Attestation in a Capability Machine},
author = {June Rousseau and Denis Carnier and Thomas Van Strydonck and Steven Keuchel and Dominique Devriese and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808287}
}