IT知识库 购物 网址 游戏 小说 歌词 快照 开发 股票 美女 新闻 笑话 | 汉字 软件 日历 阅读 下载 图书馆 编程 China
TxT小说阅读器
↓语音阅读,小说下载,古典文学↓
图片批量下载器
↓批量下载图片,美女图库↓
图片自动播放器
↓图片自动播放器↓
一键清除垃圾
↓轻轻一点,清除系统垃圾↓
vbs/VBScript DOS/BAT hta htc python perl 游戏相关 VBA 远程脚本 ColdFusion ruby专题 autoit seraphzone PowerShell linux shell Lua Golang Erlang 其它教程 CSS/HTML/Xhtml html5 CSS XML/XSLT Dreamweaver教程 经验交流 开发者乐园 Android开发资料
站长资讯 .NET新手 ASP.NET C# WinForm Silverlight WCF CLR WPF XNA VisualStudio ASP.NET-MVC .NET控件开发 EntityFramework WinRT-Metro Java C++ PHP Delphi Python Ruby C语言 Erlang Go Swift Scala R语言 Verilog 其它语言 架构设计 面向对象 设计模式 领域驱动 Html-Css JavaScript jQuery HTML5 SharePoint GIS技术 SAP OracleERP DynamicsCRM K2 BPM 信息安全 企业信息 Android开发 iOS开发 WindowsPhone WindowsMobile 其他手机 敏捷开发 项目管理 软件工程 SQLServer Oracle MySQL NoSQL 其它数据库 Windows7 WindowsServer Linux
  IT知识库 -> 信息安全 -> 实验三:klee的执行重现机制(示例分析) -> 正文阅读

[信息安全]实验三:klee的执行重现机制(示例分析)

实验三:klee的执行重现机制(示例分析) 结论性内容:
(1)如果是在程序中使用klee_make_symbolic,则可以使用下列脚本进行重现。

export LD_LIBRARY_PATH=/home/klee/xiaojiework/klee-xiaojie/build/debug/lib/:$LD_LIBRARY_PATH
gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test4.c -lkleeRuntest
KTEST_FILE=klee-last/test000015.ktest ./a.out

(2)如果是对命令行参数进行建模,即对klee进行符号执行的时候,使用 --posix-runtime选项,设定sym-args等参数,则重现只能用klee-replay,不能用(1)中的脚本。不需要链接到klee的运行库-lkleeRuntest,并且直接用gcc对代码进行编译成本地代码即可。
示例代码:

#include <stdio.h>//test.c
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include <klee/klee.h>
int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    if (result == 42)
    {
    klee_assert(0);   
    }
    return result;
}

脚本:

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

执行结果:

klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

KLEE: NOTE: Using klee-uclibc : /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca

KLEE: NOTE: Using model: /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca

KLEE: output directory is "/home/klee/kleeexperiment/modeltest/klee-out-31"

KLEE: Using STP solver backend

KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 71386000)

KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.

KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:22: ASSERTION FAIL: 0

KLEE: NOTE: now ignoring this error at this location
 

KLEE: done: total instructions = 11567

KLEE: done: completed paths = 73

KLEE: done: generated tests = 69

查看对应assertion错误的测试用例:
 
我们直接对程序输入+42,进行执行重现。

可以看到,即使是gcc test2.c -o test2(不是gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test2.c -lkleeRuntest),并且LD_LIBRARY_PATH是空的。为什么gcc能够在不链接到-lkleeRuntest的时候,对klee-assert进行解释呢?

