When Capacitors Attack: Formal Method Driven Design and Detection of Charge-Domain Trojans
Xiaolong Guo1,a, Huifeng Zhu2,c, Yier Jin1,b and Xuan Zhang2,d
1Department of Electrical and Computer Engineering, University of Florida
aguoxiaolong@ufl.edu
byier.jin@ece.ufl.edu
2Department of Electrical and Systems Engineering, Washington University in St. Louis
czhuhuifeng@wustl.edu
dxuan.zhang@wustl.edu
ABSTRACT
The rapid growth and globalization of the integrated circuit (IC) industry put the threat of hardware Trojans (HTs) front and center among all security concerns in the IC supply chain. Current Trojan detection approaches always assume HTs are composed of digital circuits. However, recent demonstrations of analog attacks, such as A2 and Rowhammer, invalidate the digital assumption in previous HT detection or testing methods. At the system level, attackers can utilize the analog properties of the underlying circuits such as charge-sharing and capacitive coupling effects to create information leakage paths. These new capacitor-based vulnerabilities are rarely covered in digital testings. To address these stealthy yet harmful threats, we identify a large class of such capacitor-enabled attacks and define them as charge-domain Trojans. We are able to abstract the detailed charge-domain models for these Trojans and expose the circuitlevel properties that critically contribute to their information leakage paths. Aided by the abstract models, an information flow tracking (IFT) based solution is developed to detect chargedomain leakage paths and then identify the charge-domain Trojans/vulnerabilities. Our proposed method is validated on an experimental RISC microcontroller design injected with different variants of charge-domain Trojans. We demonstrate that successful detection can be accomplished with an automatic tool which realizes the IFT-based solution.
