基于符号执行的格式化字符串漏洞自动验证方法研究

王瑞鹏, 张 旻, 黄 晖, 沈 毅

(国防科技大学电子对抗学院，合肥，230037)

随着信息化程度的不断提高，信息系统被广泛应用于金融、医疗、国防、工控等重要领域。高度信息化带来便利的同时也对网络空间安全提出了更高的要求。漏洞是威胁网络空间安全的重要因素，其中格式化字符串漏洞是一种常见的软件漏洞，它由Tymm Twillman首次发现于1999年[1]，其主要成因是程序未对来自外部的输入内容做出严格过滤，导致格式化控制符参数能够被外部输入所影响[2]，进而对信息系统产生较大威胁。例如CVE-2012-0809漏洞[3]，该漏洞可以提升Linux用户的权限，危害较大。因此对格式化字符串漏洞的挖掘和验证意义十分重大。

现有的自动化漏洞挖掘方法能够挖掘到大量的软件漏洞[4-8]，但不能对产生漏洞的可利用性进行验证。因此，漏洞自动验证技术在近些年成为了软件安全领域的一个研究热点。在漏洞自动验证领域，符号执行技术的准确性和可靠性使其成为自动化程序分析的重要工具。目前基于符号执行的自动化漏洞自动验证系统有很多，如AEG[9]、Mayhem[10]、CRAX[11]等，其中AEG系统利用到了源码信息，其余系统都在二进制程序层面对漏洞进行自动验证。上述的系统都期望解决通用的漏洞自动验证，其漏洞验证模型中包含针对多种不同漏洞类型的验证方式，同时存在很多文献[12～17]针对特定漏洞或特定的漏洞验证方法，如黄钊等人的FSVDTG[12]主要针对格式化字符串漏洞进行漏洞验证方法研究，方皓[13]等人主要针对Return-to-dl-resolve漏洞验证方法进行研究。上述的大部分漏洞自动验证系统都是通过分析漏洞利用特点，构建漏洞验证模型，生成漏洞验证约束条件，约束求解得到漏洞验证代码。因此，漏洞验证系统的适用范围，通常由系统内漏洞验证模型适用范围决定。现有系统在针对格式化字符串漏洞自动验证时，构建了参数位于栈空间的漏洞验证模型，而忽略了参数位于其他空间时的情况。

本文提出了一种基于符号执行的格式化字符串漏洞自动验证方法，对现有的格式化字符串漏洞验证系统的漏洞验证模型进行了拓展，提高了格式化字符串漏洞自动验证系统的性能，降低了对于漏洞可利用性的误判，扩大了系统的适用范围，解决了对格式化字符串参数位于堆区及BSS段空间的漏洞自动验证的问题。

1 格式化字符串漏洞

1.1 格式化字符串参数

格式化字符串参数是格式化字符串函数用于将指定的字符串转换为期望的输入输出格式的控制符参数，格式化字符串参数的格式如下：

%[parameter][flags][width][precision]
[length]type

一般以%开始，以type结束，例如“%d”。配合printf()等格式化字符串函数，能够将函数参数以指定格式进行输入输出。

其中parameter一般为n$，指获取格式化字符串中的指定参数，flags表示标志位，width输出的最小字段宽度，precision表示输出精度，即输出的最大长度，length表示输出的字节长度。

格式化字符串中的type表示了预期输入输出的格式。常见的type类型及其使用效果如表1所示[18]。

表1 常见type类型及其含义

1.2 格式化字符串漏洞

格式化字符串漏洞是格式化控制符参数被程序的外部输入污染所导致的。例如printf(a,b)语句，假设这里的a参数可被外部输入污染，若此时参数a中的内容为合法的格式化字符串内容时，变量b中的内容就会按照指定格式打印出来，但若a中内容为“%d%d”等非法格式化字符串内容，程序不仅会将变量b打印出来，而且会尝试将函数未定义的第3个参数打印出来，由于此时程序未定义第3个参数，所以系统便打印了非预期的内存内容[19]。如果精心构造格式化字符串漏洞中格式化控制符参数的内容，可以实现任意内存地址的读写，进而获取系统权限，引发严重的系统安全问题。

