|
| | | | |
| | | |
| Stat |
Members: 3665
Articles: 2'599'751
Articles rated: 2609
25 January 2025 |
|
| | | | |
|
Article overview
| |
|
|
Security Verification of Low-Trust Architectures | | Qinhan Tan
; Yonathan Fisseha
; Shibo Chen
; Lauren Biernacki
; Jean-Baptiste Jeannin
; Sharad Malik
; Todd Austin
; | | Date: |
1 Sep 2023 | | Abstract: | 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. | | Source: | arXiv, 2309.00181 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|
REGISTER