Sockeye: a language for analyzing hardware documentation
Ben Fiedler, Samuel Gruetter, Timothy Roscoe

TL;DR
Sockeye introduces a domain-specific language for formal hardware documentation analysis, enabling security proofs, error detection, and vulnerability discovery across multiple hardware platforms.
Contribution
It provides a novel language and tooling for formal security analysis of hardware documentation, with proofs and real-world vulnerability findings.
Findings
Formal security proofs for memory confidentiality and integrity.
Discovered documentation errors in hardware references.
Identified a vulnerability on a real-world server chip.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