2 漏洞自动验证方法设计

本文提出了一种基于符号执行的格式化字符串漏洞自动验证方法。该方法核心流程如图1所示。

图1 方法核心流程

首先，监控程序的运行状态，在程序运行至格式化字符串函数时，进行漏洞的存在性检测；之后判断当前格式化字符串参数的存储位置，并根据参数的不同存储位置，构建对应的漏洞验证约束；最后，将构建好的约束作为约束求解器输入，约束求解得到最终漏洞验证输入实例。

2.1 漏洞存在性检测

如第1.1节中所述，格式化字符串漏洞是由于外部输入对格式化字符串参数的污染而导致的。本方法会监控程序中每个格式化字符串函数，判断格式化字符串参数是否被外部输入影响，从而判断漏洞的存在性。

首先对程序中目标危险函数进行挂钩操作。当测试程序运行至目标函数时对其进行拦截，并对目标函数的格式化字符串参数进行判断，若当前参数取值为符号值，则表明当前函数的格式化字符串参数已被系统引入的符号变元所污染，即该参数会被外部输入污染，从而证明格式化字符串漏洞的存在，反之，则说明当前函数不存在格式化字符串漏洞，如图2所示。

图2 漏洞存在性检测方法

2.2 栈空间格式化字符串漏洞验证约束构建

当漏洞的格式化字符串参数存储于栈空间时，可通过格式化字符串函数在栈空间内布置任意地址，进而利用格式化字符串漏洞实现对任意地址读写。利用形如address+%offset $s的漏洞验证载荷进行任意地址读操作，利用形如address + padding + %offset $n的漏洞验证载荷进行任意地址写操作。其中address表示目标读写地址，offset表示address与危险函数参数的相对偏移，该方法如图3所示。

图3 栈空间格式化字符串漏洞任意地址读写方法

通常期望写入address地址的数值远大于缓冲区大小，导致address + padding的长度无法满足漏洞验证条件，所以通常利用形如% num s的格式化字符串产生长度为num的字符串。

为了构建上述漏洞验证载荷，实现对address地址的读写操作，需要首先计算offset的取值，当前的格式化字符串缓冲区地址保存在第1个参数内，因此*(ESP+4)为栈中address的地址，因此offset的取值如式(1)所示。

offset=(*(ESP+4)-(ESP-4))/4

(1)

在计算格式化字符串时，由于期望向目标地址写入的值往往较大，采取一次覆盖目标地址为期望值的时间效率极为低下，所以，在这种情况下，可以采用两次写入的方法，既节省缓冲区大小，又可以缩短漏洞验证时间，即利用“%hn”一次写入下2字节数据，上述计算格式化字符串漏洞验证载荷过程如算法1所示。

1)算法1：计算格式化字符串漏洞验证载荷。

输入：目标地址Ta，目标值Tv，参数偏移Offset

输出：目标格式化字符串Fs

1.Tv_high=Tv<<16;

2.Tv_low=Tv mod 65536;

3.if Tv_high

4.Fs=(Ta+2)+(Ta)+＂%＂+(Tv_high-8)+＂s＂;

5.Fs +=＂%＂+(Offset) +＂$n%＂+(Tv_low - Tv_high) +＂s%＂+(Offset+1)+＂$n＂;

6.else

7.Fs=(Ta)+(Ta+2)+＂%＂+(Tv_low-8)+＂s＂ ;

8.Fs+=＂%＂+(Offset)+＂$n%＂+(Tv_high-Tv_low)+＂s%＂+(Offset+1)+＂$n＂;

9.end if

10.return Fs;

接下来，会构建符号内存内容与格式化字符串漏洞验证载荷相等的约束：

