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

作     者：王冠 郝晓星 WANG Guan;HAO Xiao-xing

作者机构：北京工业大学信息学部北京100124 北京市可信计算重点实验室北京100124 

出 版 物：《计算机技术与发展》 (Computer Technology and Development)

年 卷 期：2021年第31卷第12期

页      面：116-121页

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家重点研发计划(2019YFB2102303) 国家自然科学基金(61971014)。 

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

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