这是因为在klee/klee.h中是这样定义的:
# define klee_assert(expr) \
((expr) \
? (void) (0) \
: __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \
所以压根不需要链接到kleeRuntest运行库。
下面改用--sym-arg选项,

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --libc=uclibc --posix-runtime test2.bc --sym-arg 3



可以看到,和使用--sym-args生成了同样的测试用例。即+42,我们可以直接在命令行使用./test2 +42进行执行重现。
但是,在实际的实验进程中(由于反复试验,求解每次随机返回一个解),我还生成了另外内容的测试用例,同样覆盖assertion错误。内容如下:
 
对于这个测试用例,内容是\x0b42,实际上就是三个字符,第一个是垂直制表符号,第二个是字符'4',第三个是字符'2'。第一个无法直接通过命令行输入,所以我们使用klee的重现机制。
我们同时搜集的还有内容是‘42\x00\x00’的测试用例,连同之前的两个测试用例,三个测试用例都放在了generatedtests目录下:
使用脚本:

均没有任何assertion fail的反应。但是使用klee-repaly的时候,

三个测试输入依次是:
垂直字表符,42(垂直字表符,我们从键盘是敲不出来的)
42
+42
所以,对命令行建模的时候,需要用klee-replay的机制。
我们采取在程序中使用klee_make_symbolic的方式,再分析一下klee执行重现机制。
代码:

int main() { //test4.c
    int argc=2;
    int size=4;
    char argv[size];
    klee_make_symbolic(argv, sizeof argv, "argv");
    argv[3]='\0';
    int result = argc > 1 ? atoi(argv) : 0;
    if (result == 42)
    {
    klee_assert(0);   
   //printf("yes");
    }
    return result;
}

由于不需要对命令行参数进行建模,我们使用如下脚本:
clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test4.c
klee --optimize --libc=uclibc test4.bc --sym-args 0 1 3
去除了--posix-runtime选项,因为不需要对命令行参数进行建模。需要保留--libc=uclibc选项,因为还要对atoi函数进行建模和处理。
 

下一步使用klee的重现机制。我们看到,可以使用KTEST_FILE的方式。
 

再试试klee-replay,结果显示:
 

由于test4.c中有klee_make_symbolic的语句,导致我们必须链接到lkleeRuntest才能执行重现。我们手动去掉这个语句,再编译成本地可执行代码,不链接到kleeRuntest运行库,即直接使用gcc -o test4 test4.c。结果仍然报错。
 

分析完毕!klee-replay和KTestFile指定文件各有应用场景,正如随笔一开始所给出的结论性内容。
上一篇文章      下一篇文章      查看所有文章
加:2017-05-13 23:21:20  更:2017-05-16 17:13:22 
 
  信息安全 最新文章
基于MD5的增强型摘要算法
【原创】【小程序开发教程】2、小程序域名配
秒懂VPN与网络代理(Proxy)的关系
渗透之信息收集
HTTP协议详解
UBER公司5700万用户信息泄露我们学到什么
SSL证书生成流程
也许,这样理解HTTPS更容易
SSL编程(2).NET最简单的客户端
Bugku
技术频道: 站长资讯 .NET新手区 ASP.NET C# WinForm Silverlight WCF CLR WPF XNA Visual Studio ASP.NET MVC .NET控件开发 Entity Framework WinRT/Metro Java C++ PHP Delphi Python Ruby C语言 Erlang Go Swift Scala R语言 Verilog 其它语言 架构设计 面向对象 设计模式 领域驱动设计 Html/Css JavaScript jQuery HTML5 SharePoint GIS技术 SAP Oracle ERP Dynamics CRM K2 BPM 信息安全 企业信息化其他 Android开发 iOS开发 Windows Phone Windows Mobile 其他手机开发 敏捷开发 项目与团队管理 软件工程其他 SQL Server Oracle MySQL NoSQL 其它数据库 Windows 7 Windows Server Linux
脚本语言: vbs/VBScript DOS/BAT hta htc python perl 游戏相关 VBA 远程脚本 ColdFusion ruby专题 autoit seraphzone PowerShell linux shell Lua Golang Erlang 其它教程
网站开发: CSS/HTML/Xhtml html5 CSS XML/XSLT Dreamweaver教程 经验交流 开发者乐园 Android开发资料
360图书馆 软件开发资料 文字转语音 购物精选 软件下载 新闻资讯 小游戏 Chinese Culture 股票 三丰软件 开发 中国文化 网文精选 阅读网 看图 日历 万年历 2018年12日历
2018-12-10 19:45:40
多播视频美女直播
↓电视,电影,美女直播,迅雷资源↓
TxT小说阅读器
↓语音阅读,小说下载,古典文学↓
一键清除垃圾
↓轻轻一点,清除系统垃圾↓
图片批量下载器
↓批量下载图片,美女图库↓
  网站联系: qq:121756557 email:121756557@qq.com  IT知识库