(2022) Axiomatic hardware-software contracts for security.
|
Text
lcms_ISCA22_cameraready.pdf Download (856kB) | Preview |
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 efficacy of LCMs, we first 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 real-world crypto-libraries.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Conference: | ISCA ACM International Symposium on Computer Architecture |
| Depositing User: | Hamed Nemati |
| Date Deposited: | 23 Sep 2022 07:20 |
| Last Modified: | 23 Sep 2022 07:20 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3784 |
Actions
Actions (login required)
 |
View Item |