CHERI와 같은 Capability 기반 아키텍처는 소프트웨어 컴포넌트의 아키텍처적 격리(isolation)에 강력한 지원을 제공합니다. 추가적으로 마이크로아키텍처 누출(leakage)으로부터 보호하기 위해, 소프트웨어는 상수 시간 방식(constant-time fashion)으로 작성될 수 있습니다. 하지만 현대 프로세서는 추측 실행(speculative execution)에 크게 의존하며, 이는 상수 시간 보장(constant-time guarantees)을 무효화하고 격리된 비밀 정보(isolated secrets)를 일시적으로 누출시킬 수 있습니다. 본 논문에서는 CHERI에 대한 안전한 추측(secure speculation) 제공이 간단하지 않으며, 기존 제안들이 기밀성 보장(confidentiality guarantees)을 유지하는 데 실패함을 보여줍니다. 우리는 Capability 안전성, 추측 실행, 그리고 정보 흐름 보안(information-flow security)에 대해 공동으로 추론하기 위한 형식적 프레임워크를 개발하고, 이를 사용하여 잠재적인 누출을 입증합니다. 이후 이러한 프레임워크 내에서 새로운 프로세서 설계인 SCHERI를 제시하고, 이것이 상수 시간 정책에 대한 종단 간(end-to-end) 안전한 추측 보장을 제공함을 형식적으로 증명합니다. 우리의 결과는 Spectre 공격에 강건한(resilient) 미래 Capability 기반 프로세서를 구축하기 위한 형식적 토대와 실질적인 지침을 제공합니다.