[1]王 冠,郝晓星.一种面向 UEFI 模块的形式化建模与验证方法[J].计算机技术与发展,2021,31(12):116-121.[doi:10. 3969 / j. issn. 1673-629X. 2021. 12. 020]
　WANG Guan,HAO Xiao-xing.A Formal Modeling and Validation Method for UEFI Module[J].,2021,31(12):116-121.[doi:10. 3969 / j. issn. 1673-629X. 2021. 12. 020]
点击复制

一种面向 UEFI 模块的形式化建模与验证方法()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
31
期数:
2021年12期
页码:
116-121
栏目:
网络与安全
出版日期:
2021-12-10

文章信息/Info

Title:
A Formal Modeling and Validation Method for UEFI Module
文章编号:
1673-629X(2021)12-0116-06
作者:
王 冠1; 2 ; 郝晓星1; 2
1. 北京工业大学 信息学部,北京 100124;
2. 北京市可信计算重点实验室,北京 100124
Author(s):
WANG Guan1; 2 ; HAO Xiao-xing1; 2
1. Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China;
2. Beijing Key Laboratory of Trusted Computing,Beijing 100124,China
关键词:
UEFI; 形式化方法; 模型检验; 安全漏洞; 有限状态自动机; 下推自动机
Keywords:
UEFI; formal method; model checking; security vulnerabilities; finite state automaton; push down automaton
分类号:
TP301
DOI:
10. 3969 / j. issn. 1673-629X. 2021. 12. 020
摘要:
固件作为一种固化在 ROM 中的特殊软件程序,主要负责加电自检,硬件设备初始化,引导操作系统等基础功能,运行级别和安全等级较高,亟需一种高效、可靠的 UEFI 模块安全检测方法。 采用形式化方法对 UEFI 模块进行规约与验证,对于提高固件的安全性具有重要意义。 基于现有的有限状态自动机和下推自动机基础,分别对 UEFI 模块中的安全漏洞属性和 UEFI 模块程序控制流进行形式化建模,利用模型检验对上述模型进行形式化验证。 其中利用数据抽象思想将UEFI 模块抽象为程序控制流且压缩其状态规模来缓解模型检验时的状态爆炸问题,并给出了相关模型的定义以及模型间转换、组合的算法。 实验结果表明,对 UEFI 模块的抽象及压缩能够很好地缓解模型检验中的状态爆炸问题,并且该形式化验证方法能够实现对 UEFI 模块安全漏洞的自动化验证,且能够达到较低的漏报率。
Abstract:
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.

相似文献/References:

[1]高丽萍 褚伟.基于B方法的组件开发[J].计算机技术与发展,2007,(07):28.
　GAO Li-ping,CHU Wei.An Approach of Component Development with B Method[J].,2007,(12):28.
[2]张志锋 徐洁 邓璐娟 任雪利.基于B的UML形式化需求分析[J].计算机技术与发展,2007,(08):133.
　ZHANG Zhi-feng,XU Jie,DENG Lu-juan,et al.Requirement Analysis Formalized Using UML Based on B[J].,2007,(12):133.
[3]李勇,曹子宁. 基于需求的形式化建模与验证方法研究[J].计算机技术与发展,2017,27(06):7.
　LI Yong,CAO Zi-ning. Investigation on Formal Modeling and Verification MethodBased on Specification[J].,2017,27(12):7.
[4]战芸娇,魏欧,胡军,等.面向驾驶舱显示系统需求的形式化建模与分析[J].计算机技术与发展,2018,28(03):20.[doi:10.3969/ j. issn.1673-629X.2018.03.005]
　ZHAN Yun-jiao,WEI Ou,HU Jun,et al.Formal Modeling and Analysis of Cockpit Display System Requirements[J].,2018,28(12):20.[doi:10.3969/ j. issn.1673-629X.2018.03.005]
[5]卜星晨,曹子宁,王福俊.基于组件自动机的概率连续行为的形式化模型[J].计算机技术与发展,2020,30(11):1.[doi:10. 3969 / j. issn. 1673-629X. 2020. 11. 001]
　BU Xing-chen,CAO Zi-ning,WANG Fu-jun.Formal Model of Probabilistic Continuous Behavior Based on Component Automata[J].,2020,30(12):1.[doi:10. 3969 / j. issn. 1673-629X. 2020. 11. 001]
[6]耿 雪,邹盛荣*,刘晓莹,等.UML 到 Event-B 的系统化转换方法[J].计算机技术与发展,2023,33(12):113.[doi:10. 3969 / j. issn. 1673-629X. 2023. 12. 016]
　GENG Xue,ZOU Sheng-rong*,LIU Xiao-ying,et al.Systematic Transformation Method from UML to Event-B[J].,2023,33(12):113.[doi:10. 3969 / j. issn. 1673-629X. 2023. 12. 016]

更新日期/Last Update: 2021-12-10