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 的能力。