Kevin Cheang

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2023-224

August 11, 2023

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

Hardware platforms, such as microprocessors and Trusted Execution Environments (TEEs), aim to provide strong memory isolation properties. However, in recent years, this has been shown not to be the case through hardware attacks such as the class of transient execution attacks. These attacks affect programs executing on widely-used microprocessor designs in our present-day devices. Although mitigations have been proposed, many have not been adopted and lack formal guarantees. As a result, security-critical applications have been conservative in using hardware platforms without some form of cryptographic approach for secure computation, despite the additional computational overhead. One approach to ensure safety for this class of attacks is to use formal methods to prove information flow properties. Yet, there is limited work in verifying attacks on hardware platforms that are heterogeneous in nature, namely those that contain hardware and software in the trusted computing base.

This thesis defines a notion of secure information flow for hardware platforms and proposes methods to formally verify non-interference-based properties efficiently using abstractions and composition. To accomplish the former, we formalize the trace property-dependent observational determinism property for capturing a new class of non-interference properties. This property is motivated by verifying transient execution attacks and the need for secure speculation. To enable efficient verification on hardware platforms, we introduce an efficient proof system, SymboTaint, and the formalism of information flow state machines to reason about secure information flow compositionally. Finally, we explore a complementary method to enforce secure information flow for general programs by relaxing the programming model of a family of TEE designs and by formally verifying them. This direction builds on top of existing abstractions of TEEs to provide memory isolation guarantees with an efficient memory-sharing scheme on TEEs through combined design and verification. Together, this provides a methodology for enforcing memory isolation for heterogeneous systems, where joint modeling and analysis of hardware and software have become imperative for security.

Advisors: Sanjit A. Seshia

---

BibTeX citation:

@phdthesis{Cheang:EECS-2023-224,
    Author= {Cheang, Kevin},
    Title= {Formal Specification and Verification of Secure Information Flow for Hardware Platforms},
    School= {EECS Department, University of California, Berkeley},
    Year= {2023},
    Month= {Aug},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-224.html},
    Number= {UCB/EECS-2023-224},
    Abstract= {Hardware platforms, such as microprocessors and Trusted Execution Environments (TEEs), aim to provide strong memory isolation properties. However, in recent years, this has been shown not to be the case through hardware attacks such as the class of transient execution attacks. These attacks affect programs executing on widely-used microprocessor designs in our present-day devices. Although mitigations have been proposed, many have not been adopted and lack formal guarantees. As a result, security-critical applications have been conservative in using hardware platforms without some form of cryptographic approach for secure computation, despite the additional computational overhead. One approach to ensure safety for this class of attacks is to use formal methods to prove information flow properties. Yet, there is limited work in verifying attacks on hardware platforms that are heterogeneous in nature, namely those that contain hardware and software in the trusted computing base.

This thesis defines a notion of secure information flow for hardware platforms and proposes methods to formally verify non-interference-based properties efficiently using abstractions and composition. To accomplish the former, we formalize the trace property-dependent observational determinism property for capturing a new class of non-interference properties. This property is motivated by verifying transient execution attacks and the need for secure speculation. To enable efficient verification on hardware platforms, we introduce an efficient proof system, SymboTaint, and the formalism of information flow state machines to reason about secure information flow compositionally. Finally, we explore a complementary method to enforce secure information flow for general programs by relaxing the programming model of a family of TEE designs and by formally verifying them. This direction builds on top of existing abstractions of TEEs to provide memory isolation guarantees with an efficient memory-sharing scheme on TEEs through combined design and verification. Together, this provides a methodology for enforcing memory isolation for heterogeneous systems, where joint modeling and analysis of hardware and software have become imperative for security.},
}

EndNote citation:

%0 Thesis
%A Cheang, Kevin 
%T Formal Specification and Verification of Secure Information Flow for Hardware Platforms
%I EECS Department, University of California, Berkeley
%D 2023
%8 August 11
%@ UCB/EECS-2023-224
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-224.html
%F Cheang:EECS-2023-224