Save what must be saved: Secure context switching with Sailor
Neelu S. Kalani
34th USENIX Security Symposium (USENIX Security '25) · Day 3 · System Security 4: Kernel and Low-Level System Security
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.
AI review
Sailor is legitimate systems security research: a symbolic-execution-based tool that automatically derives which architectural state must be swapped during context switches, backed by Sail/Isla/Z3, and validated against three real targets — including a formally verified monitor. The bugs found in Komodo and Keystone are genuinely embarrassing for those projects and make the "formally verified" claim worth unpacking in front of an audience. USENIX-caliber work.