Klee 的限制(LLVM 程序分析工具)

Posted

技术标签:

【中文标题】Klee 的限制(LLVM 程序分析工具)【英文标题】:Limits of Klee (the LLVM program analysis tool) 【发布时间】:2011-08-10 04:49:20 【问题描述】:

http://klee.llvm.org/ 是一个程序分析工具,它通过符号执行和约束求解来工作,找到可能导致程序崩溃的输入,并将它们作为测试用例输出。这是一项非常令人印象深刻的工程,迄今为止已经产生了一些良好的结果,包括在 Unix 实用程序的开源实现集合中发现了许多错误,这些实用程序被认为是有史以来编写的一些经过最彻底测试的软件。

我的问题是:它做什么?

当然,任何此类工具都有其固有的限制,即它无法读取用户的想法并猜测输出应该是什么。但撇开原则上不可能的事不谈,大多数项目似乎还没有使用 Klee。当前版本的限制是什么,它还不能处理什么样的错误和工作负载?

【问题讨论】:

【参考方案1】:

正如我在阅读 http://llvm.org/pubs/2008-12-OSDI-KLEE.html 后所说的那样

它无法检查大程序的所有可能路径。它甚至在 sort 实用程序上也失败了。这 问题是一个停止问题(Undecidable problem),KLEE是一个启发式的,所以它只能在有限的时间内检查一些路径。

它不能快速工作,根据论文,它需要 89 小时才能为 CORUTILS 中的 141000 行代码生成测试(其中使用了 libc 代码)。而最大的单个程序只有 ~10000 行。

它对浮点、longjmp/setjmp、线程、asm一无所知;可变大小的内存对象。

更新:/来自 llvm 博客/http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html

5 . LLVM“Klee”子项目使用符号分析通过一段代码“尝试所有可能的路径”来查找代码中的错误并生成一个测试用例。这是一个很棒的小项目主要受限于不能在大型应用程序上运行。

Update2:KLEE 需要修改程序。 http://t1.minormatter.com/~ddunbar/klee-doxygen/overview.html

。符号内存是通过插入对 KLEE 的特殊调用(即 klee_make_symbolic)来定义的。在执行期间,KLEE 跟踪符号内存的所有使用。

【讨论】:

不知道你对“快”的定义是什么。我肯定不能在 89 小时内为 141,000 行代码编写测试代码。 (我当然可以在星期一早上 9 点打开机器,然后在星期五早上 9 点之前忽略它,如果这样会得到我无法编码的测试 :) 我的意思是,KLEE 可能需要几个月甚至更长的时间才能实现对大型项目的良好覆盖。 所以?自行车和电力很便宜。我的个人时间不是,而且我可靠地做到这一点的技能也不好。 “自行车是工程师最好的朋友”。 Klee 并不严格要求在所有情况下都修改程序。它可以将命令行参数、文件和标准输入视为其执行的符号。【参考方案2】:

总的来说,KLEE 应该是一个相当不错的学术研究符号执行引擎。在实际使用中,可能会受到以下几个方面的限制:

[1] KLEE中的LLVM IR解释器使用的内存模型是耗内存和耗时的。对于每个执行路径,KLEE 维护一个私有的“地址空间”。地址空间为局部变量维护一个“堆栈”,为全局变量和动态分配的变量维护一个“堆”。但是,每个变量(本地或全局)都包装在一个 MemoryObject 对象中(MemoryObject 维护与此变量相关的元数据,例如起始地址、大小和分配信息)。每个变量使用的内存大小将是原始变量的大小加上 MemoryObject 对象的大小。当要访问一个变量时,KLEE首先搜索“地址空间”来定位对应的MemoryObject。 KLEE 将检查 MemoryObject 并查看访问是否合法。如果是这样,访问将完成并且 MemoryObject 的状态将被更新。这样的内存访问显然比 RAM 慢。这样的设计可以很容易地支持符号值的传播。然而,这个模型可以通过学习污点分析(标记变量的符号状态)来简化。

[2] KLEE 缺乏系统环境模型。在 KLEE 中建模的唯一系统组件是一个简单的文件系统。不支持其他,例如套接字或多线程。当程序调用这些非建模组件的系统调用时,KLEE 要么(1)终止执行并引发警报,要么(2)将调用重定向到底层操作系统(问题:符号值需要具体化,并且某些路径将是错过;来自不同执行路径的系统调用会相互干扰)。我想这就是上面提到的“它对线程一无所知”的原因。

[3] KLEE 不能直接处理二进制文件。 KLEE 需要待测程序的 LLVM IR。而其他符号执行工具,例如来自 BitBlaze 项目的 S2E 和 VINE 可以在二进制文件上工作。有趣的是 S2E 项目依赖 KLEE 作为其符号执行引擎。

关于上面的回答,我个人有不同的看法。首先,KLEE 确实不能完美地处理大型程序,但是哪个符号执行工具可以呢?路径爆炸更像是一个理论上的开放问题,而不是一个工程问题。其次,正如我所提到的,KLEE 可能由于其内存模型而运行缓慢。但是,KLEE 并没有白白减慢执行速度。它保守地检查内存损坏(例如缓冲区溢出),并将为每个执行的路径记录一组有用的信息(例如对输入的约束以遵循路径)。另外,我不知道其他可以超快运行的符号执行工具。第三,“浮点、longjmp/setjmp、线程、asm;可变大小的内存对象”只是工程作品。例如,KLEE 的作者实际上做了一些事情来使 KLEE 支持浮点(http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf)。第三,KLEE 不一定需要对程序进行检测来标记符号变量。如上所述,符号值可以通过命令行输入到程序中。事实上,用户也可以将文件指定为符号。如果需要,用户可以简单地检测库函数以使输入符号化(一劳永逸)。

【讨论】:

以上是关于Klee 的限制(LLVM 程序分析工具)的主要内容,如果未能解决你的问题,请参考以下文章

实验三:klee的执行重现机制(示例分析)

XCode 5.1 单元测试覆盖分析在使用块的文件上失败

KLEE概览

LLVM 之 Clang 静态分析器篇:程序缺陷诊断——除零错误

编译器简介

LLVM 之 Clang 静态分析器篇:程序缺陷诊断——内存泄露