Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors

• URL: http://arxiv.org/abs/2401.09383v1
• Date: Wed, 17 Jan 2024 17:54:53 GMT
• Title: Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors
• Authors: Gideon Mohr, Marco Guarnieri, Jan Reineke,
• Abstract summary: 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.
• Score: 6.061386291375516
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. For a given ISA, our approach relies on human experts to (a) capture the space of possible contracts in the form of contract templates and (b) devise a test-case generation strategy to explore a microarchitecture's potential leakage. For a given implementation of an ISA, these two ingredients are then used to automatically synthesize the most precise leakage contract that is satisfied by the microarchitecture. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors. Our experiments demonstrate the practical applicability of the methodology and uncover subtle and unexpected leaks.

Related papers

• Designing and Implementing a Generator Framework for a SIMD Abstraction Library [53.84310825081338]
  We present TSLGen, a novel end-to-end framework for generating an SIMD abstraction library. We show that our framework is comparable to existing libraries, and we achieve the same performance results.
  arXiv  Detail & Related papers  (2024-07-26T13:25:38Z)
• 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)
• Mechanistic Design and Scaling of Hybrid Architectures [114.3129802943915]
  We identify and test new hybrid architectures constructed from a variety of computational primitives. We experimentally validate the resulting architectures via an extensive compute-optimal and a new state-optimal scaling law analysis. We find MAD synthetics to correlate with compute-optimal perplexity, enabling accurate evaluation of new architectures.
  arXiv  Detail & Related papers  (2024-03-26T16:33:12Z)
• Testing side-channel security of cryptographic implementations against future microarchitectures [38.73923812516342]
  A recent study suggests that new microarchitectural optimizations might open the Pandora's box of microarchitectural attacks. We develop an expressive domain-specific language, called LmSpec, that allows chip vendors to specify the leakage model for the given optimization. We conduct an empirical study of 18 proposed microarchitectural optimizations on 25 implementations of eight cryptographic primitives in five popular libraries.
  arXiv  Detail & Related papers  (2024-02-01T14:56:54Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• 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)
• Security Verification of Low-Trust Architectures [2.7080187684202968]
  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.
  arXiv  Detail & Related papers  (2023-09-01T00:22:24Z)
• Citadel: Real-World Hardware-Software Contracts for Secure Enclaves Through Microarchitectural Isolation and Controlled Speculation [8.414722884952525]
  Hardware isolation primitives such as secure enclaves aim to protect programs, but remain vulnerable to transient execution attacks. This paper advocates for processors to incorporate microarchitectural isolation primitives and mechanisms for controlled speculation. We introduce two mechanisms to securely share memory between an enclave and an untrusted OS in an out-of-order processor.
  arXiv  Detail & Related papers  (2023-06-26T17:51:23Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  We consider vertical logistic regression (VLR) trained with mini-batch descent gradient. We provide a comprehensive and rigorous privacy analysis of VLR in a class of open-source Federated Learning frameworks.
  arXiv  Detail & Related papers  (2022-07-19T05:47:30Z)
• 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)
• Detecting Security Fixes in Open-Source Repositories using Static Code Analyzers [8.716427214870459]
  We study the extent to which the output of off-the-shelf static code analyzers can be used as a source of features to represent commits in Machine Learning (ML) applications. We investigate how such features can be used to construct embeddings and train ML models to automatically identify source code commits that contain vulnerability fixes. We find that the combination of our method with commit2vec represents a tangible improvement over the state of the art in the automatic identification of commits that fix vulnerabilities.
  arXiv  Detail & Related papers  (2021-05-07T15:57:17Z)

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.