CISPA
Browse
cispa_all_3784.pdf (835.98 kB)

Axiomatic hardware-software contracts for security

Download (835.98 kB)
conference contribution
posted on 2023-11-29, 18:22 authored by Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, Caroline Trippel
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.

History

Preferred Citation

Nicholas Mosier, Hanna Lachnitt, Hamed Nemati and Caroline Trippel. Axiomatic hardware-software contracts for security. In: ISCA ACM International Symposium on Computer Architecture (ISCA). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

ISCA ACM International Symposium on Computer Architecture (ISCA)

Legacy Posted Date

2022-09-23

Open Access Type

  • Hybrid

BibTeX

@inproceedings{cispa_all_3784, title = "Axiomatic hardware-software contracts for security", author = "Mosier, Nicholas and Lachnitt, Hanna and Nemati, Hamed and Trippel, Caroline", booktitle="{ISCA ACM International Symposium on Computer Architecture (ISCA)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC