Enter, Exit, Page Fault, Leak: Testing Isolation Boundaries for Microarchitectural Leaks

TL;DR

This paper introduces a novel testing tool that systematically probes microarchitectural isolation boundaries in CPUs, revealing new security leaks and validating a proactive approach to hardware security verification.

Contribution

It extends model-based relational testing to detect microarchitectural leaks across security domains, providing a systematic and proactive testing methodology.

Findings

Discovered four new microarchitectural leaks in six x86-64 CPUs.

Validated the effectiveness of the testing tool with only two false positives.

Confirmed known leaks, demonstrating the tool's reliability.

Abstract

CPUs provide isolation mechanisms like virtualization and privilege levels to protect software. Yet these focus on architectural isolation while typically overlooking microarchitectural side channels, exemplified by Meltdown and Foreshadow. Software must therefore supplement architectural defenses with ad-hoc microarchitectural patches, which are constantly evolving as new attacks emerge and defenses are proposed. Such reactive approach makes ensuring complete isolation a daunting task, and leaves room for errors and oversights. We address this problem by developing a tool that stress tests microarchitectural isolation between security domains such as virtual machines, kernel, and processes, with the goal of detecting flaws in the isolation boundaries. The tool extends model-based relational testing (MRT) methodology to enable detection of cross-domain information leakage. We design a new test case generator and execution sandbox to handle multi-domain execution, new leakage models to encode expected leaks, and new analysis techniques to manage nondeterminism. We use this tool to perform an in-depth testing campaign on six x86-64 CPUs for leakage across different isolation boundaries. The testing campaign exposed four new leaks and corroborated numerous known ones, with only two false positives throughout the entire campaign. These results show critical gaps in current isolation mechanisms as well as validate a robust methodology for detecting microarchitectural flaws. As such, this approach enables a shift from reactive patching to proactive security validation in processor design.