Statistical and Formal Methods in Hardware Security

March 27, 2018

Yiorgos Makris

Professor ECE Department, The University of Texas at Dallas

Partly because of design outsourcing and migration of fabrication to low-cost areas around the globe, and partly because of increased reliance on third-party intellectual property, the integrated circuit (IC) supply chain is now considered far more vulnerable than ever before. With electronics ubiquitously deployed in sensitive domains and critical infrastructure, such as wireless communications, industrial environments, as well as health, financial and military applications, understanding the corresponding risks and developing appropriate remedies have become paramount. To this end, in this presentation I will discuss the role that statistical and formal methods can play in ensuring security and trustworthiness of ICs and the systems wherein they are deployed, and I will introduce two solutions that my research group has contributed to the area of hardware security.

The first contribution, known as Statistical Side-Channel Fingerprinting, is a statistical method for assessing whether an integrated circuit originates from a known distribution or not, based on parametric measurements such as delay, power, electromagnetic emanations, temperature, etc. Effectiveness of this method in detecting ICs which have been subjected to malicious modifications (a.k.a. hardware Trojans) will be demonstrated using silicon measurements from a custom-designed wireless cryptographic IC. Solutions to the main challenges of statistical side-channel fingerprinting, namely the availability of a statistically significant trusted population and the detection of hardware Trojans which are activated after deployment, will also be discussed and demonstrated in silicon.

The second contribution, known as Proof-Carrying Hardware Intellectual Property, is a formal method for proving compliance of an electronic design acquired from a third-party vendor with a set of security properties. These properties, which are expressed as theorems with corresponding proofs in a formal proof management system (i.e., Coq) and which can be automatically checked by the consumer, outline the boundaries of trusted operation without necessarily specifying the exact functionality of the design. Effectiveness of this method in certifying secure instruction execution will be demonstrated on a popular microcontroller and its utility for data secrecy protection through fully-automated information flow tracking will be demonstrated on a cryptographic core. 

I will conclude by revisiting the modus operandi of the hardware security research area as it enters its second decade of activity and I will emphasize the need for (i) intensified efforts towards statistical and formal methods which can offer risk bounds and provable security, and (ii) synergy platforms whereby hardware security can be seamlessly integrated with software security, network security and cryptography, towards developing holistic system-level solutions for both contemporary and emerging applications. In this context, I will also briefly review our recent efforts in mixed-signal and system-level proof-carrying hardware, covert wireless communications, machine learning-based malware detection and workload forensics, as well as in establishing an NSF Industry/University Cooperative Research Center on Hardware and Embedded System Security and Trust (CHEST).
Published on March 27th, 2018Last updated on March 29th, 2018