A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators

• URL: http://arxiv.org/abs/2312.06515v1
• Date: Mon, 11 Dec 2023 16:44:19 GMT
• Title: A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators
• Authors: Anna Lena Duque Antón, Johannes Müller, Lucas Deutschmann, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz,
• Abstract summary: Hardware Trojans (HTs) in security-critical IPs like cryptographic accelerators pose severe security risks. We propose a novel formal verification method for HT detection in non-interfering accelerators at the Register Transfer Level (RTL) Our method guarantees the exhaustive detection of any sequential HT independently of its payload behavior, including physical side channels.
• Score: 5.1042748857552755
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The threat of hardware Trojans (HTs) in security-critical IPs like cryptographic accelerators poses severe security risks. The HT detection methods available today mostly rely on golden models and detailed circuit specifications. Often they are specific to certain HT payload types, making pre-silicon verification difficult and leading to security gaps. We propose a novel formal verification method for HT detection in non-interfering accelerators at the Register Transfer Level (RTL), employing standard formal property checking. Our method guarantees the exhaustive detection of any sequential HT independently of its payload behavior, including physical side channels. It does not require a golden model or a functional specification of the design. The experimental results demonstrate efficient and effective detection of all sequential HTs in accelerators available on Trust-Hub, including those with complex triggers and payloads.

Related papers

• Physical Layer Deception with Non-Orthogonal Multiplexing [52.11755709248891]
  We propose a novel framework of physical layer deception (PLD) to actively counteract wiretapping attempts. PLD combines PLS with deception technologies to actively counteract wiretapping attempts. We prove the validity of the PLD framework with in-depth analyses and demonstrate its superiority over conventional PLS approaches.
  arXiv  Detail & Related papers  (2024-06-30T16:17:39Z)
• Lazy Layers to Make Fine-Tuned Diffusion Models More Traceable [70.77600345240867]
  A novel arbitrary-in-arbitrary-out (AIAO) strategy makes watermarks resilient to fine-tuning-based removal. Unlike the existing methods of designing a backdoor for the input/output space of diffusion models, in our method, we propose to embed the backdoor into the feature space of sampled subpaths. Our empirical studies on the MS-COCO, AFHQ, LSUN, CUB-200, and DreamBooth datasets confirm the robustness of AIAO.
  arXiv  Detail & Related papers  (2024-05-01T12:03:39Z)
• Frequency-Aware Deepfake Detection: Improving Generalizability through Frequency Space Learning [81.98675881423131]
  This research addresses the challenge of developing a universal deepfake detector that can effectively identify unseen deepfake images. Existing frequency-based paradigms have relied on frequency-level artifacts introduced during the up-sampling in GAN pipelines to detect forgeries. We introduce a novel frequency-aware approach called FreqNet, centered around frequency domain learning, specifically designed to enhance the generalizability of deepfake detectors.
  arXiv  Detail & Related papers  (2024-03-12T01:28:00Z)
• Evasive Hardware Trojan through Adversarial Power Trace [6.949268510101616]
  We introduce a HT obfuscation (HTO) approach to allow HTs to bypass detection method. HTO can be implemented with only a single transistor for ASICs and FPGAs. We show that an adaptive attacker can still design evasive HTOs by constraining the design with a spectral noise budget.
  arXiv  Detail & Related papers  (2024-01-04T16:28:15Z)
• Scalable Ensemble-based Detection Method against Adversarial Attacks for speaker verification [73.30974350776636]
  This paper comprehensively compares mainstream purification techniques in a unified framework. We propose an easy-to-follow ensemble approach that integrates advanced purification modules for detection.
  arXiv  Detail & Related papers  (2023-12-14T03:04:05Z)
• DeMiST: Detection and Mitigation of Stealthy Analog Hardware Trojans [0.21301560294088315]
  Capacitance-based Analog Hardware Trojan (AHT) is one of the stealthiest HT that can bypass most existing HT detection techniques. We propose a novel way to detect such capacitance-based AHT in this paper.
  arXiv  Detail & Related papers  (2023-10-06T03:45:41Z)
• Trojan Playground: A Reinforcement Learning Framework for Hardware Trojan Insertion and Detection [0.0]
  Current Hardware Trojan (HT) detection techniques are mostly developed based on a limited set of HT benchmarks. We introduce the first automated Reinforcement Learning (RL) HT insertion and detection framework to address these shortcomings.
  arXiv  Detail & Related papers  (2023-05-16T16:42:07Z)
• Multi-criteria Hardware Trojan Detection: A Reinforcement Learning Approach [0.0]
  Hardware Trojans (HTs) can severely alter the security and functionality of digital integrated circuits. This paper proposes a multi-criteria reinforcement learning (RL) HT detection tool that features a tunable reward function for different HT detection scenarios. Our preliminary results show an average of 84.2% successful HT detection in ISCAS-85 benchmark.
  arXiv  Detail & Related papers  (2023-04-26T01:40:55Z)
• ATTRITION: Attacking Static Hardware Trojan Detection Techniques Using Reinforcement Learning [6.87143729255904]
  We develop an automated, scalable, and practical attack framework, ATTRITION, using reinforcement learning (RL) ATTRITION evades eight detection techniques across two HT detection categories, showcasing its behavior. We demonstrate ATTRITION's ability to evade detection techniques by evaluating designs ranging from the widely-used academic suites to larger designs such as the open-source MIPS and mor1kx processors to AES and a GPS module.
  arXiv  Detail & Related papers  (2022-08-26T23:47:47Z)
• Mate! Are You Really Aware? An Explainability-Guided Testing Framework for Robustness of Malware Detectors [49.34155921877441]
  We propose an explainability-guided and model-agnostic testing framework for robustness of malware detectors. We then use this framework to test several state-of-the-art malware detectors' abilities to detect manipulated malware. Our findings shed light on the limitations of current malware detectors, as well as how they can be improved.
  arXiv  Detail & Related papers  (2021-11-19T08:02:38Z)
• Scalable Backdoor Detection in Neural Networks [61.39635364047679]
  Deep learning models are vulnerable to Trojan attacks, where an attacker can install a backdoor during training time to make the resultant model misidentify samples contaminated with a small trigger patch. We propose a novel trigger reverse-engineering based approach whose computational complexity does not scale with the number of labels, and is based on a measure that is both interpretable and universal across different network and patch types. In experiments, we observe that our method achieves a perfect score in separating Trojaned models from pure models, which is an improvement over the current state-of-the art method.
  arXiv  Detail & Related papers  (2020-06-10T04:12:53Z)

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.