若未指定Ta或Tv，默认Ta为当前栈空间中存储的EIP值，并在栈空间内布置shellcode，使Tv等于shellcode的地址。但由于格式化字符串漏洞验证载荷长度受到Ta和Tv的影响，所以无法直接断定shellcode布置位置，进而无法确定Tv具体数值。为了解决这一问题，本文采用了启发式算法来探寻shellcode的合理布置位置。从符号值的起始位置开始解尝试，并利用约束求解判断当前解是否为可行解，从而得到shellcode的合理布置位置，其过程如算法2所示。

2)算法2：启发式算法计算shellcode的合理布置位置。

输入：符号区域起始位置SymStart, 符号区域结束位置SymEnd, Shellcode,格式化字符串Fs

输出：shellcode布置位置ShellcodeLocal

1.for i = Symstart to SymEnd-len(Shellcode) do

2.Set(Shellcode,SymStart + i);

3.Fs= CalcFs(SymStart + i);

4.Set(Fs,SymStart);

5.if getSymSolution() then

6.return ShellcodeLocal;

7.end if

8.end for

在确定了shellcode的布置位置后，构建shellcode布置的约束条件为：

2.3 堆区及BSS段格式化字符串漏洞验证约束构建

当漏洞函数的格式化字符串参数存储于堆区及BSS段时，栈空间无法被直接写入地址。由于无法向栈空间写入目标地址，所以2.2节中的方法在当前情况下失效。目前大多的格式化字符串漏洞自动验证系统在遇到该情况时，会判定当前的漏洞无法被攻击者利用，从而给予该漏洞以中低危风险等级。但事实上，这种漏洞仍有可能通过间接方式，达到对目标地址的任意读写。

在程序运行时，程序的栈空间一般不会存在期望修改地址的指针，所以需要一个指向栈地址的指针，间接向栈空间填入期望修改的地址。而EBP寄存器在程序运行中的作用是将各个函数调用串联起来，所以EBP指针就是一条存在于栈空间内的指针链，因此系统会利用栈下存储的EBP指针，间接实现任意地址读写，如图4所示。

图4 堆区及BSS段格式化字符串漏洞任意地址读写方法

若此时目标地址Address的值无法确定，默认通过修改EBP将函数栈迁移至堆区及BSS段，并在该部分内存区域构建栈内存布局，控制程序执行流程，如图5所示。

图5 栈迁移的流程

通过格式化字符串修改栈空间内存放EBP内容的地址，使其指向格式化字符串参数所在空间，通过2次leave指令后，程序的ESP寄存器会指向该空间，此时程序的栈被迁移到该内存空间，随后的ret指令便会将程序执行流程劫持至shellcode处。此时格式化字符串漏洞验证载荷为“%”+value+“s%”+offset+“$nAAAA”+ShellcodeLocal+shellcode，其中ShellcodeLocal由算法2可得， offset为栈中EBP内容存放地址的函数参数相对偏移，可由各个函数栈的EBP成链的特点计算得到。

2.4 约束求解

在得到不同类型的格式化字符串漏洞验证用例约束后，对其进行处理，得到期望的漏洞验证用例生成的约束。

此时得到的约束由程序运行时的符号执行路径约束CrashConstraints和输入约束InputConstraints构成，当前约束能够触发程序漏洞路径，但其与第2.2、第2.3节中最终得到的约束产生了冲突，如下式所示。

(Eq Formatstring0(Read w8 0 buf))∩

(Eq "A" (Read w8 0 buf))

⋮

因此需要将输入约束InputConstraints从最终的生成约束中减去，得到约束为：

ExploitConstraints

将最终的约束作为约束求解器的输入，得到最终的漏洞验证代码。

3 实验

3.1 系统实现

依照上述方法，本文基于S2E[20]实现了格式化字符串漏洞自动验证原型系统FSAEG，框架如图6所示。系统利用QEMU[21]进行全系统仿真，对目标程序运行状态进行监控，利用KLEE[22]实现系统的符号执行功能，利用Z3[23]实现约束求解。

图6 FSAEG系统框架

格式化字符串漏洞自动验证插件通过监控器获取进程和模块加载的时刻以及程序运行时的状态，并利用获取到的信息构建漏洞自动验证约束条件，实现漏洞自动验证。

