Lune

USENIX Security2025

Save what must be saved: Secure context switching with Sailor

Neelu S. Kalani, Thomas Bourgeat, Guerney D. H. Hunt, Wojciech Ozga

2025Year

Abstract

We introduce a tool called Sailor that automatically identifies ISA-state that must be swapped across context switches to prevent information leaks or computational integrity breaches. Sailor parses traces generated from an existing tool, Isla, a symbolic execution engine for ISA specifications written in the domain-specific language, Sail. We demonstrate Sailor for the RISC-V architecture. In this work, we extend Isla to automatically generate traces for multiple instructions, in the same format as provided by the RISC-V specification manuals. Based on the identified ISA-state, we automatically generate tests to check if the context switch implementations on existing systems swaps the state correctly or not. The associated artifacts include: 1. The patch to Isla for generating traces for all instructions in a general-purpose RISC-V processor (rv64gc). 2. The python scripts to compute the ISA-state relevant for context switching. This includes parsing of the Isla traces (ISA-Inspector) and the classifier algorithm (Analyzer), as shown in Figure 3 of the paper. 3. The automatic test generator (also shown in Figure 3 ) that generates tests to provide experimental evaluation of existing systems.