Security Verification of Low-Trust Architectures

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.

Title	Security Verification of Low-Trust Architectures
Creator	Tan, Q.
	Chen, S.
	Jeannin, J. B.
	Malik, S.
	Fisseha, Y.
	Austin, T.
	Biernacki, Lauren
Publisher	Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
Academic Department	Electrical & Computer Engineering
Academic Department	Computer Science
Division	Engineering
Division	Natural Sciences
Organization	Lafayette College
Date Issued	2023
Date Available	2023-12-20
Type	Article
Language	English
Keyword	Formal Verification
	Low-Trust Architecture
	Information Flow
Bibliographic Citation	Tan, Q., et al. (2023) "Security Verification of Low-Trust Architectures." Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM. 945-959.
Standard Identifier	Handle 10385/7d278v68f
Standard Identifier	DOI 10.1145/3576915.3616643
Permalink	http://hdl.handle.net/10385/7d278v68f
Rights Statement	Creative Commons - Attribution
Rights Holders	Jeannin, J. B.
	Tan, Q.
	Austin, T.
	Biernacki, L.
	Fisseha, Y.
	Malik, S.
	Chen, S.