3.2 实验验证

本次实验的环境为Linux 32位系统关闭ASLR、CANARY、NX等漏洞利用缓解机制。实验宿主机配置为Windows 10、Intel Core i7-9750H@2.60 GHz、32 GB内存、虚拟机配置为Ubuntu 16.04、7 GB内存。

为了证明系统的有效性，本文以一个典型格式化字符串参数存储于栈空间的漏洞示例FMT-3，来验证系统在应对格式化字符串参数位于栈空间时自动验证的有效性。

FMT-3的代码如图7所示。在代码的13行，存在明显的格式化字符串漏洞，传入printf的格式化字符串为可以通过用户输入改变的s1，而s1的位置则处在栈空间内。

图7 FMT-3程序源码

以2019年BRHG自动化漏洞挖掘竞赛格式化字符串漏洞题目A0012来验证系统在应对格式化字符串参数位于栈以外空间时自动验证的有效性。

A0012代码如图8所示。在代码的23行，存在明显的格式化字符串漏洞。传入printf的格式化字符串为可以通过用户输入改变的buff，而buff处于bss段，漏洞函数调用前有3次其他函数调用。

图8 BRHG-A0012程序源码

在实验结果上，本系统能够对上述示例产生漏洞验证代码，如图9、图10所示，并成功实现漏洞验证，获取系统权限。

图9 FMT-3漏洞验证代码

图10 BRHG-A0012漏洞验证代码

为了对比不同系统之间的性能差异，本文对HEAP-FMT、TEA-FMT程序做了测试，其中HEAP-FMT为格式化字符串参数存储于堆空间的格式化字符串漏洞程序，TEA-FMT为带有tea[24]加密的缓冲区位于栈空间的格式化字符串漏洞程序。在对比FSVDTG、CRAX、AFL和本系统后，得到结果如表2所示。

表2 各系统对不同类型实例测试结果

针对该实验结果分析如下：

1)AFL是模糊测试的常用工具之一，其采用模糊测试技术对漏洞进行挖掘和测试，能够发现程序中格式化字符串漏洞，但是由于在FMT-3实例和BRHG-A0012实例中存在可持续输入的循环结构，导致AFL无法生成测试用例，且其并不支持对漏洞自动验证功能。

2)CRAX是一种典型的基于符号执行的漏洞自动验证工具，其支持对漏洞产生漏洞验证代码，但在判断格式化字符串时，需要格式化缓冲区长度大于50，故未能成功检测FMT-4及HEAP-FMT中的格式化字符串漏洞，此外CRAX只采用了格式化字符串栈中任意读写的漏洞验证模型，所以其不能对缓冲区位于其他空间的实例进行漏洞自动验证。

3)FSVDTG是专门针对格式化字符串漏洞进行漏洞测试的工具，其能够检测各种格式化字符串漏洞，并对部分程序能够进行漏洞自动验证，但是由于其同样只采用了单一的漏洞验证模型，所以不能对格式化字符串参数位于其他空间的漏洞程序进行漏洞自动验证。

本系统(FSAEG)能够能够检测格式化字符串漏洞，并在格式化字符串参数位于栈外其他空间时，成功实现漏洞验证代码的自动生成，达到其他系统所无法达到的效果。

在此次实验中，所有系统均无法对含有tea加密的实例TEA-FMT进行漏洞自动验证，主要原因是符号执行中约束求解器的性能瓶颈。

4 结语

本文总结了格式化字符串漏洞验证的相关原理，并针对现有系统无法解决的参数位于栈以外内存空间的漏洞自动验证问题，设计实现了能够适用于不同参数存储位置的格式化字符串漏洞自动验证系统FSAEG。最后通过实验验证了方法的有效性，并与同类方法进行了对比，证实了FSAEG系统能够有效解决目标问题。但由于符号执行本身的路径爆炸问题，使得符号执行并不能解决过于庞大的程序，因此在下一步的工作中，拟采用模糊测试、静态分析等手段，辅助符号执行，进一步提升系统的自动验证效果。