Group of Software Security In Progress

GoSSIP @ LoCCS.Shanghai Jiao Tong University

FirmUp: Precise Static Detection of Common Vulnerabilities in Firmware

作者:Yaniv David, Nimrod Partush, Eran Yahav

单位:Technion, Israel

出处:ACM ASPLOS 2018

原文:https://dl.acm.org/citation.cfm?doid=3173162.3177157

Overview

对于两个片段代码片段,即使有语法上的差别,其中的局部代码还是有很多相同的语义。从语义上讲,两个完整的函数不可能完全一致,但是肯定有很高的相似性,问题的难点正是在于,在不同的指令选择,指令顺序,寄存器使用下,如何挖掘这种相似性。
为了能把不同编译选项编译好的二进制文件拿来比较,将其中的函数进行基本块级别的拆分,然后将基本块进一步切片成更小的片段,再将这种片段中的寄存器名和地址偏移一致化,以函数为单位制成一张表。以这两个表中相同的代码片段的数量作为相似度。
单纯用函数大小来统一化相似性分数会产生误差,因为函数大小的受制因素很多。此外,如果匹配行为的目标是整个binary,则会因为一些编译选项会丢失一部分源码的缘故,产生局部的不匹配,而这种不匹配会产生连锁反应。使用往复博弈的方法来更好的完成局部匹配的任务。

对固件Binary的处理

来自不同架构的可执行文件需要lift成一种通用的形式,作者使用Angr及其使用的封装的Valgrind作为工具链,利用Angr将代码lift成VEX-IR。除了翻译成中间语言还需要基本块的信息,基本块的信息来自于IDA Pro的分析结果。
对可执行文件的处理会有几种特殊情况:
– ELF文件格式有可能是有问题的
– 在MIPS中,有一种延迟分支槽的机制
– lift工具有的时候不能准确地将基本块和函数对应起来

作者也进行了CFG正确性,ELF文件text代码覆盖度的检查,排除弥补工具的纰漏。他们发现的工具问题及对应的改进,基本上都被工具作者们采纳了。

函数切分

对函数的区分,以CFG的基本块(BB)为基准。算法如下,输入为基本块的代码,输出为Strand
alg.1

Strand的优化与归一

  • 清除偏移
    清楚了静态全局变量和跳转地址这一类的偏移。不删除栈上和结构体的偏移,因为他们和语义有关
  • 寄存器折叠
    写之前被读的寄存器认为是作为函数的参数出现,最后被计算的是返回值
  • 编译器优化
    把VEX-IR转成LLVM-IR,再对LLVM-IR进行优化,优化的操作包括:表达式简化、常量折叠、指令合并、通用子表达式清除,无效代码清除
  • 变量名归一
    变量名是将变量按顺序进行重命名
    p进行所有操作完成后,得到的所有strand用Strand(p)表示

    相似度即为函数q与t的Strand(t)与Strand(q)的交集的元素个数

    Back-and-Forth博弈算法

    以函数为中心的比较的不足

    以函数为中心的比较方法很容易找到某一个函数在目标可执行文件中的最佳匹配,但是这个最佳匹配可能不是正确的匹配,这样的话相当于这个函数会占用掉一个比它更合适的匹配

    博弈算法

    alg.2 博弈是双方的博弈,目标binary(T)和查询binary(Q)(分析者自己编译的)中的函数集合分别作为双方的“牌”,首先由查询方给出查询binary中要查询的一个函数Qa,然后给出对方集合中和它相似度最高的函数Ta;另一方要检查,在对方集合Q中,对方给出的己方Ta在对方函数Q中最相似的Qb,如果Qb就是Qa,那么就认为Qa和Ta是相似的。

    Evaluation

    制作语料集

    从5000个多个品牌的固件中只有2000多有可以用的可执行文件。
    最后得到了200000左右个Binary,每个binary大概有200个函数,总共有40000000个左右。
    主要使用广泛流传的软件的CVE,这些CVE都是最新版本,使用gcc 5.2,默认编译选项。包含了各种漏洞类型。

实验即从固件中,匹配CVE报告中有漏洞的函数。

在固件中发掘CVE

table2
如表所示,共发现了373处漏洞,其中147个存在于最新版的固件。值得一提的有,第6行的假阳性来自于我们使用的1.15版本的wget,wget在1.12版本后的实现非常不同。 第三行中的curl_easy_unescape,这个函数在06年就被deprecate了,但是固件是14年发行的。

和以前的工作比较准确度

固件分为两个大类,一种有符号,另一种没有符号(stripped) fig6
由于Bindiff有根据函数名解析的机制,而又不能明显地找到设置的位置来关闭,所以Bindiff的实验中,只使用没有stripped的固件。从图来看,Bindiff假阳性的问题很严重。
fig8
GitZ是用于发现函数的来源的,它获取一个函数集合,和查询函数,给出一个相似度降序的函数列表。本次实验使用可执行文件的所有函数作为集合、一个查询函数作为查询函数,作为输入,以列表首项为匹配结果。
fig9
博弈算法的效果如上图,纵向地比,如果不用博弈算法,准确度要从90.11%下降到67.3%。和同为使用strand作为比较算法的GitZ相比,可以认为GitZ列表的前N项中含有真正匹配和多轮博弈类似。

总结

这是作者从变量角度对代码分片,继而进行相似性比较工作[PLDI’16]的延续。相较于之前基于统计的算法,这次使用的双方博弈的算法,为比较两个不同而静态链接相似函数可执行文件,尝试了新的思路,使得比较更加稳定。从结果来看,效果也很好。不过和[PLDI’16]一样,作者使用了没有优化过的Bindiff作为比较的依据,对于主要任务是进行区分的Bindiff,这种比较不够公平。 Evaluation中,固件来源只提到了来自网络,没提到其运行的硬件环境;也没有对不同编译参数下的纵向比较,显得不够充分。