Sockeye: a language for analyzing hardware documentation
Ben Fiedler, Samuel Gruetter, Timothy Roscoe
TL;DR
Sockeye addresses the problem of underspecified hardware documentation by providing a formal DSL to describe hardware semantics, software assumptions, and security properties. It translates specifications into machine-checkable forms and uses multiple backends (SMT, Rosette, CBMC) to prove properties or generate counterexamples, demonstrated across eight real-world SoCs. The work uncovers documentation ambiguities, reproduces known hardware bugs, and even identifies a previously unknown vulnerability, illustrating both the utility and limitations of formalizing hardware manuals for system integration. This approach offers a path toward rigorous, automated verification of SoC security properties and a framework for distinguishing hardware bugs, documentation errors, and insecure configurations.
Abstract
Systems programmers have to consolidate the ever growing hardware mess present on modern System-on-Chips (SoCs). Correctly programming a multitude of components, providing functionality but also security, is a difficult problem: semantics of individual units are described in English prose, descriptions are often 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 SoCs 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. Our tooling offers system integrators a way of formally describing security properties for entire SoCs, and means to prove them or find counterexamples to them.