Save what must be saved: Secure context switching with Sailor
summary
Sailor uses the machine‑readable Sail ISA and the Isla symbolic executor to generate instruction traces (about 3 GB traces, 20 hours symbolic execution) and an algorithm that outputs exactly which registers must be saved per privilege pair. It flags concrete bugs: VisionFive2 Linux exposes performance counters across processes, Komodo’s handwritten spec misses newer registers, Keystone fails to disable or save floating‑point and vector state. The tool auto‑generates tests, parses traces in under 10 seconds, and can feed results into CI or verification.
AI-written summary · about
chapters (11)
- 0:00Sailor and context switching
- 0:33Context switching fundamentals
- 1:14Bugs in context switch implementations
- 3:20Sailor’s ISA state analysis
- 4:27ISA state that must be swapped
- 7:18Algorithm for secure state
- 8:24Execution traces processing
- 9:27Testing context switch security
- 10:11Beyond verification and testing
- 10:55Case studies: Vision 52, Komodo, Keystone
- 12:19Future work and conclusion
related talks
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
20mSail RISC-V: Status and Future Challenges
16mTooling Design and Lessons Learned from Systematic Evaluations of the Preservation of(…)
19mCoSMIX: A Compiler-based System for Secure Memory Instrumentation and Execution in Enclaves
51mTutorial: Performance Tools
23mBeating the Benchmarks: Co-evolving the ISA and Development Tools
16mMitigating Transient-Execution Attacks with CHERI Compartments
27mMitigating speculative execution attacks with ASI - follow up