rwa*_*ace 18 verification code-analysis llvm klee
http://klee.llvm.org/是一个程序分析工具,它通过符号执行和约束求解来工作,找到可能导致程序崩溃的输入,并将这些输出作为测试用例输出.这是一个非常令人印象深刻的工程,到目前为止已经产生了一些好的结果,包括在Unix实用程序的开源实现集合中发现了许多错误,这些错误被认为是有史以来最全面测试的软件之一.
我的问题是:它不做什么？
当然,任何这样的工具都有固有的限制,它无法读取用户的想法并猜测输出应该是什么.但抛开原则上是不可能的,大多数项目似乎还没有使用Klee; 当前版本的限制是什么,它还没有处理哪种类型的错误和工作负载？
osg*_*sgx 20
正如我在阅读http://llvm.org/pubs/2008-12-OSDI-KLEE.html后所说
它无法检查大程序的所有可能路径.即使在sort效用方面也失败了.问题是暂停问题(Undecidable problem),KLEE是一种启发式算法,因此它能够在有限的时间内只检查一些路径.
据文章称,它无法快速工作,需要89小时才能在COREUTILS中生成141000行代码的测试(其中使用了libc代码).最大的单个程序只有~10000行.
它对浮点,longjmp/setjmp,threads,asm一无所知; 可变大小的内存对象.
更新:/来自llvm blog/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跟踪符号存储器的所有使用.
Jun*_*xzm 10
总的来说,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;可变大小的内存对象"只是工程工作.例如,http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf).第三,KLEE不一定需要对程序进行检测以标记符号变量.如上所述,符号值可以通过命令行输入程序.实际上,用户还可以将文件指定为符号.如果需要,用户可以简单地检测库函数以使输入符号化(一劳永逸).