优先验证高风险候选,让符号执行预算用在关键位置。
Solidity · Static Analysis · Symbolic Execution · Adaptive Budget
复杂智能合约会产生大量静态告警,逐一验证却需要高昂的时间和内存开销。本项目在 SliSE 重入检测复现流程上,加入候选风险排序与自适应预算分配:根据代码特征和告警证据,决定先验证谁、验证多少个,再由符号执行完成漏洞验证。
| 候选排序 | 预算分配 | 异常恢复 | 实验评估 |
|---|---|---|---|
| 融合局部风险模式与静态告警,优先验证高分候选 | 支持固定、启发式与学习式预算 | 块级验证发生内存异常时尝试整合约回退 | 同时记录检测覆盖、命中排名、验证开销与失败终态 |
候选块评分融合代码本身的风险信号和相关静态告警:
S(c) = S_feat(c) + S_warn(c)
- 代码特征:价值转移、低级调用、
delegatecall、外部调用后的状态写入,以及函数与合约复杂度。 - 告警证据:告警类型、影响等级、置信度和源码行号距离。
- 排序规则:按总分降序排列,再结合告警距离与稳定次序处理同分候选;局部防御模式仅作为弱抑制信号。
实现入口:priority_ranker.py。框架图中的告警评分分支对应 S_warn。
从告警数量、候选覆盖、头部得分差、分数分布及合约规模构建特征快照,为当前合约选择验证深度。
| 策略 | 预算 K | 决策依据 |
|---|---|---|
| 固定预算 | 手动指定,例如 3 / 5 / 10 | 为不同验证深度建立对照 |
| 启发式预算 | 3 / 5 / 10 | 排序明确时压缩预算,不确定或复杂样本扩大预算 |
| 学习式预算 | 3 / 10 | 从历史固定预算结果学习小预算或保守预算的选择 |
预算学习器预测验证深度,漏洞判断由符号执行阶段完成。学习式推理异常可配置为启发式回退、固定 K=10 或显式报错。
实现入口:adaptive_budget.py · 训练流水线。
按照候选排名执行 Top-K 验证,并记录首次命中位置与耗时。块级验证遇到 MemoryError 时尝试 whole-contract 回退,分别记录:
recovered |
no_hit |
failed |
|---|---|---|
| 回退后恢复命中 | 回退完成但未命中 | 回退仍无法完成 |
实现入口:SliSE.py。
以下命令在仓库根目录执行,以 Windows PowerShell 为例。
1. 创建环境并安装依赖
python -m venv .venv
.\.venv\Scripts\Activate.ps1
python -m pip install -r requirements.txt2. 检查 Solidity 编译器
solc --version当前复现流程使用 solc 0.4.23,运行器会将本机存在的 $HOME\.solc-select\artifacts\solc-0.4.23 加入分析子进程的 PATH。请先准备可用的对应版本。
3. 运行候选排序对照实验
python run_experiment.py --mode priority默认对 DB2、DB3 重入标注子集分别运行 baseline 与 Top-3 排序策略,生成实验记录、评估结果与对照报告。
完整分析依赖 Slither、Z3 和 Solidity 编译器。依赖版本见 requirements.txt;旧版分析组件在不同 Python 和操作系统环境中的兼容性需实际验证。
| 模式 | 实验内容 | 主要产物 |
|---|---|---|
priority |
Baseline 与固定 Top-K 对照,默认 K=3 | 排序对照与评估报告 |
priority-sweep |
固定预算扫描,默认 K=5、10 | 预算与效果权衡报告 |
adaptive |
启发式预算分配 | 预算特征、策略报告与异常诊断 |
learned |
构建训练表、训练预算模型并在线评估 | 模型、训练指标与学习式预算报告 |
full |
DB1、DB2、DB3 基础分析 | 各数据集原始分析结果 |
完整预算对照:按顺序运行四个阶段
学习式预算需要额外安装机器学习依赖:
python -m pip install -r requirements-ml.txt为各阶段指定同一组目录,使固定预算结果可用于后续对照与训练:
$experimentPaths = @(
'--output-root', 'experiments_runtime_fallback_full',
'--evaluation-root', 'evaluation_runtime_fallback_full',
'--report-root', 'reports_runtime_fallback_full'
)
python run_experiment.py --mode priority @experimentPaths
python run_experiment.py --mode priority-sweep --topk-list 5 10 @experimentPaths
python run_experiment.py --mode adaptive @experimentPaths
python run_experiment.py --mode learned @experimentPathspriority-sweep 需要已有 baseline 实验和评估结果;learned 需要固定预算记录及自适应实验数据。默认情况下,前两个模式使用 experiments、evaluation、reports,后两个使用带 _runtime_fallback_full 的目录,因此连续复现时应显式对齐路径。
单合约、批量分析与断点续跑
单合约分析,将路径替换为实际 Solidity 文件:
python run_slise.py -s path/to/contract.sol -vt reentrancy目录批量分析:
python batch_analyze.py --input-dir Datasets/DB2/Reentrancy_label --output-dir tmp/DB2全量流程小规模试跑,每个数据集最多处理 20 个文件:
python run_experiment.py --mode full --max-files-per-dataset 20完整基础分析与续跑:
python run_experiment.py --mode full --resume使用上一节定义的目录继续自适应实验:
python run_experiment.py --mode adaptive --resume @experimentPaths查看全部实验参数:
python run_experiment.py --help| 维度 | 指标 | 关注的问题 |
|---|---|---|
| 检测覆盖 | Recall | 当前评估口径下检出了多少漏洞样本? |
| 排序效果 | Recall@K、First-hit rank | 有效命中是否出现在验证序列前部? |
| 验证效率 | Time-to-first-hit、Stage-II calls | 首次命中需要多久、消耗多少验证调用? |
| 运行鲁棒性 | Fallback outcome、Runtime failure | 异常后能否恢复,失败是否被单独统计? |
按上述统一目录流程运行后,主要结果位于:
reports_runtime_fallback_full/
├── aggregate/comparison.md # 策略对照
├── aggregate/comparison_budget_tradeoff.md # 预算与效果权衡
├── adaptive/adaptive_budget_report.md # 启发式预算分析
├── adaptive/budget_feature_table.csv # 预算特征明细
├── learned/learned_budget_report.md # 学习式预算评估
└── diagnostics/db2_memoryerror_analysis.md # 内存异常诊断
结果目录在运行时生成,默认不纳入版本控制。比较结果时,应保持数据子集、验证预算、回退策略与评估口径一致,并区分训练表现与独立评估;单次耗时不能直接代表稳定加速效果。
SliSE/
├── SliSE_tool/ # 检测器、候选排序与预算策略
├── Datasets/ # DB1 / DB2 / DB3 输入数据
├── pipeline/
│ ├── evaluation/ # 结果评估与实验比较
│ ├── reporting/ # 汇总、预算与诊断报告
│ └── training/ # 训练表构建与模型训练
├── tests/ # 回归测试
├── docs/assets/ # 方法框架图
├── run_experiment.py # 统一实验入口
├── run_slise.py # 单合约分析入口
├── batch_analyze.py # 批量分析入口
├── requirements.txt # 基础分析依赖
└── requirements-ml.txt # 学习式预算依赖
开发验证
安装相应依赖后运行:
python -m unittest discover -s tests -p "test_*.py"运行器优先使用仓库内 .venv,不存在时使用当前 Python。回归检查覆盖排序、预算分配与评估等逻辑,真实数据上的符号执行仍需单独验证。
本仓库基于 SliSE 开展复现与验证调度改进。底层工具的历史说明见 SliSE Tool,当前实验入口及依赖以仓库根目录为准。
