Lifting Micro-Update Models from RTL for Formal Security Analysis

Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, and Sanjit A. Seshia. Lifting Micro-Update Models from RTL for Formal Security Analysis. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 631–648, ACM, 2024.

Download

[pdf] 

Abstract

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. <p> 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.

BibTeX

@inproceedings{godbole-asplos24,
  author       = {Adwait Godbole and
                  Kevin Cheang and
                  Yatin A. Manerkar and
                  Sanjit A. Seshia},
  editor       = {Rajiv Gupta and
                  Nael B. Abu{-}Ghazaleh and
                  Madan Musuvathi and
                  Dan Tsafrir},
  title        = {Lifting Micro-Update Models from {RTL} for Formal Security Analysis},
  booktitle    = {Proceedings of the 29th {ACM} International Conference on Architectural
                  Support for Programming Languages and Operating Systems (ASPLOS)},
  pages        = {631--648},
  publisher    = {{ACM}},
  year         = {2024},
  abstract  = {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.
  <p>
  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.},
}