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

王 冠，郝晓星

(1.北京工业大学 信息学部，北京 100124；2.北京市可信计算重点实验室，北京 100124)

0 引 言

UEFI作为定义在平台固件层与操作系统层之间的一个开放且抽象的业界标准编程接口，与传统的BIOS相比绝大部分代码采用C语言编写，提升了UEFI固件的开发效率，并且采用驱动模块化设计提高了UEFI系统的可扩展性，使得UEFI迅速取代BIOS。与此同时，UEFI固件程序容量几何数量增长，功能愈加复杂，新颖的接口以及驱动加载模式，再加上大量的C语言源码问题，使得UEFI固件的安全问题更加明显，更由于UEFI固件在计算机中的特殊位置，使其成为攻击操作系统的跳板[1]。目前针对UEFI固件的安全检测技术主要是模糊测试技术、污点分析技术、符号执行技术。模糊测试技术[2-3]在大体量软件漏洞检测中具有先天优势，可重用性高，但自动化程度不高，效率低下，代码覆盖率不高。污点分析技术[4]可提供精确的信息流传播跟踪，但需要额外的系统开销与大量的先验分析，检测条件苛刻。符号执行技术[5]由于对路径敏感，状态爆炸问题严重，没有很高的分析精度。

形式化方法[6-8]是基于严格的数学基础，对计算机硬件、软件系统进行形式规约、开发和验证的技术。形式化验证方法对程序模型和安全属性进行自动验证且验证时能覆盖整个程序空间，漏报率低，非常适合高安全级别系统或程序的安全验证及分析。为对UEFI模块中安全漏洞进行分析与检验，提高UEFI固件的安全性，该文提出一种针对UEFI模块的形式化建模与验证的方法。该方法先对UEFI模块中可能存在的安全漏洞属性和UEFI模块进行形式化建模分析，再利用数据抽象技术[8-9]缓解形式化验证过程中的状态爆炸问题。

1 相关技术

1.1 形式化方法

形式化方法的两项主要研究内容为形式规约与形式化验证。形式规约利用形式规约语言描述整个系统的模型或者系统需要满足的安全属性[7]。形式化验证就是验证现有的程序或者系统是否满足其形式规约。形式化验证有两种形式，基于演绎的定理证明和基于算法的模型检验。定理证明的基本思想为：程序或系统满足其形式规约，然后通过一系列推理规则，以演绎推理的方式来证明此逻辑命题的正确性[7]。模型检验[7,9-10]提出的基本思想是：随着计算机并发系统的高速发展，验证一个程序或系统是否满足一个公式要比证明该公式在所有情况下均被满足要容易得多，所以提出了在有限状态自动机模型上来验证公式的可满足性的新思路。模型检验通过自动遍历程序或系统的有限状态来检验系统模型与其性质规约的满足关系。如果程序或系统的形式化模型不满足给定的性质规约，模型检验算法会给出不满足的反例，可以根据反例对系统或程序进行分析和调试，如果模型检验算法未发现反例，则系统或程序一定满足所检验的性质[7]。

1.2 有限状态自动机

有限状态自动机(finite state automaton，FSA)[11-12]分为非确定和确定两种形式，两者是等价的，其唯一的区别就是状态转移函数不同，确定有限状态机一个输入对应一个状态转移，非确定有限状态自动机一个输入对应多个状态转移，然后从多个状态转移中非确定地选择其中一个。有限状态自动机识别正则语言[12]，其所接受的所有字符串构成了自动机识别的语言L(M)。确定有限状态自动机的定义如下：

定义1：确定有限状态自动机(deterministic finite automaton，DFA)可以写成元组的形式(Q，Σ，δ，Q0，F)，其中：

(1)Q表示状态的非空有限集合，∀q∈Q，q称为DFA的一个状态；

(2)Σ表示输入字符的集合，Σ={a0,a1,…,an}；

(3)δ表示状态转移或移动函数，δ：Q×Σ*→Q，δ(qn，an)=qm；

(4)Q0∈Q表示DFA的初始状态;

(5)F⊆Q表示DFA的终止状态集合，∀q∈F，q称为DFA的一个终止状态。

确定有限状态自动机DFA从初始状态Q0开始，逐个读入字符集Σ中的字符，根据当前状态qn、输入的字符an和状态转移函数δ来决定DFA的下一状态qm。当输入字符结束，如果DFA的当前状态qm∈F，表示DFA接受该字符集Σ，否则表示DFA不接受该字符集。

1.3 下推自动机

