Theorem proof based gate level information flow tracking for hardware security verification

Digital hardware lies in the heart of systems deployed in finance, medical care, basic infrastructure and national defense systems. However, due to the lack of effective security verification tools, hardware designs may contain security vulnerabilities resulting from performance optimizations, side...

Full description

Saved in:
Bibliographic Details
Published in:Computers & security 2019-08, Vol.85, p.225-239
Main Authors: Qin, Maoyuan, Hu, Wei, Wang, Xinmu, Mu, Dejun, Mao, Baolei
Format: Article
Language:English
Subjects:
Cybersecurity
Debugging
Defense programs
Electronic design automation
Formal method
Gate level information flow tracking
Hardware
Hardware security
Heart
Information flow
Low level
Malware
Properties (attributes)
Security verification
Security vulnerability
System effectiveness
Theorem proof
Theorem proving
Tracking
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Digital hardware lies in the heart of systems deployed in finance, medical care, basic infrastructure and national defense systems. However, due to the lack of effective security verification tools, hardware designs may contain security vulnerabilities resulting from performance optimizations, side channels, insecure debug ports and hardware Trojans, which provide attackers low level access to critical resources and effective attack surface to compromise a system. To address these security threats, we propose a theorem proof based gate level information flow tracking (GLIFT) method for formal verification of security properties and identifying security vulnerabilities that cause security property violations. Our method integrates a precise information flow tracking (IFT) model with the Coq theorem proof environment, inheriting the accuracy of GLIFT and the scalability of theorem proving based formal verification. We formalize semantic circuits and security theorems for proving security properties in order to detect security violations. The proposed method has been demonstrated on an OpenRISC development interface core and an RSA implementation both from OpenCores as well as several Trojan benchmarks from Trust-HUB. Experimental results show that the proposed method detects insecure debug port, timing channel and hardware Trojans that cause violation of important security properties such as confidentiality, integrity and isolation and also derives the trigger condition of hardware Trojans.
ISSN:0167-4048
1872-6208
DOI:10.1016/j.cose.2019.05.005