Reliable Hardware Trojan Detection for RISC-V Processors using Formal Verification

In this work we present a systematic formal verification methodology to detect Hardware Trojans reliably. We are first to suggest the additional use of signal connection properties and show how they have to be combined with design functionality properties to detect each inserted Hardware Trojan. For Hardware Trojans modifying the program counter we present a complete property set for detecting each inserted Hardware Trojan at an arbitrary position in a RISC-V processor. For all this properties we get full proofs with short runtimes. Additionally, we researched a generic Hardware Trojan model to formally proof detection coverage for our properties.

Christian Appold works as a Research Engineer in the field of Microprocessor R&D at automotive supplier DENSO in Munich. He studied Computer Science and did his PhD in the field of Model Checking based formal verification of parallel software at University of Würzburg. Afterwards he worked for companies like ARM, IBM or Dialog Semiconductor (now Renesas) in the field of formal verification of hardware, as a research engineer or in product development. One focus of his work in DENSO is ensuring Hardware Security of our processors and SoCs, which includes extending our use of formal verification.