下推自动机(push down automaton，PDA)[11-12]除了包含有限状态外，还包括一个长度不限的栈，下推自动机的状态转移不仅参考有限状态部分还要考虑栈的当前状态，状态转移过程还包括栈的出栈、入栈操作。下推自动机的定义如下：

定义2：下推自动机PDA可以写成元组的形式(Q，Σ，Γ，δ，Q0，Z0，F)，其中：

(1)Q、Σ、Q0、F与DFA中含义一致;

(2)Γ表示有限的堆栈字母表，为能够推入堆栈的符号的集合;

(3)δ表示转移函数，δ为Q×(Σ∪{ε})×Γ到Q×Γ*子集的映射，映射关系：δ(q,a,X)={(q1,γ1)，(q2,γ2)，…，(qn,γn)}，控制着自动机的行为。形式上δ的自变量可以表示为一个三元组δ(q,a,X)，其中q∈Q，表示PDA当前状态;a∈Σ或a=ε，ε为空串表示不是输入符号;X∈Γ，表示当前堆栈栈顶符号;

δ的输出是序对(q,γ)的有穷集合，其中q表示新状态，γ表示堆栈符号用来替代当前堆栈栈顶符号X，如果γ=ε，则弹出栈顶元素X，如果γ=X，堆栈不发生改变，如果γ=YZ，那么栈顶符号X被Z代替，然后Y推入栈；

(4)Z0∈Γ，表示PDA栈中的初始符号。

2 形式化建模与验证方法设计

该文使用模型检验对UEFI模块进行形式化验证，其中UEFI模块代码采用下推自动机PDA进行建模，UEFI模块中可能存在的安全漏洞属性采用确定有限状态自动机DFA进行建模，最后采用模型检验算法验证UEFI模块是否满足给定的安全漏洞属性模型。UEFI模块形式化验证流程如图1所示。

图1 形式化验证流程

2.1 安全漏洞属性建模

利用有限状态自动机对UEFI模块的安全漏洞属性进行建模。首先，需要对安全漏洞进行形式化分析，确定安全漏洞的状态集合Q、初始状态Q0、终止状态集合F。其次，将安全漏洞所涉及的一系列可能的程序点采用抽象语法树(abstract syntax tree，AST)[13]进行描述，作为有限状态自动机的输入信息Σ。最后，根据状态间的转移关系设计状态间的转移函数δ。安全漏洞的形式化描述中每一次状态转移的结果是确定的，所以基于确定有限状态自动机DFA的UEFI模块安全漏洞属性模型(security vulnerabilities deterministic finite automaton，SVDFA)的定义如下：

定义3：SVDFA可以写成元组的形式(Q，Σ，δ，Q0，F)，其中：

(1)Q表示安全漏洞所涉及的非空有限状态集合，∀q∈Q，q为在安全漏洞状态转移时可能达到的任意状态;

(2)Σ表示可能引起安全漏洞状态转移的程序操作表达式集合，程序操作源码转为与上下文无关的AST语法描述的表达式;

(3)δ表示安全漏洞状态转移函数集合，δ：Q×Σ*→Q，δ(qn,an)=qm，qn∈Q表示当前状态，an∈Σ表示输入的程序节点表达式，qm∈Q表示转移后状态;

(4)Q0∈Q表示安全漏洞的初始状态;

一是，养殖草鸡需要较大的放养场地，慈王村拥有丰富的土地资源，村民荒地较多，鸡舍环境干净优越。得天独厚的自然条件极其适宜草鸡养殖。二是，草鸡优良的保健价值日益得到市场的青睐。三是，慈王村领导干部对草鸡散养技术、环境调控与疾病防疫有一定的研究。四是，慈王村地理位置优越，茶园、农家乐数量居多，当地清真食品“爆炒草鸡”远近闻名，草鸡市场供不应求，销售优势明显。

(5)F⊆Q表示满足安全漏洞的最终接受状态集合。

SVDFA的状态迁移从初始状态Q0开始，如果当前程序执行点的AST表达式an与当前状态qn能满足状态转移函数δ(qn,an)=qm，SVDFA当前状态由qn变为qm，如果程序检验完毕，SVDFA在状态转移过程中有状态q∈F，则表示该程序可能出现安全漏洞模型描述的安全问题，否则没有出现安全漏洞属性模型描述的安全问题。UEFI模块中的安全问题可能非常复杂，如果一开始就对一个复杂的安全问题进行形式化建模将非常困难且不精确。通常一个复杂的安全问题由几个简单的安全问题组成，采用笛卡尔乘积的方式将一些简单安全漏洞属性模型{Mi=(Qi,Σi,δi,Q0i,Fi)}集合组合成一个复杂的安全漏洞属性模型S=(Q，Σ，δ，Q0，F)，这种建模方式使得安全漏洞描述模块化，并且使得模型扩展、复用成为可能。

