标签: 形式化验证

针对科学实验载荷使用的Linux操作系统，对其测试方法等做了研究总结。模型检测作为一种全自动运行的形式化验证手段，在其适用领域对发现系统逻辑错误意义重大。针对操作系统测试需要，对Linux管道通信进行了源代码研究，使用有限状态自动机进行建模并转化为Promela语言，并运用SPIN模型检测工具对其进行了形式化验证；对之前研究中模型不完整、不够细化、主体间关联性等问题进行了改进和完善，并就实验中发现的问题进行分析，并提出了改进方案。

针对集成电路在RTL代码级设计阶段由于使用第三方IP软核引入的安全性问题，现有的功能测试方法较难实现全覆盖检测无法保障电路安全性。本文在已有基于携带证明代码思想的基础上改进提出一种安全性验证方法。该方法结合形式化验证平台coq，运用形式化逻辑描述电路代码和安全性假设，构造证明过程并采用系统的证明检查器验证证明过程。通过在DES电路代码的实验，说明了该验证方法能有效检测出电路中后门路径类型的硬件木马。相比较于测试类方法覆盖率不能达到100%而无法确定电路是非安全性，本文提出的方法可以确定电路是安全或非安全，能够保证电路代码级的安全可信性。