摘要
针对硬件设计长期缺乏有效的安全验证方法问题,提出了一种硬件安全门级细粒度形式化验证方法.该方法使用形式化语言在逻辑门层面上描述硬件电路的安全属性,构造包含安全属性跟踪逻辑的形式化语义语句,从而将硬件设计转化为电路语义模型,并结合霍尔逻辑三元组理论构造用于验证该模型安全属性的定理.定理的证明过程是以人机交互的方式在定理证明器环境下验证定理的合理性.实验结果表明,该方法能够形式化地遍历电路语义模型的状态空间,精确验证不同输入状态下电路语义模型的安全性.该方法通过构造安全属性跟踪逻辑提高了验证的精确性,结合定理证明提高了验证覆盖率,能够有效地验证硬件设计的安全性.
No effective security verification method for hardware design is available for a long time.To solve this problem,this paper proposes a Fine-granularity Gate Level Formal Verification Method for Hardware Security,which is able to describe the security properties of the circuit and construct the semantic circuit in the customized formal language on Coq.With the help of the Hoare Logic theory,a provable theorem for verifying the security property of the semantic circuit is generated.The process of verification relies on tactics to generate and validate the proof in human-computer interaction.The results show that this method not only verifies the security properties of the semantic model,but also solves the problem of insufficient verification coverage in simulation.In conclusion,this method can raise accuracy and efficiency of verification.
作者
秦茂源
慕德俊
胡伟
毛保磊
QIN Maoyuan;MU Dejun;HU Wei;MAO Baolei(Research&Development InstitutcofAutomationControl,Northwestern Polytcchnical University in Shenzhen,Shenzhen 518057,China)
出处
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2018年第5期143-148,共6页
Journal of Xidian University
基金
国家自然科学基金资助项目(61672433)
深圳市科技创新委员会基础研究资助项目(201703063000517)
国家密码发展基金资助项目(MMJJ20170210)
中央高校基本科研业务费专项资金资助项目(3102017OQD094)
关键词
硬件设计
安全验证
定理证明
形式化语义模型
细粒度
hardware design
security verification
theorem proof
formal semantic model
fine-granularity
