Compositional Proofs of Information Flow Properties for Hardware-Software Platforms

Kevin Cheang, Adwait Godbole, 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},
    Institution = {EECS Department, University of California, Berkeley},
    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