复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节,但是,在实际的验证工作中,操作系统内核中全局性质的不变式定义,复杂数据结构程序的形式化描述和验证仍存在很多困难.本文针对操作系统内核中满足的全局性质,在代码层以函数为单位,用全局不变式进行定义,并在不同的函数中进行形式化验证,从而证明各个函数符合操作系统内核的全局性质;针对操作系统内核中经常使用的复杂数据结构程序,本文通过扩展形状图理论,提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序,并对该方法进行了正确性证明,最终成功验证操作系统内核中关于任务创建与调度,消息队列创建与操作相关的代码.

复杂内核数据结构的形式化描述和验证

对数据结构进行形式化描述是内核验证的重要组成部分,但是在实际的验证工作中,内核经常会使用一些不规则的数据结构,而对不规则数据结构的形式化定义仍存在诸多困难.针对内核中的复杂数据结构,本文提出使用结构拆分以及形状和内存分离的方法来形式化定义内核中的不规则数据结构,并运用该方法成功刻画了某航天操作系统内核的进程管理数据结构,最终成功验证了该内核中相关API的代码.相关的代码验证工作在定理证明工具Coq中完成.