{"ID":2847621,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.27485","arxiv_id":"2510.27485","title":"Sockeye: a language for analyzing hardware documentation","abstract":"The ever increasing complexity of hardware platforms poses a challenge to systems programmers. Correctly programming a multitude of components, providing functionality and security, is difficult: semantics of individual units are described in prose, underspecified, and prone to inaccuracies. Rigorous statements about platform security are often impossible. We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties. We then create machine-readable specifications for a diverse set of eight platforms from their reference manuals, and formally prove their (in-)security. In addition to security proofs about memory confidentiality and integrity, we discover a handful of documentation errors. Finally, our analysis also revealed a vulnerability on a real-world server chip, which was confirmed by the vendor to apply to a wide family of deployed network appliances. Our tooling offers system integrators a way of formally describing security properties for whole platforms, and the means to find counterexamples, or proving them correct.","short_abstract":"The ever increasing complexity of hardware platforms poses a challenge to systems programmers. Correctly programming a multitude of components, providing functionality and security, is difficult: semantics of individual units are described in prose, underspecified, and prone to inaccuracies. Rigorous statements about p...","url_abs":"https://arxiv.org/abs/2510.27485","url_pdf":"https://arxiv.org/pdf/2510.27485v2","authors":"[\"Ben Fiedler\",\"Samuel Gruetter\",\"Timothy Roscoe\"]","published":"2025-10-31T14:04:01Z","proceeding":"cs.CR","tasks":"[\"cs.CR\",\"cs.OS\",\"cs.PL\"]","methods":"[]","has_code":false}