Adwait Godbole and Kevin Cheang and Yatin Manerkar and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2023-230

September 8, 2023

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-230.pdf

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, hand-writing accurate abstract models is tedious and error-prone. Hence, we need techniques to automatically generate models which enable sound yet scalable security analysis. 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 semi-automatically generate micro-update models from RTL. We implement our modelling and generation framework in a prototype tool. We evaluate our approach and tool 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 citation:

@techreport{Godbole:EECS-2023-230,
    Author= {Godbole, Adwait and Cheang, Kevin and Manerkar, Yatin and Seshia, Sanjit A.},
    Title= {Specifying and Generating Abstract Models for Formal Security Analysis},
    Year= {2023},
    Month= {Sep},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-230.html},
    Number= {UCB/EECS-2023-230},
    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, hand-writing accurate abstract models is tedious and error-prone. Hence, we need techniques to automatically generate models which enable sound yet scalable security analysis. 
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 semi-automatically generate micro-update models from RTL. We implement our modelling and generation framework in a prototype tool. We evaluate our approach and tool 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.},
}

EndNote citation:

%0 Report
%A Godbole, Adwait 
%A Cheang, Kevin 
%A Manerkar, Yatin 
%A Seshia, Sanjit A. 
%T Specifying and Generating Abstract Models for Formal Security Analysis
%I EECS Department, University of California, Berkeley
%D 2023
%8 September 8
%@ UCB/EECS-2023-230
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-230.html
%F Godbole:EECS-2023-230