%0 Journal Article %T 基于门级信息流分析的多值逻辑形式化方法研究<br>Gate Level Information Flow Analysis for Formal Method of Multi-Valued Logic System %A 邰瑜 %A 慕德俊 %A 胡伟 %A 毛保磊 %A 郭蓝天 %J 西北工业大学学报 %D 2017 %X 硬件系统设计规模的增大使得测试和验证覆盖率难以保证，所隐含的安全漏洞容易导致敏感信息泄露。门级信息流分析方法能够实现对硬件中全部逻辑信息流精确度量，防止有害信息流所引发的信息泄露。现有的工作主要研究布尔逻辑系统下门级信息流分析的基本理论、生成算法、跟踪逻辑形式化及检测验证等问题。然而，在硬件系统的设计和验证中通常需要采用多值逻辑描述电路的逻辑状态，基于门级信息流分析方法，采用构造方法生成系统的信息流模型，研究多值逻辑标签传播问题，分别构建针对四值逻辑和九值逻辑的标签传播规则集，对门级信息流跟踪逻辑进行形式化描述，通过分析多值逻辑传播规则的逻辑特性对基本门信息流跟踪逻辑进行扩展。<br>The testing and verification coverage is hard to guarantee in the design phase due to the continuous increasing in the scale of integrated circuits. Consequently, the security vulnerabilities residing in hardware designs tend to cause leakage of sensitive information or system failure. As a solution, gate level information flow tracking (GLIFT) can precisely measure and effectively control all the information flows in the underlying hardware to prevent information leakage resulting from these harmful flows of information. However, preliminary research mainly focused on the basic theories of GLIFT and generation algorithms for tracking logic formalization under the Boolean logic system, while digital circuits are typically described using multi-valued logic system during hardware design and verification. This paper proposes to expand the gate level logic information flow analysis method for multi-valued logic system. We derive the label propagation rule set for four-valued and nine-valued logic systems by extending the minimum label propagation set for Boolean logic. In addition, the formal descriptions of GLIFT logic for primitive gates are amended in order to support the features of multi-valued logic in label propagation in computing hardware %K 门级信息流分析 %K 多值逻辑 %K 标签传播规则 %K 形式化描述 %K GLIFT逻辑< %K br> %K gate level information flow analysis %K multi-valued logic %K label propagation rules %K formal description %K GLIFT logic %U http://journals.nwpu.edu.cn/xbgydxxb/CN/abstract/abstract6848.shtml