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

来源：计算机技术与发展杂志2021年第12期北京时间：

作者：王冠;';郝晓星;'

单位：1. 北京工业大学 信息学部,北京 100124;2. 北京市可信计算重点实验室,北京 100124

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

关键词：UEFI;形式化方法;模型检验;安全漏洞;有限状态自动机;下推自动机