2.2 程序控制流模型

数据抽象作为一种解决状态爆炸问题的有效手段，其基本思想就是在对系统进行模型检验时剔除系统中与检验无关的信息，仅保留有用信息，最后对抽象系统进行分析与验证就会变得容易，进而缓解模型检验时的状态爆炸问题。将UEFI模块近似抽象为对应的控制流模型后，对于复杂的UEFI模块，状态空间数量仍然很多，而要检验的安全漏洞属性往往是有限状态空间。该文根据安全漏洞属性再次压缩控制流模型，将控制流模型中与安全漏洞属性无关的控制流进行删除，进一步压缩状态空间，最终得到只与安全漏洞属性相关的UEFI模块抽象模型。将UEFI模块代码抽象为与程序节点相关的控制流模型，只对抽象出的控制流进行建模，降低整个模型的复杂度。本建模方式关注点在于程序执行路径中有哪些可能被执行的函数或方法以及执行顺序，并不考虑真实执行下的具体数据流，是一种对原系统的近似抽象。UEFI模块的程序控制流图(UEFI control flow graph，UCFG)定义如下：

定义4：UCFG可以写为元组的形式(N，E，IE，CE)，其中：

(1)N表示所有程序节点的集合，∀n∈N，n表示程序控制流中的一个程序节点，n具有三种属性n(NAME，OP，TYPE)，其中NAME表示程序点的名称，OP表示程序节点源码转为抽象语法树AST描述后的表达式，TYPE表示程序节点的类型。程序节点TYPE有三种类型;

·CALL，表示调用普通过程(方法或函数)的程序节点;

·RETURN，表示此程序节点为return操作;

·OTHER，表示除CALL和RETURN以外的其他程序节点。

(3)IE表示传输边，为程序控制流中普通过程内的程序节点传输边，IE={|n1,n2∈N且n1,n2属于同一过程内};

(4)CE表示调用边，为程序控制流中普通过程间的程序节点调用边，CE={|n1,n2∈N且n1,n2不属于同一过程内}。

例如，在对如图2所示的函数调用序列进行控制流建模时会有：传输边IE={(n1,n2)}，表示一条从程序点n1到程序点n2的过程内传输边；调用边CE={(n1,nx)，(n2,ny)}，表示会有从程序点n1到函数FunctionA()定义节点nx和n2到函数FunctionB()定义节点ny两条调用边。

图2 函数调用序列

由于静态分析只是对语法语义的分析，并不涉及真实数据流，对于条件判断语句如if-else或while等控制结构，并不会做出精准判断，目前采用的建模策略为默认每条分支都有可能执行，如图3的代码序列，会产生传输边IE={(n1,n2)，(n1,n3)}。

图3 控制结构序列

通过上述UEFI模块程序控制流模型UCFG，就可以描述一个程序中所有的程序节点转换路径，源程序被抽象为一个从入口程序点出发，沿着传输边IE与调用边CE的一条有限或无限的有向图。

UEFI模块安全漏洞属性的有限状态机模型SVDFA中的Σ集合数量有限，且在大多数情况下远远少于程序控制流UCFG中的程序点集合N的数量，所以在抽象的程序控制流中仍有大量与安全漏洞检测无关的控制流节点，该文利用安全漏洞属性模型SVDFA对程序控制流UCFG进行压缩，删减无用节点，节点类型的判定算法描述如下：

1.initialize: Uesful Node UF←{}，Uesless Node UL ←{}

2.for ∀n∈Ndo

3. ifn∈Eor n.OP∈SVDFA. Σ then

4.UF←{n}

5. end if

6.end for

7.for ∀n∈Ndo

8.ifn∉UF and (∀n∈DFS(n，{IE，CE}) ) ∉ UF then

9.UL←{n}

10. end if

11.end for

其中DFS(n，{IE，CE})函数表示找出程序节点n在边集{IE，CE}中直接或间接调用的所有节点。

2.3 程序建模

将UEFI模块代码抽象的程序控制流模型UCFG转换为下推自动机PDA时，Q，Q0，F都只包含一个虚拟状态{s}，即表示在UCFG→PDA时PDA不存在状态的转换，只是利用Σ，Γ，δ来记录程序节点的执行路径。UEFI模块代码的下推自动机模型(UEFI push down automaton，UPDA)定义如下：

定义5：UPDA可以表示为元组形式(Q，Σ，Γ，δ，Q0，Z0，F)，其中：

