Visible to the public Property Specific Information Flow Analysis for Hardware Security Verification

TitleProperty Specific Information Flow Analysis for Hardware Security Verification
Publication TypeConference Paper
Year of Publication2018
AuthorsHu, W., Ardeshiricham, A., Gobulukoglu, M. S., Wang, X., Kastner, R.
Conference Name2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
ISBN Number978-1-4503-5950-4
KeywordsAcceleration, Collaboration, Complexity theory, composability, control theory, Design methodology, formal verification, Hardware, hardware information flow analysis, hardware security, hardware security verification, hardware security vulnerabilities, Hardware Trojans, Human Behavior, human factors, information flow analysis, information flow models, information flow security, information theoretic security, Mathematical model, Metrics, policy-based governance, potential security violations, property specific information flow analysis, property specific search, property specific trimming technique, pubcrawl, resilience, Resiliency, Scalability, security, security critical paths, security model, security of data, security property, security verification, Timing, Trojan horses, unintended design flaws

Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.

Citation Keyhu_property_2018