  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.
