Security Path Verification Through Joint Information Flow Analysis
Wei Hu, Xinmu Wang, Dejun Mu · 2018
Security path verification is an effective measure for identifying design paths that can lead to security violations. However, existing techniques in this realm typically lack the flexibility in formal models for verification performance-precision tradeoffs and rely on new design languages and tools. In this paper, we propose a security path verification technique through joint information flow analysis. We formalize qualitative information flow models of different precision and complexity to enable verification performance tradeoffs. We further employ quantitative information flow metrics to assess the severity of identified security path violations. Our information flow models and security properties are described in standard HDL and property specification languages respectively, allowing verification to be performed using tools familiar to hardware designers. Experimental results show that our method is effective in identifying security vulnerabilities caused by design flaw, timing channel and hardware Trojan with verification performance benefits.