发表机构
Aarhus University; Jane Street; MPI-SWS（奥胡斯大学; 简街; 德国马克斯·普朗克软件系统研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出Griotte及Griotte OS，形式化验证CHERIoT隔离区模型的安全属性，为CHERIoT设计提供了坚实的形式化基础。
AI 中文摘要
CHERIoT是一种新型软硬件协同设计，它利用硬件能力在极简的基于能力的操作系统CHERIoT RTOS中定义了隔离区（compartment）的概念。默认情况下，隔离区相互隔离，以在出现错误或恶意行为时限制损害范围。为了实现跨隔离区通信，该操作系统提供了一个名为switcher的特权组件，它为跨隔离区调用提供接口，同时强制隔离区之间的隔离并保证栈安全。结合硬件能力，switcher对于强制CHERIoT隔离区模型的安全保障至关重要。CHERIoT的设计引发了两个问题：第一，如何形式化CHERIoT隔离区旨在提供的非形式化隔离概念？第二，鉴于CHERIoT的安全属性依赖于能力机和switcher的互补作用，CHERIoT的设计是否强制实现了预期的安全属性？在本文中，我们引入了Griotte和Griotte OS，它们是CHERIoT机器和CHERIoT RTOS的理想化但忠实的版本，我们使用它们来回答上述两个问题：第一，我们以基于延续的逻辑关系的形式正式捕获了上述安全保障，该逻辑关系捕获了switcher和能力机的组合行为；第二，我们为Griotte switcher定义了一个规范，该规范强制实现这些保障，并证明实现符合该规范。我们在一系列关键场景中演示了Griotte，这些场景展示了CHERIoT的不同方面，包括在存在与未知代码共享内存时的本地状态完整性。我们的方法是模块化的：我们单独验证隔离区，然后组合它们的规范。我们的贡献共同为CHERIoT的设计提供了坚实的形式化基础。
英文摘要
CHERIoT is a novel hardware-software co-design that leverages hardware capabilities to define a notion of compartment, in a minimalistic capability-based OS, CHERIoT RTOS. By default, compartments are isolated to limit damage in case of bugs or malicious behaviour. To allow cross-compartment communication, the OS provides a privileged component, called the switcher. The switcher provides an interface for cross-compartment calls, while enforcing isolation between compartments and guaranteeing stack safety. Together with hardware capabilities, the switcher is critical to enforce the security guarantees of the CHERIoT compartment model. The design of CHERIoT raises two questions: First, how can one formalise the informal notion of compartmentalisation that CHERIoT compartments are designed to provide? And second, given that the safety properties of CHERIoT hinge on the complementary roles of the capability machine and of the switcher, does the design of CHERIoT enforce the desired security properties? In this paper, we introduce Griotte and Griotte OS, idealised but faithful versions of the CHERIoT machine and the CHERIoT RTOS, which we use to answer these two questions: First, we formally capture the aforementioned security guarantees in the form of a continuation-based logical relation which captures the combined behaviour of the switcher and of the capability machine. And second, we define a specification for the Griotte switcher that enforces those guarantees, and prove that the implementation meets the specification. We demonstrate Griotte on a range of key scenarios illustrating different aspects of CHERIoT, including integrity of the local state in the presence of memory sharing with unknown code. Our approach is modular: we verify compartments individually, and then compose their specifications. Together, our contributions give a solid formal foundation to the design of CHERIoT.
