Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Doing Business As Name:University of Texas at Dallas
  • Yiorgos Makris
  • (972) 883-4360
Award Date:08/19/2013
Estimated Total Award Amount: $ 216,606
Funds Obligated to Date: $ 216,606
  • FY 2013=$216,606
Start Date:10/01/2013
End Date:09/30/2016
Transaction Type:Grant
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:TWC: Small: Collaborative: Toward Trusted Third-Party Microprocessor Cores: A Proof Carrying Code Approach
Federal Award ID Number:1318860
DUNS ID:800188161
Parent DUNS ID:042000273
Program:Secure &Trustworthy Cyberspace

Awardee Location

Street:800 W. Campbell Rd., AD15
Awardee Cong. District:32

Primary Place of Performance

Organization Name:University of Texas at Dallas
Street:800 W. Campbell Rd
Cong. District:32

Abstract at Time of Award

Third-party hardware Intellectual Property (IP), written as code in a Hardware Description Language (HDL), is extensively used in modern integrated circuits. Contemporary electronics typically include 75% of third party hardware IP and only 25% in-house design to provide customization or a profit-making edge. Such extensive use of third-party hardware IP in both commercial and military applications raises security and trustworthiness concerns, especially in today's globalized market. Malicious modifications to a module's HDL code may introduce vulnerabilities, jeopardizing the security of the larger system within which it is integrated. So how does one protect electronics from the threat of potentially tampered with third-party hardware IP? To this end, this project is developing a framework for facilitating acquisition of provably trustworthy microprocessor cores. Drawing concepts from software proof-carrying code (PCC), security-related properties are codified in a temporal logic to outline the boundaries of trusted operation. In the case of microprocessor cores, these security properties ensure that the microprocessor instruction set architecture (ISA) does not introduce malicious architectural state changes, thereby preventing attackers from using a programming interface to exploit maliciously introduced hardware modifications. A formal proof of these security properties is then crafted by the vendor and presented to the consumer, who can automatically check correctness and validate compliance to the security properties. An ecosystem for developing provably trustworthy microprocessor cores, including a foundations framework, libraries, software tools, and demonstrations, as well as an educational module on Trusted Integrated Circuits and Systems are being developed as part of this project.

Project Outcomes Report


This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.

In this project, we developed and enhanced a proof-carrying hardware framework for ensuring trustworthiness of hardware designs. Specifically, we developed rules to convert a hardware design to a formal representation and develop security properties ensuring trustworthiness of microprocessor circuits. These security properties ensure that instructions produce correct results at the specified register/memory location, do not illegally access registers or memory locations, and do not change the program execution flow. While our initial conversion methodology flattens the design hierarchy in the formal representation, we also enhanced the rules to preserve hierarchy. This new conversion approach enables development of hybrid hardware modules containing the hardware design and the lemmas which can be used in the development of proofs of security properties in higher level modules, thereby improving reusability of lemmas and reducing the proof development burden. To help designers in the conversion, we automated the process and introduced VeriCoq and VeriCoq-H which implement the conversion using the flat and hierarchy-preserving approach, respectively.


While automating the whole process, including the proof construction for security properties, requires a much broader effort and might not be entirely feasible, we were able to develop a fully automate proof-carrying hardware framework for specialized classes of circuits. Specifically, we enhanced the proof-carrying hardware framework with information flow tracking capabilities and introduced VeriCoq-IFT. VeriCoq-IFT , seeking to (i) automate the process of converting designs from HDL to the Coq formal language, (ii) generate security property theorems ensuring information flow policies, (iii) construct proofs for such theorems, and (iv) check their validity for the design, with minimal user intervention. VeriCoq-IFT can be utilized to reveal possible information leakage capabilities in hardware designs and we successfully tested its utility in evaluating trustworthiness of several genuine and Trojan infested DES and AES encryption cores. In conjunction with the original proof-carrying hardware framework, we also demonstrated that our methodology can be applied to protect data secrecy, including integrity of sensitive information, in hardware designs.


VeriCoq-IFT focuses on information leakage in the digital domain. The risk of accidental information leakage, however, is not restricted to the digital domain. Indeed, analog signals originating from sources of sensitive information, such as biometric sensors, as well as analog outputs of a circuit, could also carry or leak secrets. Moreover, similar to digital designs, analog circuits can also be contaminated with malicious information leakage channels capable of evading traditional manufacturing test. Compounding the problem, in analog/mixed-signal circuits such information leakage channels can cross the analog/digital or digital/analog interface, making their detection even harder. To this end, we invoked the proof-carrying hardware methodology to enable systematic formal evaluation of information flow policies in analog/mixed-signal designs. By integrating IFT across the digital and analog domain, we demonstrated that our method is able to detect sensitive data leakage from the digital domain to the analog domain and vice versa, without requiring any modification of the current analog/mixed-signal circuit design flow.



Last Modified: 03/29/2017
Modified by: Yiorgos Makris

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.