Verifying Hardware Resource Isolation through Mandatory Access Control Policy

Published

May 28, 2026

Author(s)

Christopher Nokes, Kostas Amberiadis, D. Richard Kuhn, Edwards Reed, Michael Zuzak

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.

Conference Dates

April 8-10, 2026

Conference Location

San Francisco, CA, US

Conference Title

27th International Symposium on Quality Electronic Design (ISQED 2026)

Pub Type

Conferences

Download Paper

https://doi.org/10.1109/ISQED69900.2026.11534784

Local Download

Keywords

hardware verification, Mandatory Access Control, hardware vulnerability detection

Citation

Nokes, C. , Amberiadis, K. , Kuhn, D. , Reed, E. and Zuzak, M. (2026), Verifying Hardware Resource Isolation through Mandatory Access Control Policy, 27th International Symposium on Quality Electronic Design (ISQED 2026), San Francisco, CA, US, [online], https://doi.org/10.1109/ISQED69900.2026.11534784, https://tsapps.nist.gov/publication/get_pdf.cfm?pub_id=959997 (Accessed August 18, 2026)

Additional citation formats