Save what must be saved: Secure context switching with Sailor

Save what must be saved: Secure context switching with Sailor

Speakers: Neelu S. Kalani, PhD Student, EPFL

Conference: USENIX Security

YouTube: https://www.youtube.com/watch?v=ERQ8ONmYjck

Overview

The talk "Save what must be saved: Secure context switching with Sailor," presented by Neelu S. Kalani from EPFL, addresses a fundamental yet persistently challenging problem in system security: ensuring the integrity and isolation of security domains during context switching. While a core concept taught in introductory operating systems courses, the practical implementation of secure context switches is fraught with difficulties, often leading to subtle yet critical vulnerabilities. Kalani and her team, including collaborators from IBM, highlight how the ever-increasing complexity of instruction set architectures (ISAs), with their hundreds or thousands of registers, makes it nearly impossible for human developers to correctly identify and swap all necessary architectural state.

This research introduces Sailor, a novel tool designed to automate the analysis of ISA specifications and systematically determine which architectural state must be saved and restored during a context switch. By leveraging machine-readable ISA specifications written in the Sail language and employing symbolic execution, Sailor identifies potential information leaks and integrity violations that arise from incomplete context switch implementations. The significance of this work lies in its ability to bring rigorous, automated verification to a traditionally manual and error-prone process, thereby enhancing the security posture of operating systems, hypervisors, and security monitors against sophisticated adversaries who might exploit these overlooked architectural details.

The talk not only details Sailor's methodology but also presents compelling evidence of its necessity by revealing critical bugs in widely used or formally verified systems, including the Linux kernel running on a RISC-V board, the Komodo security monitor, and the Keystone security monitor. These findings underscore that even well-regarded software can harbor context switching vulnerabilities, proving that the problem is far from solved. Sailor offers a proactive solution, providing developers with actionable insights to build more robust and secure systems in an era of rapidly evolving hardware.

Background

▶ Watch: Introduction to secure context switching and common bugs (0:00)

Context switching is a cornerstone of modern operating systems, enabling multiple processes or threads to share a single CPU core while maintaining isolation. At its core, a context switch involves privileged software (like the OS kernel or a hypervisor) saving the complete architectural state of the currently executing security domain (e.g., a process) and restoring the state of another. This process ensures that data from one domain does not inadvertently leak to another and that the execution of one domain does not improperly influence another. The state that needs to be swapped includes general-purpose registers, program counters, stack pointers, and various control registers.

The challenge, as highlighted by Neelu Kalani, stems from the exponential growth in the complexity of ISAs. Modern architectures like ARM, RISC-V, and x86 feature thousands of registers and intricate interaction rules defined across thousands of pages of documentation. Forgetting to swap even a single bit in one of these registers during a context switch can create a covert channel, leading to information leaks or integrity violations. This problem is exacerbated by the continuous introduction of new ISA extensions, which add further complexity and new state elements that might need to be managed.

Despite the critical importance of secure context switching, existing implementations, even in industry-standard and formally verified software, frequently contain bugs. This is often due to the manual and human-intensive process of interpreting vast, prose-style ISA manuals and then translating those specifications into correct code. Prior attempts at formal verification, while valuable, can become outdated if their underlying ISA specifications do not keep pace with hardware evolution, rendering their security proofs incomplete or invalid. The talk posits that a systematic, automated approach is essential to overcome this inherent human fallibility and the ever-present challenge of ISA complexity.

Key Findings

▶ Watch: Introducing Sailor: automated testing with machine-readable ISA specs (3:00)

The research presented in the talk directly challenges the assumption that context switching is a solved problem by uncovering significant vulnerabilities in real-world systems. Through the application of their Sailor tool, Neelu Kalani and her team identified several critical bugs:

