SPARCv8汇编程序形式化验证

发布时间：2021-09-01 09:44

　　系统软件是计算机系统的核心部分,其安全性和可靠性是构建高可信计算机系统的关键。而形式化验证技术基于严格的数学理论和方法,能够为系统软件的正确性提供强有力的保证。在系统软件中,内嵌汇编代码常被用于实现与底层硬件平台之间的交互。汇编代码的安全性和正确性对于保证整个系统的正确性是非常重要的。在某航天嵌入式操作系统的形式化验证工作项目中,该操作系统的内嵌汇编程序是由SPARCv8指令集编写的,而项目前期工作所采用的验证框架,无法验证这部分内嵌汇编程序的正确性。为了完善这一部分工作,本文基于己有的形式化验证技术提出了一套用于SPARCv8汇编程序验证的方法,并做出了如下贡献:首先,本文为SPARCv8汇编程序设计了一种霍尔风格的验证逻辑。并为验证逻辑中的推理规则提供了直接风格的（direct-style）、基于语义的解释。该验证逻辑支持SPARCv8汇编程序中函数调用的模块化验证,以及SPARCv8的三个特性的验证:包括延时跳转、特殊寄存器的延时写入和寄存器窗口机制。其次,应用所设计的验证逻辑,本文验证了某航天嵌入式操作系统中任务上下文切换程序的主要功能模块,累计共验证了约250行SPARCv8... 

【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校

【文章页数】：111 页

【学位级别】：硕士

【部分图文】：

图３．１?ＳＰＡＲＣｖ８程序机器模型??

刁寄存摇

定义了断言语言之后，我们在这一节开始介绍推理规则的设计，设计推理规??则的目的是为了证明程序满足其所对应的程序规范。所以，我们首先从程序规范??入手通过图４．３来向读者阐释我们验证逻辑中程序规范的定义。??（Ｓｐｅｃ）?＾?：：＝?｛ｆ?＾??ｆｉ：?＾１??１１??ｆ２：?０２??１２??０３１??Ｉｓ??代码堆Ｃ??图４．３验证逻辑程序规范??２６??


本文编号：3376757