Developing Methods For Formal Modeling And Security Verification Of Hardware Design

The integrated circuit is the core and foundation of the computer system.Due to the lack of effective security verification tools,hardware security is facing serious threats such as unsafe debug port,hardware Trojan,hardware timing side-channel,and so on.Traditional functional testing and verification can not satisfy the requirements of test coverage,and can not detect highly covert hardware timing side-channel and hardware Trojan.The information flow analysis provides a method to detect security vulnerabilities in the design and verification phases through formalizing hardware design from the perspective of information flow and verifying information flow security properties of the design.However,most of the existing methods are at a higher level of abstraction,which results in the difficulty in modeling,the high design complexity of formal language,and the difficulty in detecting hardware timing side-channel.To address these problems,this thesis focuses on research the information flow model,formal language,formal verification method for addressing hardware security vulnerabilities at the gate level abstract level.The main work and contributions of this thesis are as follows:(1)We propose a gate-level Coq semantic conservative information flow model to address the shortcomings of the high abstract level methods.The model uses a conservative label propagation strategy and designs a Coq semantic conservative information flow model formal language.This language only defines the concepts and operations related to labels and allows the Coq semantic conservative information flow model to capture all information flows in the system conservatively by type-checking without considering the influence of input data.Based on this model,we propose a method to detect security vulnerabilities by proving the desired information flow security properties.This method provides a minimum functional Coq semantic conservative information flow model logic library,a code conversion tool,and a formal description method for describing the desired information flow security properties,which are used to construct a Coq semantic conservative information flow model and desired theorem for any HDL design.Experimental results show that the proposed method can conservatively detect hardware security vulnerabilities such as hardware Trojan and timing side-channel that violate information flow security policy.(2)We propose a gate-level Coq semantic precise information flow model to address the false positives caused by conservative information flow models.This model uses a precise label propagation strategy and designs a Coq semantic precise information flow model formal language.Since this language considers the impact of input data on label propagation,the constructed model can capture the actual information flow by type-checking.Based on this model,this paper proposes a method to detect security vulnerabilities by proving the desired information flow security properties.This method provides a minimum functional Coq semantic precise information flow model logic library,an extended code conversion tool,and a formal description method,which are used to construct the Coq semantic conservative information flow model and expected theorem for any HDL design.Experimental results show that this method can accurately detect the hardware security vulnerabilities that violate the information flow policy,and can effectively eliminate false positives.(3)We discuss the Coq semantic conservative/precise information flow model from two aspects of complexity and accuracy,and then study the strategy of weighing the complexity and accuracy of the model,and further propose a dual model security verification based hardware Trojan detection method.Because this method makes full use of the advantages of the two models,hence it can detect hardware Trojans effectively and quickly.Besides,this method also designs a reverse derivation technology to deduce the trigger conditions of hardware Trojans by using the internal results of the qualitative analysis and electrical connections of the Coq semantic precise information flow model.Experiments show that this method can effectively detect hardware Trojans and their trigger conditions such as single plaintext,plaintext input sequence,internal clock,and so on.(4)We propose a gate-level time label tracking logic model to address the problem that the existing information flow models are difficult to distinguish time information flow from function flow.This model uses a set of time labels and the time label propagation policy to model hardware timing flow,instead of using security labels and security label propagation policy to model logical information flow.Based on this model,we propose a method to detect the hardware timing side-channels by model checking the desired hardware system execution time invariance properties.This method provides a minimum functional time label tracking logic library and a code conversion tool to generate the time label tracking logic model for any HDL design.Experimental results show that the proposed method can independently detect the hardware time side channel caused by unbalanced branches,fast channels,cache hit-miss without considering the influence of function flow.