1. Linux on StarFive VisionFive 2 Board: When analyzing the Linux kernel shipped with the StarFive VisionFive 2 board, Sailor discovered that performance counters were directly exposed to user-level processes. This exposure creates a potential timing channel vulnerability, where one user process could infer information about another by observing changes in these un-cleared counters across context switches. In contrast, upstream Linux typically exposes these counters only through the perf tool, which explicitly clears them to prevent such leaks. This finding highlights a deviation in a specific platform's Linux implementation that introduces a security flaw.

1. Komodo Security Monitor: Komodo, a security monitor known for its formally verified properties, was found to suffer from outdated ISA specifications. Its security proofs rely on self-written specifications that have not been kept current with the evolving ISA. Consequently, registers introduced with newer ISA states were not taken into account during context switching. This means that the formally proven security properties for Komodo do not hold true for systems implementing these newer ISA features, leaving them vulnerable to information leaks through unmanaged state.

1. Keystone Security Monitor: The Keystone security monitor exhibited similar issues, specifically leaking ISA extension state, such as floating-point or vector extension registers, across security domains. More critically, Keystone lacked proactive checks to discover if unsupported ISA extensions (e.g., vector extensions) were actually implemented by the underlying platform. Without these checks, an unprivileged adversary could easily leverage these unmanaged, unsupported extensions to leak sensitive information, as the monitor would not recognize or clear their state during a context switch.

These findings are not isolated incidents but rather illustrative examples of a systemic problem arising from the manual management of increasingly complex ISA specifications. The talk emphasizes that the goal was not to mount attacks, but to robustly demonstrate that incomplete context switching implementations create real-world security implications, including information leaks and potential integrity violations. Sailor's ability to automatically pinpoint these oversights underscores its value as a crucial tool for identifying and mitigating such vulnerabilities before they can be exploited.

Technical Deep Dive

▶ Watch: Algorithm to identify ISA state requiring context swap (6:00)

Sailor's core innovation lies in its systematic, automated approach to identifying all ISA state that must be properly handled during a context switch. This is achieved by leveraging machine-readable ISA specifications and symbolic execution.

The process begins with the Sail language, an open-source, high-level, and executable specification language used to formally describe the behavior of ISAs. Unlike traditional prose-style manuals, Sail specifications are precise and machine-interpretable. Sailor takes this Sail specification as its primary input.

The heart of Sailor's analysis is Isla, a symbolic execution engine specifically designed for Sail. Isla takes the Sail specification along with a specific instruction and a set of ISA constraints. Internally, Isla utilizes the Z3 SMT solver (Satisfiability Modulo Theories) to perform symbolic execution. This process explores all possible execution paths an instruction might take, considering different initial states and environmental conditions. For instance, for a common load instruction in RISC-V, Isla can generate as many as 264 distinct execution traces, each representing a unique interaction with the ISA state.

These execution traces are crucial because they capture every side effect an instruction might have on the architectural state, including flags set, exceptions generated, or registers modified. For example, a floating-point operation might set a specific flag to indicate an exception type. If this flag is not cleared or saved during a context switch, its value could leak information to the next security domain.

To illustrate, consider the control and status register (CSR) minstret in RISC-V, which denotes the number of instructions retired. When executed with supervisor mode privileges, Isla might generate two traces:

1. One trace where the instruction successfully reads the register, assuming minstret access is enabled for supervisor mode.
2. Another trace where the instruction traps (generates an exception) because access to the counter is not enabled for supervisor mode.

Both traces reveal interactions with minstret and potentially other related state.

The critical step is then to systematically identify which of these ISA states must be swapped. Sailor employs a sophisticated algorithm that looks for potential "channels" through which information can leak or integrity can be compromised. A simple heuristic is applied: if one security domain has the capability to write to a particular register (or affect its value), and another security domain has the capability to read from that register (or its computation depends on its value), then that register must be swapped during a context switch between these two domains.

