Sockeye: Bug-finding and proofs for platform configurations and hardware based on reference manuals
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 are the first to address this problem for closed-source hardware platforms, by introducing a domain-specific language to formally describe hardware semantics based on hardware reference manuals, assumptions about software behavior, and desired security properties. We demonstrate the practicality of our approach by creating machine-readable specifications for a diverse set of eight platforms from their reference manuals, and formally proving 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.