面向形式化安全分析的微体系结构关系模型
密码学与安全
2021-12-21 v1 硬件体系结构
摘要
对于精确定义微体系结构对软件安全（即安全契约）影响的软硬件契约的需求日益增长。我们认为，此类契约应明确考虑支撑硬件泄漏的微体系结构级实现细节，从而在契约与其所代表的微体系结构之间建立直接对应关系。同时，这些契约应保持尽可能抽象，以支持高效的形式化分析。鉴于这些目标，我们提出了泄漏 containment 模型（LCMs）——一种新颖的公理化安全契约，支持对程序在特定微体系结构上运行时的安全保证进行形式化推理。我们的核心贡献是源自用于形式化处理器内存一致性模型的既有公理化词汇、用于形式化定义 LCMs 的公理化词汇表。利用该词汇表，我们将微体系结构泄漏（聚焦于通过硬件内存系统的泄漏）形式化，从而可在程序中自动检测。为说明 LCMs 的有效性，我们给出两个案例研究。首先，我们证明我们的泄漏定义忠实地涵盖了文献中一组（瞬态与非瞬态）微体系结构攻击。其次，我们开发了基于 LCMs 的静态分析工具，可自动识别程序中的 Spectre 漏洞，并能扩展到分析 libsodium 等实际规模代码库。
引用
@article{arxiv.2112.10511,
title = {Relational Models of Microarchitectures for Formal Security Analyses},
author = {Nicholas Mosier and Hanna Lachnitt and Hamed Nemati and Caroline Trippel},
journal= {arXiv preprint arXiv:2112.10511},
year = {2021}
}