Security Verification of Low-Trust Architectures

Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean Baptiste Jeannin, Sharad Malik, Todd Austin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationCCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
PublisherAssociation for Computing Machinery, Inc
Pages945-959
Number of pages15
ISBN (Electronic)9798400700507
DOIs
StatePublished - Nov 15 2023
Event30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023 - Copenhagen, Denmark
Duration: Nov 26 2023Nov 30 2023

Publication series

NameCCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security

Conference

Conference30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023
Country/TerritoryDenmark
CityCopenhagen
Period11/26/2311/30/23

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Computer Science Applications
  • Software

Keywords

  • Formal Verification
  • Information Flow
  • Low-Trust Architecture

Fingerprint

Dive into the research topics of 'Security Verification of Low-Trust Architectures'. Together they form a unique fingerprint.

Cite this