Security Verification of Low-Trust Architectures

• URL: http://arxiv.org/abs/2309.00181v1
• Date: Fri, 1 Sep 2023 00:22:24 GMT
• Title: Security Verification of Low-Trust Architectures
• Authors: Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik, Todd Austin,
• Abstract summary: We perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture. We first define the security requirements of the ISA of SE low-trust architecture. We show how these proof obligations can be successfully discharged using commercial formal verification tools.
• Score: 2.7080187684202968
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
  CHERI provides and enforces fine-grained memory protection directly in the hardware. VeriCHERI is conceptionally different from previous works in that it does not require any ISA specification. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.
  arXiv  Detail & Related papers  (2024-07-26T11:48:55Z)
• Securing the Open RAN Infrastructure: Exploring Vulnerabilities in Kubernetes Deployments [60.51751612363882]
  We investigate the security implications of and software-based Open Radio Access Network (RAN) systems. We highlight the presence of potential vulnerabilities and misconfigurations in the infrastructure supporting the Near Real-Time RAN Controller (RIC) cluster.
  arXiv  Detail & Related papers  (2024-05-03T07:18:45Z)
• Stop Stealing My Data: Sanitizing Stego Channels in 3D Printing Design Files [56.96539046813698]
  steganographic channels can allow additional data to be embedded within the STL files without changing the printed model. This paper addresses this security threat by designing and evaluating a emphsanitizer that erases hidden content where steganographic channels might exist.
  arXiv  Detail & Related papers  (2024-04-07T23:28:35Z)
• SISSA: Real-time Monitoring of Hardware Functional Safety and Cybersecurity with In-vehicle SOME/IP Ethernet Traffic [49.549771439609046]
  We propose SISSA, a SOME/IP communication traffic-based approach for modeling and analyzing in-vehicle functional safety and cyber security. Specifically, SISSA models hardware failures with the Weibull distribution and addresses five potential attacks on SOME/IP communication. Extensive experimental results show the effectiveness and efficiency of SISSA.
  arXiv  Detail & Related papers  (2024-02-21T03:31:40Z)
• Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors [6.061386291375516]
  We propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors.
  arXiv  Detail & Related papers  (2024-01-17T17:54:53Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• Towards Remotely Verifiable Software Integrity in Resource-Constrained IoT Devices [18.163077388258618]
  Low-cost security architectures have been proposed for remote verification of their software state via integrity proofs. This article provides a holistic and systematic treatment of this family of architectures. It also compares (qualitatively and quantitatively) the types of software integrity proofs, respective architectural support, and associated costs.
  arXiv  Detail & Related papers  (2024-01-09T01:50:21Z)
• Secure Instruction and Data-Level Information Flow Tracking Model for RISC-V [0.0]
  Unauthorized access, fault injection, and privacy invasion are potential threats from untrusted actors. We propose an integrated Information Flow Tracking (IFT) technique to enable runtime security to protect system integrity. This study proposes a multi-level IFT model that integrates a hardware-based IFT technique with a gate-level-based IFT (GLIFT) technique.
  arXiv  Detail & Related papers  (2023-11-17T02:04:07Z)
• A Novel Approach to Identify Security Controls in Source Code [4.598579706242066]
  This paper enumerates a comprehensive list of commonly used security controls and creates a dataset for each one of them. It uses the state-of-the-art NLP technique Bidirectional Representations from Transformers (BERT) and the Tactic Detector from our prior work to show that security controls could be identified with high confidence.
  arXiv  Detail & Related papers  (2023-07-10T21:14:39Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  We present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications. We provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology. We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions.
  arXiv  Detail & Related papers  (2021-06-03T16:45:40Z)
• Symbolic Reinforcement Learning for Safe RAN Control [62.997667081978825]
  We show a Symbolic Reinforcement Learning (SRL) architecture for safe control in Radio Access Network (RAN) applications. In our tool, a user can select a high-level safety specifications expressed in Linear Temporal Logic (LTL) to shield an RL agent running in a given cellular network. We demonstrate the user interface (UI) helping the user set intent specifications to the architecture and inspect the difference in allowed and blocked actions.
  arXiv  Detail & Related papers  (2021-03-11T10:56:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.