Contract-Aware Secure Compilation
Abstract
Microarchitectural attacks exploit the abstraction gap between the Instruction Set Architecture (ISA) and how instructions are actually executed by processors to compromise the confidentiality and integrity of a system. To secure systems against microarchitectural attacks, programmers need to reason about and program against these microarchitectural side-effects. However, we cannot -- and should not -- expect programmers to manually tailor programs for specific processors and their security guarantees. Instead, we could rely on compilers (and the secure compilation community), as they can play a prominent role in bridging this gap: compilers should target specific processors microarchitectural security guarantees and they should leverage these guarantees to produce secure code. To achieve this, we outline the idea of Contract-Aware Secure COmpilation (CASCO) where compilers are parametric with respect to a hardware/software security-contract, an abstraction capturing a processor's security guarantees. That is, compilers will automatically leverage the guarantees formalized in the contract to ensure that program-level security properties are preserved at microarchitectural level.
Cite
@article{arxiv.2012.14205,
title = {Contract-Aware Secure Compilation},
author = {Marco Guarnieri and Marco Patrignani},
journal= {arXiv preprint arXiv:2012.14205},
year = {2020}
}