Formal Detection Method for Hardware Vulnerabilities and Trojan of Embedded Devices

摘要

As become more widely used, embedded systems security has increasingly gained attention. From the hardware point of view, this paper describes the background of approach to the vulnerabilities and hardware Trojan detection of embedded system, basic ideas and objectives; established the model- ESM (Embedded Systems Model) used to describe embedded systems, provides the encoding method of the ESM system state. Based on this model, this article describes how to use model checking methods to detect vulnerabilities and Trojan existence of an embedded system.