Category Archives: symbolic execution

ZESTI论文阅读笔记

A. 彻底对敏感操作进行测试 ZESTI将程序输入替换成符号值, 并在同时记录相应的具体输入值, 在遇到分支时使用具体输入来导向程序执行流程. 在执行程序时, ZESTI会收集路径条件并用于验证潜在的错误操作. 例如, 只要程序访问符号内存地址, ZESTI就会检查对于所有满足当前路径条件的输入而言, 该操作是否安全. 1: int v[100]; 2: void f ( int x) { 3: if (x > 99) 4: x = 99; 5: v[x] = 0; 6 : } 上例代码存在bug: 当输入的x是负数时是可以访问非法内存的. 测试套件可以使用不同的参数调用此函数并验证函数行为, … Continue reading

Posted in papers, symbolic execution | Leave a comment

KLEE中Seed模式流程解析

main.cpp cl::list<std::string> SeedOutFile(“seed-out”); cl::list<std::string> SeedOutDir(“seed-out-dir”); 在main.cpp中首先会对ReplayKTestDir和ReplayKTestFile做判断. 如果用户有指定, 那么会继续判断SeedOutDir和SeedOutFile是否为空. if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) { assert(SeedOutFile.empty()); assert(SeedOutDir.empty()); … // replay ktest 文件模式 } else { // 没有指定replay ktest模式 // 直接从SeedOutFile读取seed for(){ KTest *out = kTest_fromFile(it->c_str()); } seeds.push_back(out); } 最终读取到的seed都保存在std::vector<KTest *> seeds中. 然后判断是否有读取到seed … Continue reading

Posted in symbolic execution | Leave a comment

KLEE中Seed模式相关选项介绍

测试使用的命令为: klee -seed-out=./klee-out-0/test000002.ktest -only-seed -only-replay-seeds get_sign.bc 测试结果: varas@varas-virtual-machine:~/Downloads/klee/examples/get_sign$ klee -seed-out=./klee-out-0/test000002.ktest -only-seed -only-replay-seeds get_sign.bc KLEE: output directory is “/home/varas/Downloads/klee/examples/get_sign/klee-out-6” KLEE: Using STP solver backend KLEE: KLEE: using 1 seeds KLEE: seeding done (0 states remain) KLEE: done: total instructions = 21 … Continue reading

Posted in symbolic execution | Leave a comment