如何为测试Linux内核函数btrfs_map_block搭建KLEE环境

一、准备btrfs_map_block用于KLEE测试的步骤 #

1. 提取目标函数与最小依赖集 #

直接从目标内核版本的fs/btrfs/volumes.c中复制btrfs_map_block函数代码，然后梳理它直接依赖的核心元素：

• 结构体：仅保留函数用到的字段，比如struct btrfs_fs_info、struct btrfs_bio、struct btrfs_chunk，删除无关成员
• 宏定义：从内核头文件提取BTRFS_MAX_MIRRORS、BTRFS_CHUNK_ITEM_KEY这类必要宏
• 辅助函数：优先复制无复杂依赖的小函数（如btrfs_calc_block_group_type），复杂依赖函数留到下一步做桩

2. 编写依赖桩函数 #

对于依赖内核子系统（内存管理、文件树操作等）的复杂函数，编写桩函数模拟核心行为：

• 内存分配函数：比如kmalloc，返回符号化内存块供KLEE分析
• 树查询函数：比如btrfs_lookup_chunk，返回预设或符号化的struct btrfs_chunk实例，可针对性构造CVE-2019-19816的触发场景（如chunk长度为0）
• 链表迭代：简化list_for_each_entry这类宏为基础循环，避免依赖内核链表实现

示例桩函数：

// 模拟kmalloc，返回符号化内存
void *kmalloc(size_t size, unsigned int flags) {
    void *buf = malloc(size);
    klee_make_symbolic(buf, size, "kmalloc_buf");
    return buf;
}

// 模拟chunk查询，返回符号化chunk结构
int btrfs_lookup_chunk(struct btrfs_fs_info *fs_info, u64 logical, struct btrfs_chunk **out_chunk) {
    *out_chunk = malloc(sizeof(struct btrfs_chunk));
    klee_make_symbolic(*out_chunk, sizeof(struct btrfs_chunk), "target_chunk");
    // 可手动设置触发漏洞的字段，比如chunk->length = 0
    return 0;
}

3. 编写测试驱动程序 #

构造包含符号化输入的main函数，覆盖CVE-2019-19816的漏洞场景：

• 初始化符号化的struct btrfs_fs_info、struct btrfs_bio等结构体字段
• 调用btrfs_map_block函数
• 添加断言检查结果（比如断言返回值合法、无内存越界、未触发除以0等漏洞行为）

示例驱动框架：

#include <klee/klee.h>
#include <assert.h>

// 提取的内核类型定义
typedef unsigned long long u64;
typedef unsigned int u32;

// 简化的btrfs结构体
struct btrfs_fs_info {
    u64 sectorsize;
    struct btrfs_root *chunk_root; // 仅保留必要指针
};

struct btrfs_bio {
    u64 logical;
    u32 nr_pages;
};

// 引入桩函数、目标函数...

int main() {
    struct btrfs_fs_info fs_info;
    struct btrfs_bio bio;
    struct btrfs_map_token token;

    // 符号化输入参数
    klee_make_symbolic(&fs_info.sectorsize, sizeof(fs_info.sectorsize), "sectorsize");
    klee_make_symbolic(&bio.logical, sizeof(bio.logical), "logical_block");
    klee_make_symbolic(&bio.nr_pages, sizeof(bio.nr_pages), "nr_pages");

    // 调用目标函数
    int ret = btrfs_map_block(&fs_info, &bio, 1, &token);

    // 针对CVE-2019-19816的断言：避免除以0或溢出
    assert(ret != -EINVAL);
    // 可添加更多针对漏洞场景的断言

    return 0;
}

4. 清理内核编译属性 #

删除目标函数中的内核特定属性（如__init、__always_inline、__cold），或通过宏定义清空：

#define __init
#define __always_inline inline
#define __cold

二、确保测试时正确引入Linux头文件的方法 #

1. 提取内核头文件的必要片段 #

不要直接使用系统默认的Linux头文件，从目标内核版本的源码树中提取核心内容：

• 类型定义：从include/linux/types.h复制u64、u32、loff_t等typedef
• BTRFS专属定义：从include/linux/btrfs.h、include/linux/btrfs_tree.h复制struct btrfs_chunk、BTRFS_CHUNK_ITEM_KEY等相关内容
• 仅保留测试需要的部分，避免引入无关依赖导致编译错误

2. 定义内核特有的宏与编译选项 #

在测试代码开头添加必要的宏定义，适配内核GNU C扩展：

#define __KERNEL__
#define CONFIG_BTRFS_FS
#define __LE64_TYPE __u64
#define __le64 __attribute__((__packed__)) __LE64_TYPE

编译时使用KLEE的GNU C标准：

klee --cxx --std=gnu11 --include-path ./extracted_kernel_headers test_btrfs_map_block.c

3. 调整头文件包含顺序 #

遵循内核头文件的包含优先级：

// 先包含基础类型头文件
#include "extracted_types.h"
// 再包含BTRFS相关头文件
#include "extracted_btrfs.h"
// 最后包含测试依赖和KLEE头文件
#include <klee/klee.h>

4. 处理字节序与对齐问题 #

内核中常用的__le64、__be32等字节序类型，可简化为对应无符号类型（如__le64替换为u64），或复制内核中的字节序转换宏（如le64_to_cpu）到测试代码中。

关键注意事项 #

• 匹配内核版本：必须使用CVE-2019-19816对应的内核版本源码（如Linux 5.3及之前），避免函数逻辑差异
• 聚焦漏洞场景：针对该CVE的核心问题（未检查chunk长度是否为0导致的整数溢出/除以0），在桩函数中构造对应符号化输入
• 限制KLEE资源：内核函数逻辑复杂，需调整KLEE参数（如--max-memory=1G、--max-time=3600）避免资源耗尽

内容的提问来源于stack exchange，提问作者Nabel Zaharudin