Sockeye: Bug-finding and proofs for platform configurations and hardware based on reference manuals

arXiv:2510.27485 · cs.CR, cs.OS, cs.PL · Submitted 2025-10-31 · Read on arXiv

cs.CR, cs.OS, cs.PL

Submitted: 2025-10-31

Updated: 2026-09-15

Comments: To be published in proceedings of SOSP'26

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

Core — 23× in this paper · explained in 2 episodes
Trace — 5× in this paper · explained in 2 episodes
Address Space Controller — 4× in this paper
Actor — 2× in this paper · explained in 3 episodes
Formal Methods — 2× in this paper · explained in 3 episodes
System Management Mode — 2× in this paper
Abstraction — 1× in this paper · explained in 1 episode
Adam — 1× in this paper · explained in 2 episodes
Address Protection — 1× in this paper
Direct Memory Access — 1× in this paper
Initial Data — 1× in this paper · explained in 2 episodes
SMT solver — 1× in this paper · explained in 2 episodes
System Memory Management Unit — 1× in this paper

Related papers