(1)Q={s}，表示状态的有限集合;

(2)Σ={IE∪CE}，表示输入符号的有限集合，实际为控制流模型UCFG中所有类型边的集合;

(3)Γ={Ν}，表示有限的堆栈字母表，实际为控制流模型UCFG中所有程序节点的集合N;

(4)δ表示转移函数集合，δ为Q×(Σ∪{ε})×Γ到Q×Γ*子集的映射，映射关系：δ(s,a,X)={(s,γ1)，(s,γ2)，…，(s,γn)}。转移函数生成算法如下:

1.for ∀e∈Σ，e={|n1,n2∈Σ} do

2. if e.n1.TYPE=RETURN then

3. UPDA.δaddδ(s，e，e.n1)={(s，ε)}

4. end if

5. if e.n1.TYPE=CALL then

6.UPDA.δaddδ(s，e，e.n1)={(s，e.n2e.n1)}

7. end if

8. if e.n1.TYPE=OTHER then

9. UPDA.δaddδ(s，e，e.n1)={(s，e.n2)}

10. end if

11.end for

(5)Q0=s，表示初始状态;

(6)Z0∈{E}，表示UPDA堆栈中的初始符号，实际为控制流模型UCFG中的程序入口节点;

(7)F={s}，表示UPDA的接受状态或终结状态集合。

2.4 形式化验证

基于自动机理论[12]的形式化验证框架如下：假设采用Σ表示程序中所有程序节点表达式集合，S⊆Σ*表示所有符合安全漏洞属性的程序节点执行序列，γ∈Σ*表示程序中一条可行的程序节点执行序列。Γ⊆Σ*表示程序中所有可行程序节点执行序列的集合。判断S∩Γ是否为空，如果为空则说明没有出现安全漏洞，不为空则可能出现安全问题。

通常程序可能的执行序列Γ是不可计算集，因此S∩Γ为一个不可判定问题，但可以通过限定S和Γ的形式将问题具体化来判定。首先，在UEFI模块中通常的时序安全漏洞属性的程序节点序列都能使用正则语言描述，假设S为正则语言，则存在SVDFA可以识别S，即S⊆L(SVDFA)。其次，程序的可行执行路径需要一个栈来记录返回调用者地址，需要用上下文无关语言描述，所以假设Γ为一个上下文无关的语言，则存在UPDA可以识别Γ，即Γ⊆L(UPDA)。判定S∩Γ变为判定L(SVDFA)∩L(UPDA)是否为空，则定义P=L(SVDFA)∩L(UPDA)，因为L(SVDFA)为正则语言，L(UPDA)为上下文无关语言，则P为上下文无关语言。同理，P可以被一个下推自动机(security vulnerabilities UEFI push down automaton，SVUPDA)接受，且SVUPDA为SVDFA与UPDA的交集。SVUPDA可由SVDFA与UPDA组合而成[14]，定义如下：

定义6：SVUPDA可以表示为元组形式(Q，Σ，Γ，δ，Q0，Z0，F)，其中：

(1)Q表示状态的有限集合，实际值为SVDFA中安全漏洞的状态集合Q;

(2)Σ表示输入符号的有限集合，实际值为UPDA中所有类型边的集合Σ;

(3)Γ表示有限的堆栈字母表，实际值为UPDA中所有程序节点的集合Γ；

(4)δ表示转移函数集合，δ为Q×(Σ∪{ε})×Γ到Q×Γ*子集的映射，映射关系：δ(q,a,X)={(q1,γ1)，(q2,γ2)，…，(qn,γn)}。转移函数生成算法描述如下:

1.for ∀i∈UPDA.δ，i(s,e,n1)={(q1，X)}，e={|n1,n2∈Σ} do

2. if i.X=i.n2then

3. for ∀j∈SVDFA.δ，j(qn，an)=qmdo

4. if i.n1.op = j.anthen

5.SVUPDA.δaddδ(j.qn，i.e，i.n1)={( j.qm，i.n2)})

6. end if

7. end for

8. end if

9. if i.X = i.n2i.n1then

10. for ∀q∈SVDFA.Q do

11.SVUPDA.δaddδ(q，i.e，i.n1)={(q，i.n2i.n1)})

12. end for

13. end if

14. if i.X=εthen

15. for ∀q∈SVDFA.Q do

16. SVUPDA.δaddδ(q，i.e，i.n1)={(q，ε)})

17. end for

18. end if

19.end for

从上述转移函数算法中可知，当UPDA中的程序节点类型TYPE为CALL或RETURN时，SVUPDA的状态不发生变化，只是记录SVUPDA的堆栈变化，当UPDA中的程序节点类型TYPE为OTHER时，既记录SVUPDA的堆栈变化，也记录了状态的转移。

