使用KLEE对findutils进行符号执行编译指南

符号执行是一种强大的程序分析技术，而KLEE是其中广受欢迎的工具之一。本文将详细介绍如何将findutils项目编译为KLEE可用的LLVM bitcode文件，为后续的符号执行分析做准备。

准备工作

在开始之前，需要确保系统已安装以下工具：

• wllvm (Whole Program LLVM)
• LLVM工具链
• 基本的开发工具链(autotools等)

获取findutils源代码

首先需要从官方仓库克隆findutils的最新代码：

git clone git://git.savannah.gnu.org/findutils.git
cd findutils

构建配置系统

findutils使用GNU构建系统，需要先运行bootstrap脚本生成configure文件：

./bootstrap

设置编译环境

为了生成适合KLEE分析的bitcode文件，需要配置特定的编译环境：

export CC=wllvm
export CFLAGS="-g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__"

这些标志的作用是：

• -g 保留调试信息
• -O1 使用基本优化级别
• -Xclang -disable-llvm-passes 禁用LLVM优化过程
• -D__NO_STRING_INLINES 禁用字符串内联
• -D_FORTIFY_SOURCE=0 禁用fortify安全检查
• -U__OPTIMIZE__ 取消优化定义

配置项目

运行configure脚本进行项目配置，建议禁用一些可能影响符号执行的特性：

./configure --disable-nls --disable-largefile --disable-threads --without-selinux

这些选项分别禁用了：

• 国际化支持(nls)
• 大文件支持
• 多线程支持
• SELinux支持

编译项目

使用make命令编译项目，同时跳过一些文档生成步骤：

make -j 4 MAKEINFO=true HELP2MAN=true

提取bitcode文件

编译完成后，使用wllvm提供的工具提取find程序的bitcode：

extract-bc find/find

注意事项

1. 对于较旧版本的findutils(如2007年的版本)，编译过程会更加复杂，可能需要先运行import-gnulib.sh脚本并构建旧版本的autotools工具链。

2. 旧版本可能与现代glibc存在兼容性问题，可能需要额外的兼容层或修改。

3. 如果遇到依赖问题，可能需要安装额外的开发包或调整配置选项。

通过以上步骤，我们成功将findutils编译为KLEE可分析的bitcode格式，为后续的符号执行分析奠定了坚实基础。