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 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.