TY - GEN
T1 - Security Verification of Low-Trust Architectures
AU - Tan, Qinhan
AU - Fisseha, Yonathan
AU - Chen, Shibo
AU - Biernacki, Lauren
AU - Jeannin, Jean Baptiste
AU - Malik, Sharad
AU - Austin, Todd
N1 - Publisher Copyright:
© 2023 Copyright held by the owner/author(s)
PY - 2023/11/15
Y1 - 2023/11/15
N2 - Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.
AB - Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.
KW - Formal Verification
KW - Information Flow
KW - Low-Trust Architecture
UR - http://www.scopus.com/inward/record.url?scp=85179851824&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85179851824&partnerID=8YFLogxK
U2 - 10.1145/3576915.3616643
DO - 10.1145/3576915.3616643
M3 - Conference contribution
AN - SCOPUS:85179851824
T3 - CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
SP - 945
EP - 959
BT - CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery, Inc
T2 - 30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023
Y2 - 26 November 2023 through 30 November 2023
ER -