随机数发生器的安全性证明技术研究

摘要

从1965年4月摩尔在《电子学》杂志上的一篇文章中提出摩尔定律的半个多世纪以来，半导体发展迅速。集成电路已经应用到各个领域，无处不在，手机、电脑等数字产品深入每个人的生活，成为人们生活不可或缺的产品。因此集成电路的安全性越来越受到重视。
　　随着集成电路技术的不断发展，为了适应市场，降低电路的设计成本和研发周期，SoC开发已经成为集成电路的设计主流。IP库是SoC设计的重要组成部分，在使用第三方IP库的时候安全性也成为了一个突出的问题。集成电路的设计和制造分离，工厂迁往劳动力成本低的地区，不少设计也外包给了其他设计公司，在集成电路的设计过程中会使用到各种不同公司提供的电子设计自动化软件，因此现在的半导体芯片在设计过程中变得比以前更容易受到恶意篡改。
　　针对这个问题本文采用Coq来进行电路的安全性证明（等价安全性）。Coq是一种定理证明软件，适合于定理的正确性验证。本文先用Coq构建随机数发生器后处理算法的RTL代码的模型，然后将电路的RTL代码用这个模型转换成Coq语言。为了验证RTL代码是否包含硬件木马或者被人为的恶意篡改，采用Coq来验证RTL代码是否与设计时一致，以此来确定芯片的安全性。
　　随着集成电路的发展，现在密码领域的很多算法都在SoC系统中实现。Coq不仅可以用于RTL代码级的等价安全性证明，同样也可以用于密码SoC架构的等价安全性证明;结合随机预言模型，本文为另一种电路的安全性证明（计算安全性）做了理论阐述，为下一步的工作打下了一个理论基础。

目录

声明

致谢

摘要

插图与附表清单

1 绪论

1．1 课题背景

1．2 本文研究的意义和创新点

1．3 国内外研究现状

1．4 论文的主要研究内容与论文结构

2 Coq介绍及其电路RTL级等价安全性证明方法

2．1 Coq介绍

2．2 Coq的IDE环境

2．3 Coq的语法及功能介绍

2．4 Coq在RTL级的使用

2．4．1 集成电路设计的RTL验证

2．4．2 Coq的安全证明方法

2．5 本章小结

3 随机数后处理部件等价安全性证明

3．1 随机数后处理部件设计

3．1．1 随机数后处理理论

3．1．2 高阶随机数后处理部件

3．2 RTL代码转换

3．2．1 Coq到RTL转换函数

3．3 等价安全性证明

3．3．1 部分随机数后处理部件的Coq描述

3．3．2 等价安全性证明

3．4 随机预言机

3．4．1 密码协议安全性证明介绍

3．4．2 随机预言机的Coq形式化介绍

3．5 本章小结

4 总结与展望

参考文献

作者简介

作者攻读硕士学位期间发表的论文和专利