This algorithm is repeated for each ISA state per privilege mode pair. For example, if both the source and target security domains are executing in user mode, Sailor analyzes the interactions. A concrete example is the Floating Point Rounding Mode (FRM) register. If a user-mode source domain can write to FRM, and the floating-point operations performed by a user-mode target domain depend on the value of FRM, then not swapping this register would directly affect the computational integrity of the target domain. Therefore, Sailor marks FRM to be swapped for user-to-user context switches.

The entire process involves:

1. Generating traces from Isla. For a general-purpose RISC-V CPU, this can amount to 3 GB of traces, taking approximately 20 hours for symbolic execution. This is a one-time cost per Sail model update.
2. Parsing these traces to extract all relevant information about register access and dependencies.
3. Feeding this structured information into Sailor's algorithm, which then rapidly (in less than 10 seconds) produces a comprehensive list of all ISA states that must be swapped, as well as those that are not security-sensitive in a given context.

The output of Sailor is a precise, machine-generated guide for developers, indicating exactly what architectural state needs to be managed during context switching for different privilege transitions. This rigorous, automated analysis significantly reduces the risk of human error and provides a foundational basis for building truly secure context switch implementations.

Demo / Proof of Concept

▶ Watch: Sailor's workflow, performance, and one-time cost (8:00)

While the talk did not feature a live, interactive demonstration of Sailor's execution or a proof-of-concept exploit, the speakers presented concrete findings from applying their tool to real-world systems. Instead of a "demo" in the traditional sense, the talk highlighted the results of Sailor's analytical capabilities, effectively serving as a validation of its utility and accuracy.

The application of Sailor yielded specific, actionable insights into the security posture of three distinct systems:

1. StarFive VisionFive 2 Linux: Sailor's analysis revealed that performance counters were directly accessible to user programs in the Linux distribution for this RISC-V board. This finding was presented as a direct result of Sailor's automated checks, indicating that the tool identified state (performance counters) that was not being properly isolated or cleared across user process context switches, thus creating a potential information leak.
2. Komodo Security Monitor: The research demonstrated how Sailor could identify vulnerabilities stemming from outdated ISA specifications. Komodo, despite its formal verification claims, failed to account for newer ISA registers, a deficiency that Sailor automatically detected by comparing the monitor's assumed state management against the comprehensive, up-to-date Sail specification.
3. Keystone Security Monitor: For Keystone, Sailor highlighted the critical flaw of leaking ISA extension state (e.g., floating-point or vector registers) and the absence of proactive checks for unsupported extensions. The tool's output would indicate these specific registers as requiring context switching, and the absence of such handling in Keystone confirmed the vulnerability.

The presentation clarified that the primary goal of the research and the tool is not to facilitate attacks, but rather to "enable identify all such state and then actually correctly swap them during the context switching." The methodology for using Sailor's output was described as straightforward: once the algorithm identifies the necessary state, developers can use simple utilities like grep or code scanning tools to verify if their existing context switch implementations correctly handle these identified registers. Furthermore, Sailor can automatically generate tests to confirm compliance.

The "proof of concept" in this context is the successful identification of previously unknown or unaddressed context switching vulnerabilities in prominent systems, demonstrating Sailor's effectiveness in revealing subtle architectural state management flaws that human developers often miss.

Defensive Implications

▶ Watch: Key findings from analyzing Vision 52, Komodo, Keystone (10:00)

Sailor offers profound defensive implications for anyone involved in the design, implementation, or maintenance of secure systems, particularly those operating at low levels of the software stack.

1. For OS, Hypervisor, and Security Monitor Developers: The primary defense is to integrate Sailor's output directly into the development and verification workflows. Developers should use the comprehensive list of security-sensitive ISA states generated by Sailor to audit their existing context switch implementations. This includes verifying that all identified registers, including those related to performance counters, floating-point units, and other ISA extensions, are correctly saved, restored, or cleared during every type of privilege mode transition. The tool's ability to generate specific tests based on its findings provides an automated means to validate these implementations.

