本文提出 Griotte 和 Griotte OS，这是对 CHERIoT 硬件能力机器与 CHERIoT RTOS 的抽象化但忠实的建模，旨在为 CHERIoT 的分区隔离（compartmentalisation）安全保证提供形式化验证基础。CHERIoT 是一种软硬件协同设计，通过硬件能力（capabilities）定义“分区”这一概念，操作系统默认隔离各分区以限制漏洞或恶意行为造成的损害。跨分区通信依赖一个特权组件——切换器（switcher），该组件提供跨分区调用接口，同时强制分区隔离并保证栈安全。由于 CHERIoT 的安全属性依赖于能力机器与切换器的互补作用，需回答两个关键问题：其一，如何形式化地描述 CHERIoT 分区所提供隔离的具体安全含义；其二，该设计是否确实强制实施所期望的安全属性。为此，作者用基于续延的逻辑关系（continuation-based logical relation）形式化地刻画出切换器与能力机器组合行为所应满足的安全保证，并为 Griotte 的切换器定义了符合这些保证的规范，进而以证明其实现满足该规范。作者在一系列关键场景上验证了 Griotte 的有效性，这些场景涵盖 CHERIoT 的不同方面，包括在内存与未知代码共享时本地状态的完整性。该方法具有模块化特点：可分别验证每个分区，再组合其规范。整体上，该工作为 CHERIoT 设计提供了坚实的形式化基础。适合安全架构师、系统形式化验证研究者以及关注硬件/OS 隔离机制的蓝队人员阅读。