一句话：提出微更新模型并实现从 RTL 半自动生成该模型的工具 PAUL，以支持可扩展的形式化硬件安全分析。
硬件执行攻击利用微架构交互泄露秘密数据，但直接对完整硬件实现进行软件验证难以扩展，而手工编写抽象模型既繁琐又易出错。本文提出「微更新模型」（micro-update models）作为微架构特性的抽象建模框架，使其既能保持可靠性（sound）又支持可扩展的安全分析，并设计算法从 RTL 半自动生成此类模型；该框架在原型工具 PAUL 中实现。作者在 Sodor5Stage 处理器以及 cva6（Ariane）处理器的组件上合成微更新模型，展示模型可层次化生成以扩展到更大设计，并观察到相比源 RTL，使用生成模型进行分析的运行时间最多提升 8 倍。
Hardware execution attacks exploit subtle microarchitectural interactions to leak secret data. While checking programs for the existence of such attacks is essential, verification of software against the full hardware implementation does not scale. Verification using abstract formal models of the hardware can help provide strong security guarantees while leveraging abstraction to achieve scalability. However, handwriting accurate abstract models is tedious and error-prone. Hence, we need techniques to generate models that enable sound yet scalable security analysis automatically. In this work, we propose micro-update models as a modelling framework that enables sound and abstract modelling of microarchitectural features. We also develop algorithms to generate micro-update models from RTL semi-automatically. We implement our modelling and generation framework in a prototype tool called PAUL. We evaluate our approach by synthesizing micro-update models for the Sodor5Stage processor and components from the cva6 (Ariane) processor. We demonstrate how these models can be generated hierarchically, thus increasing scalability to larger designs. We observe up to 8× improvement in run time when performing analysis with the generated models as compared to the source RTL.
@inproceedings{GodboleCMS24,
title = {Lifting Micro-Update Models from RTL for Formal Security Analysis},
author = {Adwait Godbole and Kevin Cheang and Yatin A. Manerkar and Sanjit A. Seshia},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3620665.3640418}
}