一种面向UEFI模块的形式化建模与验证方法

摘要

固件作为一种固化在ROM中的特殊软件程序,主要负责加电自检,硬件设备初始化,引导操作系统等基础功能,运行级别和安全等级较高,亟需一种高效、可靠的UEFI模块安全检测方法.采用形式化方法对UEFI模块进行规约与验证,对于提高固件的安全性具有重要意义.基于现有的有限状态自动机和下推自动机基础,分别对UEFI模块中的安全漏洞属性和UEFI模块程序控制流进行形式化建模,利用模型检验对上述模型进行形式化验证.其中利用数据抽象思想将UEFI模块抽象为程序控制流且压缩其状态规模来缓解模型检验时的状态爆炸问题,并给出了相关模型的定义以及模型间转换、组合的算法.实验结果表明,对UEFI模块的抽象及压缩能够很好地缓解模型检验中的状态爆炸问题,并且该形式化验证方法能够实现对UEFI模块安全漏洞的自动化验证,且能够达到较低的漏报率.