1. For ISA Designers and Hardware Architects: Sailor's insights can guide the design of new ISA extensions. When introducing new architectural state, designers should use Sailor to ensure that these additions do not inadvertently create new security vulnerabilities, especially concerning backward compatibility. Specifically, newly introduced ISA state should not become security-sensitive when the extension is disabled, and previously classified non-security-sensitive state should not gain security relevance with the new extension. This proactive analysis can prevent the introduction of new classes of context switching bugs at the architectural level.

1. Continuous Integration and Deployment (CI/CD): A crucial defensive strategy is to integrate Sailor into the CI/CD pipeline of existing systems. Given that ISAs are continuously evolving, context switch implementations must also evolve. By running Sailor regularly (e.g., daily or weekly) against updated Sail specifications, developers can dynamically update their context switch code with the latest insights. This ensures that as new hardware features or ISA versions emerge, the system's context switching remains secure and robust against newly exposed architectural state.

1. Mitigating Timing and Information Leak Channels: The bugs found in systems like the VisionFive 2 Linux highlight the importance of carefully managing seemingly innocuous state like performance counters. Defenders must be vigilant about any architectural state that can be written by one security domain and read by another, as these constitute potential information leak channels. Sailor specifically identifies such channels, enabling developers to either properly isolate or clear these registers.

1. Beyond Formal Verification: While formal verification is valuable, the Komodo example shows its limitations when based on outdated specifications. Defenders should not solely rely on proofs derived from self-written or static ISA models. Sailor provides an independent, automated, and up-to-date analysis that can complement formal methods, ensuring that proofs remain valid as the underlying hardware specifications evolve.

In essence, Sailor provides a systematic and automated safeguard against a class of vulnerabilities that are notoriously difficult for humans to identify. By adopting Sailor's methodology, organizations can significantly enhance the isolation guarantees of their systems, reducing the attack surface for sophisticated adversaries targeting architectural state.

Key Takeaways

• Context switching remains a critical, bug-prone security surface: Despite being a fundamental OS concept, the increasing complexity of ISAs makes correct and secure context switching extremely challenging, leading to persistent vulnerabilities.
• Sailor automates the identification of security-sensitive ISA state: The tool systematically analyzes machine-readable Sail language specifications using the Isla symbolic execution engine to identify precisely which architectural state must be saved, restored, or cleared during context switches.
• Real-world bugs highlight the prevalence of context switching flaws: Sailor uncovered critical vulnerabilities in the Linux kernel (StarFive VisionFive 2), Komodo, and Keystone security monitors, demonstrating that even widely used or formally verified systems are susceptible to information leaks and integrity violations due to incomplete context switching.
• Systematic methodology prevents information leaks and integrity violations: By identifying write/read dependencies between security domains for various registers (e.g., Floating Point Rounding Mode (FRM), performance counters), Sailor provides a robust mechanism to prevent unauthorized information flow and ensure computational integrity across security domain transitions.
• Sailor's output guides secure development and ISA design: The tool's findings are invaluable for auditing existing context switch code, automatically generating verification tests, and informing the design of new ISA extensions to prevent the introduction of future vulnerabilities.
• Continuous integration is essential for evolving ISAs: Integrating Sailor into CI/CD pipelines allows systems to dynamically adapt their context switch implementations as ISA specifications evolve, ensuring ongoing security and robustness against new hardware features.

About the Speaker(s)

The primary speaker for this talk was Neelu S. Kalani, who is a PhD student at EPFL (École Polytechnique Fédérale de Lausanne). Her research focuses on critical aspects of system security, particularly addressing the challenges posed by complex hardware-software interactions.

Neelu Kalani's work on Sailor is a collaborative effort, undertaken with her co-advisor Dumar Bja from EPFL, and Gurnie Hunt and Mojik Usa from IBM. This collaboration brings together academic rigor from EPFL with industry expertise from IBM, highlighting the practical relevance and impact of their research in addressing real-world security challenges in modern computing systems.