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

TL;DR

This paper introduces a formal verification approach for detecting hardware Trojans in non-interfering accelerators at RTL, eliminating the need for golden models and ensuring exhaustive detection of all sequential Trojans, including side-channel threats.

Contribution

A novel formal method for Trojan detection in non-interfering accelerators that does not rely on golden models or detailed specifications, enabling comprehensive pre-silicon security verification.

Findings

Successfully detects all sequential HTs in tested accelerators

Effective against complex trigger and payload Trojans

Does not require golden models or functional specifications

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.