Visible to the public When Capacitors Attack: Formal Method Driven Design and Detection of Charge-Domain Trojans

TitleWhen Capacitors Attack: Formal Method Driven Design and Detection of Charge-Domain Trojans
Publication TypeConference Paper
Year of Publication2019
AuthorsGuo, Xiaolong, Zhu, Huifeng, Jin, Yier, Zhang, Xuan
Conference Name2019 Design, Automation Test in Europe Conference Exhibition (DATE)
ISBN Number978-3-9819263-2-3
Keywordsanalog attacks, capacitor-enabled attacks, Capacitors, charge-domain leakage paths, charge-domain models, charge-domain trojans/vulnerabilities, circuit-level properties, cyber physical systems, Digital circuits, formal method driven design, Hardware, IC supply chain, information flow tracking based solution, information leakage paths, integrated circuit industry, Integrated circuit modeling, integrated circuits, invasive software, pubcrawl, resilience, Resiliency, supply chain security, Testing, trojan detection approaches, trojan horse detection, Trojan horses

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 circuit-level 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 charge-domain 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.

Citation Keyguo_when_2019