Relational Models of Microarchitectures for Formal Security Analyses
This addresses the need for formal security analyses in hardware-software systems, particularly for detecting microarchitectural leakage, but it is incremental as it builds on existing axiomatic vocabularies from memory consistency models.
The paper tackles the problem of defining hardware-software security contracts that account for microarchitecture-level details to detect hardware leakage, proposing leakage containment models (LCMs) and demonstrating their efficacy by capturing known attacks and automatically identifying Spectre vulnerabilities in realistic codebases like libsodium.
There is a growing need for hardware-software contracts which precisely define the implications of microarchitecture on software security-i.e., security contracts. It is our view that such contracts should explicitly account for microarchitecture-level implementation details that underpin hardware leakage, thereby establishing a direct correspondence between a contract and the microarchitecture it represents. At the same time, these contracts should remain as abstract as possible so as to support efficient formal analyses. With these goals in mind, we propose leakage containment models (LCMs)-novel axiomatic security contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our core contribution is an axiomatic vocabulary for formally defining LCMs, derived from the established axiomatic vocabulary used to formalize processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage-focusing on leakage through hardware memory systems-so that it can be automatically detected in programs. To illustrate the efficacy of LCMs, we present two case studies. First, we demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Second, we develop a static analysis tool based on LCMs which automatically identifies Spectre vulnerabilities in programs and scales to analyze realistic-sized codebases, like libsodium.