Biblio

Jeopardy to cybersecurity threats in electronic systems is persistent and growing. Such threats present in hardware, by means such as Trojans and counterfeits, and in software, by means such as viruses and other malware. Against such threats, we propose a range of embedded instruments that are capable of real-time hardware assurance and online monitoring.

Hardware Trojan Horses and active fault attacks are a threat to the safety and security of electronic systems. By such manipulations, an attacker can extract sensitive information or disturb the functionality of a device. Therefore, several protections against malicious inclusions have been devised in recent years. A prominent technique to detect abnormal behavior in the field is run-time verification. It relies on dedicated monitoring circuits and on verification rules generated from a set of temporal properties. An important question when dealing with such protections is the effectiveness of the protection against unknown attacks. In this paper, we present a methodology based on automatic generation of monitoring and formal verification techniques that can be used to validate and analyze the quality of a set of temporal properties when used as protection against generic attackers of variable strengths.