|
|
论文:2017,Vol:35,Issue(5):884-889 |
|
|
引用本文： |
|
|
邰瑜, 慕德俊, 胡伟, 毛保磊, 郭蓝天. 基于门级信息流分析的多值逻辑形式化方法研究[J]. 西北工业大学学报 |
|
|
Tai Yu, Mu Dejun, Hu Wei, Mao Baolei, Guo Lantian. Gate Level Information Flow Analysis for Formal Method of Multi-Valued Logic System[J]. Northwestern polytechnical university |
|
|
|
|
|
|
|
| 基于门级信息流分析的多值逻辑形式化方法研究 |
|
| 邰瑜, 慕德俊, 胡伟, 毛保磊, 郭蓝天 |
|
| 西北工业大学 深圳研究院, 广东 深圳 518057 |
| 摘要: |
| 硬件系统设计规模的增大使得测试和验证覆盖率难以保证，所隐含的安全漏洞容易导致敏感信息泄露。门级信息流分析方法能够实现对硬件中全部逻辑信息流精确度量，防止有害信息流所引发的信息泄露。现有的工作主要研究布尔逻辑系统下门级信息流分析的基本理论、生成算法、跟踪逻辑形式化及检测验证等问题。然而，在硬件系统的设计和验证中通常需要采用多值逻辑描述电路的逻辑状态，基于门级信息流分析方法，采用构造方法生成系统的信息流模型，研究多值逻辑标签传播问题，分别构建针对四值逻辑和九值逻辑的标签传播规则集，对门级信息流跟踪逻辑进行形式化描述，通过分析多值逻辑传播规则的逻辑特性对基本门信息流跟踪逻辑进行扩展。 |
| 关键词:
门级信息流分析
多值逻辑
标签传播规则
形式化描述
GLIFT逻辑
|
|
| Gate Level Information Flow Analysis for Formal Method of Multi-Valued Logic System |
|
| Tai Yu, Mu Dejun, Hu Wei, Mao Baolei, Guo Lantian |
|
| Shenzhen Research Institute, Northwestern Polytechnical University, Shenzhen 518057, China |
| Abstract: |
| 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. |
| Key words:
gate level information flow analysis
multi-valued logic
label propagation rules
formal description
GLIFT logic
|
|
| 收稿日期: 2017-03-01
修回日期:
|
| DOI: |
| 基金项目: 国家自然科学基金（61303224、61672433）、国家密码发展基金（MMJJ20170210）与深圳市科创委基础研究基金（201703063000517）资助 |
| 通讯作者:
Email： |
| 作者简介: 邰瑜(1982-),西北工业大学博士研究生,主要从事硬件安全及逻辑优化研究。
|
|
| 相关功能 |
|
|
|
|
| 作者相关文章 |
|
| 邰瑜 在本刊中的所有文章 |
| 慕德俊 在本刊中的所有文章 |
| 胡伟 在本刊中的所有文章 |
| 毛保磊 在本刊中的所有文章 |
| 郭蓝天 在本刊中的所有文章 |
|
|
|
|
|
|
|
|
参考文献: |
|
|
[1] Andrysco M, Kohlbrenner D, Mowery K, et al. On Subnormal Floating Point and Abnormal Timing[C]//IEEE Symposium on Security and Privacy, 2015:623-639
[2] Hwang D D, Schaumont P, Tiri K, et al. Securing Embedded Systems[J]. IEEE Security and Privacy, 2006, 4(2):40-49
[3] Sabelfeld A, Myers A. Language-Based Information-Flow Security[J]. IEEE Journal on Selected Areas in Communications, 200321(1):5-19
[4] Tiwari M, Wassel H W, Mazloom B, et al. Complete Information Flow Tracking from the Gates up[C]//The 14th International Conference on Architectural Support for Programming Languages and Operating Systems, 2009:109-120
[5] Hu W, Oberg J, Irturk A, et al. Theoretical Fundamentals of Gate Level Information Flow Tracking[J]. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 2011, 30(8):1128-1140
[6] Oberg J, Sherwood T, Kastner R. Eliminating Timing Information Flows in a Mix-Trusted System-on-Chip[J]. IEEE Design & Test, 2013, 30(2):55-62
[7] Zhang D, Wang Y, Suh G E, et al. A Hardware Design Language for Timing-Sensitive Information-Flow Security[J]. ACM SIGARCH Computer Architecture News, 2015, 43(1):503-516
[8] Ardeshiricham A, Hu W, Marxen J, et al. Register Transfer Level Information Flow Tracking for Provably Secure Hardware Design[C]//Design, Automation & Test in Europe Conference & Exhibition, 2017:1691-1696
[9] Hu W, Becker A, Ardeshiricham A, et al. Imprecise Security:Quality and Complexity Tradeoffs for Hardware Information Flow Tracking[C]//IEEE/ACM International Conference on Computer-Aided Design, 2016:1-8
[10] Mao B, Hu W, Althoff A, et al. Quantifying Timing-Based Information Flow in Cryptographic Hardware[C]//IEEE/ACM International Conference on Computer-Aided Design, 2015:552-559
[11] Mu D, Hu W, Mao B, et al. A Bottom-up Approach to Verifiable Embedded System Information Flow Security[J]. IET Information Security, 2014, 8(1):12-17
[12] Denning D E. Cryptography and Data Security[M]. Boston, Addison-Wesley Longman Publishing Co Inc, 1982 |
|
|
|
|
|
|
|
