Griotte: Verified Compartmentalisation via Capabilities

本文提出 Griotte 和 Griotte OS，这是对 CHERIoT 硬件能力机器与 CHERIoT RTOS 的抽象化但忠实的建模，旨在为 CHERIoT 的分区隔离（compartmentalisation）安全保证提供形式化验证

历史摘要 · 未重新核验 · arXiv cs.CR