About the Speaker

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.

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

Overview

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.

Key Points

• Researched a complete property set for detecting each Hardware Trojan modifying the program counter at an arbitrary position in a RISC-V processor with formal verification
• Developed a generic Hardware Trojan model for formal verification and special new properties to prove automatically our Hardware Trojan detection property set detects each Hardware Trojan
• Work gives guidance for reliable Hardware Trojan detection with formal verification and can be directly reused by RISC-V processor vendors to significantly increase the security-level of their RISC-V processors