Resource isolation plays a crucial role in ensuring the security of hardware systems. Existing hardware security verification measures can identify improper isolation of hardware resources, but coverage is incomplete. As the search space increases with hardware size, the chances of an integrity flaw slipping through conventional verification methodologies also increase. In this work, we propose the application of Mandatory Access Control (MAC) models to the hardware resource isolation problem as an improvement to existing System-on-Chip (SoC) verification environments. To do so, we extend the definitions of subject and object, conventionally defined for the software domain, to a hardware context, allowing existing time-tested MAC policy models and verification methodologies to be directly applied to test the isolation of shared hardware resources. Using these definitions, we frame hardware isolation as a MAC problem and adopt the Biba interpretation of the Bell-LaPadula (BLP) model for hardware resource isolation. We use this model to propose a security verification methodology, in which subject-to-object interactions are defined as transactions, and are verified with respect to a security policy. Transactions that violate this security policy constitute a hardware isolation violation. We then use this transaction-based methodology to implement SystemVerilog-based verification environments for three open-source RISC-V cores. These environments are used to discover six instances of improper resource isolation (one novel, two previously documented, and three artificial test cases) with a simulation runtime overhead of less than 10%. These violations constitute security vulnerabilities in hardware, which a malicious user could exploit to access or modify memory regions or hardware peripherals that should be isolated, thereby violating trust.
Resource isolation plays a crucial role in ensuring the security of hardware systems. Existing hardware security verification measures can identify improper isolation of hardware resources, but coverage is incomplete. As the search space increases with hardware size, the chances of an integrity flaw...
See full abstract
Resource isolation plays a crucial role in ensuring the security of hardware systems. Existing hardware security verification measures can identify improper isolation of hardware resources, but coverage is incomplete. As the search space increases with hardware size, the chances of an integrity flaw slipping through conventional verification methodologies also increase. In this work, we propose the application of Mandatory Access Control (MAC) models to the hardware resource isolation problem as an improvement to existing System-on-Chip (SoC) verification environments. To do so, we extend the definitions of subject and object, conventionally defined for the software domain, to a hardware context, allowing existing time-tested MAC policy models and verification methodologies to be directly applied to test the isolation of shared hardware resources. Using these definitions, we frame hardware isolation as a MAC problem and adopt the Biba interpretation of the Bell-LaPadula (BLP) model for hardware resource isolation. We use this model to propose a security verification methodology, in which subject-to-object interactions are defined as transactions, and are verified with respect to a security policy. Transactions that violate this security policy constitute a hardware isolation violation. We then use this transaction-based methodology to implement SystemVerilog-based verification environments for three open-source RISC-V cores. These environments are used to discover six instances of improper resource isolation (one novel, two previously documented, and three artificial test cases) with a simulation runtime overhead of less than 10%. These violations constitute security vulnerabilities in hardware, which a malicious user could exploit to access or modify memory regions or hardware peripherals that should be isolated, thereby violating trust.
Hide full abstract
