Hardware Trojan detection by specifying malicious circuit properties

This work addresses the increasing danger of shipping integrated circuits (either fully digital or mixed signal) that contain malicious hardware modifications. Potential security threads are established by so called hardware Trojans, implemented in the physical silicon structure. A desire of system engineers is to identify such back-door functionalities during an early design phase. The paper discusses how techniques deduced from model checking applications can be used for Trojan detection. A set of potential malicious properties is defined and handed to an automatic tool. Any returned counterexample identifies a feasible attack path and is a basis for further detailed inspection.