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.

翻译：可信计算的核心特性之一是认证，它允许封装组件（飞地）向（本地或远程）不信任组件证明自身身份。对使用该技术的软件进行推理时，需追踪成功认证后信任关系的演化过程。此过程具有安全关键性且非平凡，但现有形式化验证技术均未支持对飞地及其客户端的认证行为进行模块化推理，亦无法证明融合可信、不可信与已认证代码系统的端到端属性。我们提出Cerisier，这是首个支持对可信、不可信及已认证代码进行模块化推理的程序逻辑，并在Iris分离逻辑及Rocq证明器中实现完全机械化。我们形式化描述了近期提出的CHERI-TrEE方案（该方案通过扩展飞地原语增强能力机），将其作为Cerise能力机及其程序逻辑的扩展。我们的程序逻辑为不可信代码定义了通用契约，该契约既涵盖能力安全性，也包含局部飞地认证。与Cerise类似，该通用契约通过定义能力权限的逻辑关系进行表达。我们通过证明可信计算中三个典型应用（安全外包计算、互认证及建模可信传感器组件）的端到端属性，展示了Cerisier的效能。