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

A Formal Modeling and Validation Method for UEFI Module

作　　者：王冠 郝晓星 WANG Guan;HAO Xiao-xing(Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China;Beijing Key Laboratory of Trusted Computing,Beijing 100124,China)

机构地区：[1]北京工业大学信息学部,北京100124 [2]北京市可信计算重点实验室,北京100124

出　　处：《计算机技术与发展》2021年第12期116-121,共6页Computer Technology and Development

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

摘　　要：固件作为一种固化在ROM中的特殊软件程序,主要负责加电自检,硬件设备初始化,引导操作系统等基础功能,运行级别和安全等级较高,亟需一种高效、可靠的UEFI模块安全检测方法。采用形式化方法对UEFI模块进行规约与验证,对于提高固件的安全性具有重要意义。基于现有的有限状态自动机和下推自动机基础,分别对UEFI模块中的安全漏洞属性和UEFI模块程序控制流进行形式化建模,利用模型检验对上述模型进行形式化验证。其中利用数据抽象思想将UEFI模块抽象为程序控制流且压缩其状态规模来缓解模型检验时的状态爆炸问题,并给出了相关模型的定义以及模型间转换、组合的算法。实验结果表明,对UEFI模块的抽象及压缩能够很好地缓解模型检验中的状态爆炸问题,并且该形式化验证方法能够实现对UEFI模块安全漏洞的自动化验证,且能够达到较低的漏报率。Firmware, as a special software program solidified in ROM,is mainly responsible for power-on self-check, hardware device initialization, guiding the operating system and other basic functions. The operating level and safety level are high, so an efficient and reliable UEFI module safety detection method is urgently needed. Formal methods are used to specify and verify UEFI modules, which is of great significance to improve the security of firmware. Based on the existing finite state automaton and push down automaton, the security vulnerability attributes and the program control flow of the UEFI module are formalized, and the above models are formally verified by model check. The UEFI module is abstracted into program control flow by data abstraction and its state scale is compressed to alleviate the state explosion problem in a model test, and the definition of related models and the algorithm of transformation and combination among models are given. The experiment shows that the abstraction and compression of the UEFI module can alleviate the state explosion problem in the model test, and the formal verification method can realize the automatic verification of the UEFI module security vulnerabilities and can achieve a low omission ratio.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]