Klee（LLVM程序分析工具）的局限性
http://klee.llvm.org/ 是一个程序分析工具，通过符号执行和约束求解来工作，找到可能导致程序崩溃的输入，并将其作为测试用例输出。这是一项极其令人印象深刻的工程，迄今为止已经产生了一些良好的结果，包括在一系列 Unix 实用程序的开源实现中发现了许多错误，这些实用程序被认为是有史以来经过最彻底测试的软件之一。
我的问题是：它不做什么？
当然，任何此类工具都有其固有的局限性，即它无法读取用户的想法并猜测输出应该是什么。但撇开原则上不可能的事情不谈，大多数项目似乎还没有使用 Klee；当前版本有哪些限制，它还不能处理哪些类型的错误和工作负载？
http://klee.llvm.org/ is a program analysis tool that works by symbolic execution and constraint solving, finding possible inputs that will cause a program to crash, and outputting these as test cases. It's an extremely impressive piece of engineering that has produced some good results so far, including finding a number of bugs in a collection of open-source implementations of Unix utilities that had been considered among some of the most thoroughly tested software ever written.
My question is: what does it not do?
Of course, any such tool has the inherent limit that it can't read the user's mind and guess what the output was supposed to be. But leaving aside the in principle impossible, most projects don't yet seem to be using Klee; what are the limitations of the current version, what sort of bugs and workloads can it as yet not handle?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
正如我在阅读 http://llvm.org/pubs/2008-12-OSDI-KLEE 后可以说的.html
无法检查大程序的所有可能路径。即使在
sort实用程序上它也失败了。这问题是一个停止问题（不可判定问题），而KLEE是一个启发式问题，因此它只能在有限的时间内检查某些路径。
它的工作速度并不快，根据论文，它需要 89 小时才能在 COREUTILS 中生成 141000 行代码的测试（其中使用了 libc 代码）。而最大的单个程序也只有~10000行。
它对浮点、longjmp/setjmp、线程、asm 一无所知；可变大小的内存对象。
更新：/来自 llvm 博客/ http://blog.llvm.org /2011/05/what-every-c-programmer-should-know_14.html
更新2：KLEE需要修改程序。 http://t1.minormatter.com/~ddunbar/klee-doxygen/overview.html
As I can say after reading a http://llvm.org/pubs/2008-12-OSDI-KLEE.html
It can't check all possible paths of big program. It failed even on
sortutility. Theproblem is a halting problem (Undecidable problem), and KLEE is a heuristic, so it is able to check only some of paths in limited time.
It can't work fast, according to paper, it needed 89-hours to generate tests for 141000 lines of code in COREUTILS (with libc code used in them). And the largest single program has only ~10000 lines.
It knows nothing about floating point, longjmp/setjmp, threads, asm; memory objects of variable size.
Update: /from llvm blog/ http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
Update2: KLEE requieres program to be modified. http://t1.minormatter.com/~ddunbar/klee-doxygen/overview.html
总体而言，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 不一定需要对程序进行检测来标记符号变量。如上所述，符号值可以通过命令行输入到程序中。事实上，用户也可以指定文件是符号的。如果需要，用户可以简单地检测库函数以使输入符号化（一劳永逸）。
Overall, KLEE should be a pretty good symbolic execution engine for academic research. For being used in practice, it could be limited by following aspects:
[1] The memory model used by the LLVM IR interpreter in KLEE is memory-consuming and time-consuming. For each execution path, KLEE maintains a private "address space". The address space maintains a "stack" for local variables and a "heap" for global variables and dynamically allocated variables. However, each variable (local or global) is wrapped in a MemoryObject object (MemoryObject maintain metadata related to this variable, such as the starting address, size, and allocation information). The size of memory used for each variable would be the size of the original variable plus the size of MemoryObject object. When an variable is to be accessed, KLEE firstly search the "address space" to locate the corresponding MemoryObject. KLEE would check the MemoryObject and see if the access is legitimate. If so, the access will be completed and state of the MemoryObject will be updated. Such memory access is obviously slower than RAM. Such a design can easily support the propagation of symbolic values. However, this model could be simplified via learning from taint analysis (labeling the symbolic status of variables).
[2] KLEE lacks models for system environments. The only system component modeled in KLEE is a simple file system. Others, such as sockets or multi-threading, are not supported. When a program invoke system calls to these non-modeled components, KLEE either (1) terminate the execution and raises an alert or (2) redirect the call to the underlying OS (Problems: symbolic values need to be concretized and some paths would be missed; system calls from different execution paths would interfere with each other). I suppose this is the reason for "it knowing nothing threads" as mentioned above.
[3] KLEE cannot directly work on binaries. KLEE requires LLVM IR of a to-be-tested program. While other Symbolic Execution tools, such as S2E and VINE from the BitBlaze project can work on binaries. An interesting thing is the S2E project relies on KLEE as its symbolic execution engine.
Regarding the above answer, I personally have different opinions. First, it's true that KLEE cannot perfectly work with large-scope programs, but which symbolic execution tool can? Path explosion is more a theoretical open problem instead of an engineering problem. Second, as I mentioned, KLEE might run slowly due to its memory model. However, KLEE does not slow down the execution for nothing. It conservatively checks memory corruptions (such as buffer overflow) and will log a set of useful information for each executed path (such as constraints on the inputs to follow a path). In addition, I did not know other symbolic execution tools that can run super fast. Third, "floating point, longjmp/setjmp, threads, asm; memory objects of variable size" are just engineering works. For example, the author of KLEE actually did something to enable KLEE to support floating point (http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf). Third, KLEE does not necessarily require instrumentation over the program to label symbolic variables. As mentioned above, symbolic values can be feed into the program via command lines. In fact, users can also specify files to be symbolic. If required, users can simply instrument the library functions to make inputs symbolic (once for all).
我对 Klee 感到失望，因为它没有任何内置数据数据结构支持。 Klee本身并不理解什么是链表。您不能使用它来验证任何图算法的实现。此外，它无法帮助捕获整数溢出错误，而整数溢出错误是安全补丁的最重要来源。
I'm disappointed by Klee that it doesn't have any builtin data data structure support. Klee itself doesn't understand what a linked list is. You cannot use it to verify any graph algorithm's implementation. Also, it cannot help catch interger overflow errors which is the most significant source of security patches.