一句话：在 Morello ISA 全规模模型上机器化证明任意不可信代码存在时软件组件的强安全封装性质。
评估新架构安全机制是否真正提供预期保护十分困难，尤其面对任意未知代码时，测试难以给出保证，而生产级 ISA 的规模又使机器化证明长期不可行。本文聚焦 CHERI/Morello 能力式安全封装，在 Morello ISA 的全规模顺序模型之上，结合并扩展三项工作：Cerise 针对理想化 capability machine 的 Iris 逻辑关系封装性证明、Islaris 对生产级 ISA 中已知代码的推理方法，以及此前仅覆盖到 domain crossing 的 T-CHERI 任意 Morello 代码安全性质。作者对运行于 Morello 的封装代码示例证明了强安全封装性质，该性质在任意不可信代码存在下仍成立，表明可为全规模工业架构的安全机制建立强机器化保证。
When designing new architectural security mechanisms, a key question is whether they actually provide the intended security, but this has historically been very hard to assess. One cannot gain much confidence by testing, as such mechanisms should provide protection in the presence of arbitrary unknown code. Previously, one also could not gain confidence by mechanised proof, as the scale of production instruction-set architecture (ISA) designs, many tens or hundreds of thousands of lines of specification, made that prohibitive. We focus in this paper especially on the secure encapsulation of software components, as supported by CHERI architectures in general and by the Arm Morello prototype architecture and hardware design in particular. Secure encapsulation is an essential security mechanism, for fault isolation and to constrain untrusted third-party code. It has previously often been implemented using virtual memory, but that does not scale to large numbers of compartments. Morello provides capability-based mechanisms that do scale, within a single address space. We prove a strong secure encapsulation property for an example of encapsulated code running on Morello, that holds in the presence of arbitrary untrusted code, above a full-scale sequential model of the Morello ISA. To do so, we build on, extend, and unify three orthogonal lines of previous work: the Cerise proof of such an encapsulation property for a highly idealised capability machine, expressed using a logical relation in Iris; the Islaris approach for reasoning about known code in production-scale ISAs; and the T-CHERI security properties of arbitrary Morello code, previously proved only for executions up to domain crossing. This demonstrates how one can prove such strong properties of security mechanisms for full-scale industry architectures.
@article{paperbot3085,
title = {Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture},
author = {Angus Hammond and Ricardo Almeida and Thomas Bauereiss and Brian Campbell and Ian Stark and Peter Sewell},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729329}
}