Axiomatic Hardware-Sofware Contracts for Security

Abstract

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 formalizing LCMs, derived from the established axiomatic vocabulary for formalizing 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 and provide a taxonomy for classifying said leakage by severity. To illustrate the efcacy of LCMs, we frst demonstrate that our leakage defnition 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 identifes Spectre vulnerabilities in programs and scales to analyze real-world crypto-libraries.