第三章SPV 安全路径验证

概述

安全路径验证App 验证 SoC 中的安全属性，确保敏感信息不会泄露到非安全域，或非安全主体无法访问安全资源。

Key Concepts

SPV 通用流程

1. 定义安全属性（哪些路径不应该连通）
2. 检查属性一致性（Consistency）
3. 创建抽象（Abstraction）简化模型
4. 证明 SPV 属性

SPV Key Commands

# 创建 SPV 属性：信息不能从 secure_src 流向 nonsecure_dst
spv_property -source secure_signal -destination nonsecure_signal -unreachable

Use Models

Slave Access

验证只有授权的 master 能访问特定 slave 寄存器。

TrustZone Slave

验证 ARM TrustZone 安全状态下，非安全 master 不能访问安全 slave。

Secure Subsystem

验证安全子系统内部信息不会泄露到非安全域。

Fault Tolerance

验证在故障注入情况下安全属性仍然成立。

GUI 功能

Generating Properties

# 从 GUI 自动生成 SPV 属性
# 选择 source 和 destination 信号，自动生成不可达属性

Checking Consistency

# 检查 SPV 属性之间是否存在矛盾
check_spv_consistency

Creating Abstractions

对于大型 SoC，可以创建抽象简化证明：

# 将模块抽象化
spv_abstraction -module complex_module -abstract

SPV 安全路径验证界面

安全路径验证方法论

信息流安全的核心思想

SPV 验证的不是"值对不对"（那是 FPV 的事），而是"信息会不会泄露"。这是完全不同的验证维度：即使密钥值从不直接出现在输出端，如果密钥的值影响了输出的时序或模式，信息就已经泄露了。

SPV 使用信息流分析（Information Flow Analysis）追踪从 -from 信号到 -to 信号的所有因果路径，证明在 -to_precond 条件下不存在这样的路径。

建模思路

• -from：安全信息源（密钥、安全寄存器、特权模式数据）
• -to：不可信目的地（非安全总线、调试端口、外部可见引脚）
• -to_precond：泄露的前提条件（如"非安全状态"、"调试模式打开"）

stopat 命令将密钥信号设为自由变量——形式引擎会尝试密钥的所有可能值，验证无论密钥是什么，在条件满足时都不会影响 -to 信号。

四种 Use Model 对比