Secure context switching:
Leverages machine-readable ISA specifications written in Sail

Sailor

Automating the search for ISA state that privileged software must save, restore, and protect across context switches.

USENIX Security '25 paper Slides Talk

Usenix Security 2025 Publication

A collaboration between EPFL and IBM Research.

Artifacts Available Artifacts Functional Results Reproduced

Save what must be saved: Secure context switching with Sailor

Published at the 34th USENIX Security Symposium, Sailor shows how machine-readable Sail ISA specifications and Isla symbolic execution can expose security-sensitive architectural state that context-switch code must handle correctly.

Read the paper

Guarantees

Context switching with less manual inspection and guesswork

Systematic ISA spec inspection

Tracks registers and other ISA state affected by instructions, instead of relying on scattered prose.

Leverage symbolic execution

Uses executable ISA models and symbolic execution to collect the state dependencies context switches care about.

Found bugs in existing code

Assesses real systems, including Linux and confidential-computing monitors, for mishandled ISA state.

The Problem

Implementing context switching correctly should not be difficult in 2025.

Modern ISAs have hundreds of registers and instructions whose effects vary by execution. A missing save or restore step can let state leak across processes, privilege domains, or enclaves.

Our Approach

Sailor automatically identifies what context must be swapped.

Sailor analyzes machine-readable Sail ISA specifications with Isla, then identifies the architectural state that context-switch implementations must preserve to avoid subtle security failures.