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.

翻译：硬件平台日益增长的复杂性给系统程序员带来了挑战。正确地对众多组件进行编程，同时提供功能性和安全性十分困难：各个单元的语义以文本形式描述、说明不足，且容易产生不准确性。关于平台安全性的严谨声明往往无法实现。我们提出了一种领域特定语言，用于描述硬件语义、软件行为假设以及所需的安全属性。随后，我们根据八个不同平台的参考手册创建了机器可读的规范，并正式证明了其（不）安全性。除了关于内存机密性和完整性的安全证明外，我们还发现了若干文档错误。最后，我们的分析还揭示了一个真实服务器芯片上的漏洞，该漏洞经供应商确认适用于广泛部署的网络设备家族。我们的工具为系统集成商提供了一种方式，用以正式描述整个平台的安全属性，并提供了寻找反例或证明其正确性的手段。