A Scalable Formal Verification Methodology for Data-Oblivious Hardware

• URL: http://arxiv.org/abs/2308.07757v2
• Date: Mon, 11 Mar 2024 08:47:15 GMT
• Title: A Scalable Formal Verification Methodology for Data-Oblivious Hardware
• Authors: Lucas Deutschmann, Johannes Mueller, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz,
• Abstract summary: We propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core.
• Score: 3.518548208712866
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique for preventing the leakage of secret information through timing. It is based on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether or not an instruction satisfies this data-independent timing criterion varies between individual processor microarchitectures. In this paper, we propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. The proposed methodology is based on an inductive property that enables scalability even to complex out-of-order cores. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. In addition, the paper discusses several techniques that can be used to make the verification process easier and faster. We demonstrate the feasibility of the proposed methodology through case studies on several open-source designs. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core. In addition to several hardware accelerators and in-order processors, our experiments also include RISC-V BOOM, a complex out-of-order processor, highlighting the scalability of the approach.

Related papers

• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  We introduce a novel Unsupervised Continual Anomaly Detection framework called UCAD. The framework equips the UAD with continual learning capability through contrastively-learned prompts. We conduct comprehensive experiments and set the benchmark on unsupervised continual anomaly detection and segmentation.
  arXiv  Detail & Related papers  (2024-01-02T03:37:11Z)
• 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 Discrepancy Aware Framework for Robust Anomaly Detection [51.710249807397695]
  We present a Discrepancy Aware Framework (DAF), which demonstrates robust performance consistently with simple and cheap strategies. Our method leverages an appearance-agnostic cue to guide the decoder in identifying defects, thereby alleviating its reliance on synthetic appearance. Under the simple synthesis strategies, it outperforms existing methods by a large margin. Furthermore, it also achieves the state-of-the-art localization performance.
  arXiv  Detail & Related papers  (2023-10-11T15:21:40Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  Hardware-firmware co-verification is critical to design trustworthy systems. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification.
  arXiv  Detail & Related papers  (2023-09-14T19:24:57Z)
• Diagnostic Spatio-temporal Transformer with Faithful Encoding [54.02712048973161]
  This paper addresses the task of anomaly diagnosis when the underlying data generation process has a complex-temporal (ST) dependency. We formalize the problem as supervised dependency discovery, where the ST dependency is learned as a side product of time-series classification. We show that temporal positional encoding used in existing ST transformer works has a serious limitation capturing frequencies in higher frequencies (short time scales) We also propose a new ST dependency discovery framework, which can provide readily consumable diagnostic information in both spatial and temporal directions.
  arXiv  Detail & Related papers  (2023-05-26T05:31:23Z)
• PAC-Based Formal Verification for Out-of-Distribution Data Detection [4.406331747636832]
  This study places probably approximately correct (PAC) based guarantees on OOD detection using the encoding process within VAEs. It is used to bound the detection error on unfamiliar instances with user-defined confidence.
  arXiv  Detail & Related papers  (2023-04-04T07:33:02Z)
• The Wyner Variational Autoencoder for Unsupervised Multi-Layer Wireless Fingerprinting [6.632671046812309]
  We propose a multi-layer fingerprinting framework that jointly considers the multi-layer signatures for improved identification performance. In contrast to previous works, by leveraging the recent multi-view machine learning paradigm, our method can cluster the device information shared among the multi-layer features without supervision. Our empirical results show that the proposed method outperforms the state-of-the-art baselines in both supervised and unsupervised settings.
  arXiv  Detail & Related papers  (2023-03-28T10:05:06Z)
• A Robust and Explainable Data-Driven Anomaly Detection Approach For Power Electronics [56.86150790999639]
  We present two anomaly detection and classification approaches, namely the Matrix Profile algorithm and anomaly transformer. The Matrix Profile algorithm is shown to be well suited as a generalizable approach for detecting real-time anomalies in streaming time-series data. A series of custom filters is created and added to the detector to tune its sensitivity, recall, and detection accuracy.
  arXiv  Detail & Related papers  (2022-09-23T06:09:35Z)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  We show how to solve the problem of checking conformance of uncertain logs against data-aware reference processes. Our approach is modular, in that it homogeneously accommodates for different types of uncertainty. We show the correctness of our approach and witness feasibility through a proof-of-concept implementation.
  arXiv  Detail & Related papers  (2022-06-15T11:39:45Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Frequency-based Multi Task learning With Attention Mechanism for Fault Detection In Power Systems [6.4332733596587115]
  We introduce a novel deep learning-based approach for fault detection and test it on a real data set, namely, the Kaggle platform for a partial discharge detection task. Our solution adopts a Long-Short Term Memory architecture with attention mechanism to extract time series features, and uses a 1D-Convolutional Neural Network structure to exploit frequency information of the signal for prediction.
  arXiv  Detail & Related papers  (2020-09-15T02:01:47Z)

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.