数据集概述
该数据集包含Intel TDX模块（版本1.5.05）的源代码、验证工具集、衍生验证任务及任务生成脚本与工具，支持基于不同初始化策略生成验证任务，适用于Intel TDX模块的安全性与可达性验证研究。
文件详解
- 核心目录结构：
- intel-tdx/src/: Intel TDX模块源代码（版本1.5.05）
- intel-tdx/formal/: 验证工具集文件
- default-size/、default-size-eager-init/: 衍生验证任务目录，包含不同初始化策略的子目录
- scripts/、harnessforge/: 任务生成脚本与工具
- 验证任务文件：
- *.i: HarnessForge生成的单文件验证任务
- 任务定义YAML文件：包含验证任务的预期结果（true表示安全任务后置条件成立；false表示可达性标签可到达）
- 配置文件：
- formal/config/目录下的YAML配置文件，用于定义验证任务生成参数
适用场景
- Intel TDX模块安全性验证：基于不同初始化策略测试模块接口函数的安全属性
- 形式化验证工具性能评估：对比不同验证工具对TDX模块任务的处理效果
- 验证任务生成方法研究：分析配置参数对任务生成结果的影响
- 可信执行环境（TEE）技术研究：支持TDX模块相关的可信计算学术研究与工程实践
