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

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2023-204

August 9, 2023

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

While agile hardware design flows have led to performant computation platforms, hardware security vulnerabilities pose a threat to security-critical software running on these platforms. Verifying programs running on such platforms w.r.t. security properties faces two major challenges: (a) vulnerable software is often nested within large pieces of code, and (b) security properties require more fine-grained platform models (compared to functional properties), leading to complex verification queries. Our work is motivated by these challenges. To address (a) we develop SymboTaint, a Hoare-style proof system that allows the decomposition of monolithic security specifications over large programs into smaller verification conditions. For challenge (b), we develop Information Flow State Machines (IFSMs), a modeling framework that provides compositionality properties. As a case study, we develop a speculative microprocessor model called Speculative Abstract Platform (SAP) which captures hardware designs with a wide range of microarchitectural features. As an evaluation, we use IFSMs to model SAP and verify observational determinism on a broad class of attack programs running on SAP.

---

BibTeX citation:

@techreport{Cheang:EECS-2023-204,
    Author= {Cheang, Kevin and Godbole, Adwait and Manerkar, Yatin A. and Seshia, Sanjit A.},
    Title= {Compositional Proofs of Information Flow Properties for Hardware-Software Platforms},
    Year= {2023},
    Month= {Aug},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-204.html},
    Number= {UCB/EECS-2023-204},
    Abstract= {While agile hardware design flows have led to performant computation platforms, hardware security vulnerabilities pose a threat to security-critical software running on these platforms. Verifying programs running on such platforms w.r.t. security properties faces two major challenges: (a) vulnerable software is often nested within large pieces of code, and (b) security properties require more fine-grained platform models (compared to functional properties), leading to complex verification queries. Our work is motivated by these challenges. To address (a) we develop SymboTaint, a Hoare-style proof system that allows the decomposition of monolithic security specifications over large programs into smaller verification conditions. For challenge (b), we develop Information Flow State Machines (IFSMs), a modeling framework that provides compositionality properties. As a case study, we develop a speculative microprocessor model called Speculative Abstract Platform (SAP) which captures hardware designs with a wide range of microarchitectural features. As an evaluation, we use IFSMs to model SAP and verify observational determinism on a broad class of attack programs running on SAP.},
}

EndNote citation:

%0 Report
%A Cheang, Kevin 
%A Godbole, Adwait 
%A Manerkar, Yatin A. 
%A Seshia, Sanjit A. 
%T Compositional Proofs of Information Flow Properties for Hardware-Software Platforms
%I EECS Department, University of California, Berkeley
%D 2023
%8 August 9
%@ UCB/EECS-2023-204
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-204.html
%F Cheang:EECS-2023-204