Save what must be saved: Secure context switching with Sailor

Instruction set architectures (ISAs) are complex, with hundreds of registers and instructions that can modify dozens of them during execution, variably on each instance. Prose-style ISA specifications struggle to capture these intricacies of the ISAs, where often the important details about a single register are spread out across hundreds of pages of documentation. Ensuring that all ISA-state is swapped in context switch implementations of privileged software requires meticulous examination of these pages. This manual process is tedious and error-prone. We propose a tool called Sailor that leverages machine-readable ISA specifications written in Sail and Isla symbolic execution engine for Sail to automate this task. Sailor determines the ISA-state that must be swapped during the context switch using the data collected from Isla and a novel algorithm to identify all the ISA-state that must be swapped during context switches. We use Sailor to assess the context switch code of multiple systems: from regular user process context switching code in the RISC-V Linux kernel on the StarFive VisionFive2 board, to the enclave context switching code in confidential computing frameworks, Keystone and Komodo. We identify multiple mishandled security-sensitive ISA-state. This research exposes an often overlooked attack surface that stems from mishandled ISA-state, enabling unprivileged adversaries to exploit system vulnerabilities.