Security Risks in AI Accelerators: Detecting RTL Vulnerabilities to Model Theft with Formal Verification

Security Risks in AI Accelerators: Detecting RTL Vulnerabilities to Model Theft with Formal Verification

연구 분야: Verification

학회: 2025 IEEE European Test Symposium (ETS)

The rapid growth of computational demands for Artificial Intelligence (AI) has spawned intensive research on dedicated AI accelerators being integrated into the hardware (HW) of modern computing systems. Unfortunately, the increased use of AI accelerators comes with new and relevant security risks. A serious threat is model theft, where attackers target the valuable AI model processed in such accelerators.In this work, we address model theft at the microarchitectural level. While various attacks have already been reported that use timing side channels in AI accelerators for model theft, there is a distinct lack of detection methods for such vulnerabilities. This paper contributes to filling this gap. We propose a formal threat model and develop a method to exhaustively prove security with respect to this threat. Our method is based on analyzing the timing dependence of the HW’s computation on all relevant parameters of the AI model. We demonstrate our approach both for data flow and systolic array architectures. In particular, we report a vulnerability in a optimization feature of Neural Networks (NNs) that was detected by our method.