(5)Q0表示初始状态，实际值为SVDFA中安全漏洞的初始状态Q0;

(6)Z0表示堆栈中的初始符号，实际值为UPDA中栈初始符号Z0；

(7)F表示SVUPDA的接受状态或终结状态集合，实际值为SVDFA中的安全漏洞的最终接受状态集合F。

通过文献[15-16]中的模型检验算法判断SVUPDA接受的语言L(P)是否为空就可判断是否出现安全漏洞，如果为空，则表示未出现安全漏洞模型SVDFA描述的安全漏洞，不为空则表示可能出现所描述的问题，需要确认是否为误报。之所以出现误报，是因为静态的语法语义分析并不考虑实际数据流，Γ除了接受实际可行路径集合外，也会接受实际数据流时不会发生的路径。但是，因为Γ⊆L(UPDA)，可以得到S∩Γ⊆L(SVDFA) ∩L(UPDA)，这保证了给定安全漏洞属性模型的完全性，即可能存在误报但无漏报。

3 实验结果与分析

基于自动机的模型检验主要能力取决于对UEFI模块中安全漏洞属性模型描述的丰富性、准确性，以及是否有状态爆炸引起的性能问题。在安全漏洞属性模型丰富性方面，该文考虑到UEFI模块中可以通过引入StdLib包调用C标准库及GNU C库，对UEFI标准库、C标准库及CNU C库进行分析，总结了六种类型的安全漏洞模型，安全漏洞模型的分类与数量如下：缓冲区溢出类型13种；资源重复释放5种；空指针引用7种；格式化字符串9种；竞态条件3种；函数调用路径7种。该文共对12个UEFI模块代码混合植入上述六类，44种的安全漏洞，共计563个由国家信息安全漏洞库CNNVD公布的EDKII中真实安全漏洞，对UEFI模块进行形式化验证，验证结果如表1所示。

表1 安全漏洞检测结果

从表1可以看出，在被检测的UEFI模块中，植入563个安全漏洞，检测报出604个可能存在的安全问题，其中包括检测出557个植入的安全漏洞，误报47个，统计漏报率1.06%，误报率7.78%。经过分析发现，漏报的主要原因是安全漏洞属性模型的不丰富造成，符合安全漏洞模型的安全漏洞都可以检测出来，检测结果基本符合形式化验证中阐述的不会有漏报的理论，降低漏报率的主要方法是不断丰富和精确安全漏洞属性模型。误报率达7.78%，经分析发现，大部分误报都是由于静态分析时并没有考虑真正数据流，在模型检验时有大量真实情况下不可达路径的原因，例如资源重复释放、竞态条件、函数调用路径类漏洞的误报，主要是因为真实数据流情况下会在条件判断的确定分支里进行资源释放，在程序抽象时会对条件判断的所有的分支进行统计，造成误报。对于性能分析，主要是验证在对程序控制流进行压缩和未压缩时的性能分析，来验证压缩算法可以缓解状态爆炸，提高检测性能。该文对代码规模约为500～5 000行范围的UEFI模块分别植入相同的6类，共65个安全漏洞进行20次检验，耗时平均值结果如图4所示。

图4 模型检验耗时

随着代码规模的增大，程序的状态空间会呈现指数增长趋势，在计算机性能不变的前提下，在未压缩的模型检验中，耗时与状态空间成正比，耗时趋势呈指数增长，预计随着代码规模持续增大会出现状态爆炸，内存不足的问题。在压缩后的模型检验中，状态空间是跟软件规模和安全漏洞属性状态数量组成的线性函数，随着软件规模持续增大，状态空间线性增长，达到缓解状态爆炸的目的。

4 结束语

固件主要负责计算机中硬件初始化和预备操作系统启动环境等功能，处于计算机中极其重要的位置，有着较高的安全级别，并且随着UEFI模块规模的逐渐庞大，被攻击面逐渐增加。该文提出一种针对UEFI模块的形式化建模与验证的方法，基于有限状态自动机和下推自动机分别对UEFI模块中的安全漏洞属性和代码进行形式化建模，采用模型检验算法进行形式化验证，同时利用数据抽象的思想压缩程序控制流的状态规模，缓解状态爆炸问题。对44种UEFI模块中可能出现的安全问题进行建模，12个植入安全问题且不同代码规模的UEFI模块进行形式化验证，实验结果表明，该检验方法漏报率为1.06%，误报率7.78%，并较好地缓解了状态爆炸问题。