Relational Models of Microarchitectures for Formal Security Analyses

• DOI: 10.48550/arxiv.2112.10511
• Publication Date: 2021-01-01
• Authors: Nicholas Mosier; Hanna Lachnitt; Hamed Nemati; Caroline Trippel
• Keywords: Microarchitecture

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