第三章SPV 安全路径验证

概述

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

Key Concepts

SPV 通用流程

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

SPV Key Commands

# 把密钥信号设为自由变量（形式引擎可驱动任意值）
stopat otp_key custom_key

# 创建 SPV 属性：otp_key 的数据不能在 s_secure 为低时到达 s_rdata
check_spv -create \
          -from otp_key \
          -to s_rdata \
          -to_precond {~s_secure}

# 证明
check_spv -prove

# 调试失败
visualize -violation -property <embedded>::spv_prop:1 -new_window

Use Models

Slave Access

验证来自安全区域的数据，在 "protected mode" 为 0 时，绝不会传播到 CPU 的寄存器存储器：

check_spv -create -from Slave.Secure.* -to CPU.RegMem.* -to_precond CPU.Protected==0

TrustZone Slave

验证以安全方式（AWPROT[1]=0）写入 slave 的数据，绝不会以非安全方式（ARPROT[1]=1）离开该 slave。注意关注点是数据"以何种方式流出"，而非"谁能发起访问"：

check_spv -create -from WDATA -from_precond AWPROT[1]==0 -to RDATA -to_precond ARPROT[1]==1

Secure Subsystem

当 DUT 是一个同时包含安全与非安全 master 和 slave 的子系统时，本使用模型的目标是验证 ROM 中的安全数据不会泄漏到 SoC 的其余部分。做法是分别建立从 ROM 到 RAM、以及从 RAM 到密钥位置的检查：

check_spv -create -from rom_data -from_precond {rom_read && rom_addr <= 1} \
          -to mem_wdata -to_precond {mem_enable && mem_write}

check_spv -create -from mem_rdata -from_precond {mem_enable && !mem_write} -to s1_encrypt.key

Fault Tolerance

文档给出的例子：DUT 比较输入 A 和 B，若二者相同，则该值传播到 Y 且 fault=0；若不同，则 Y 被置零且 fault=1。于是要验证的是：当 A != B 时，不存在从 A、B 到 Y 的路径。

其建模手法值得注意：容错模型改变设计中的 buffer，使原有逻辑被替换为悬空网线（dangling net）。而在形式验证中悬空网线被当作输入处理，即工具可以在其上驱动任意值。因此这种情况下验证的目标是限制同一时刻可能发生的故障数量。

GUI 功能

Generating Properties

生成 SPV 属性有两条途径：使用 check_spv -create 命令，或从 GUI 操作：

1. 在 SPV Setup wizard 上点击 Create Security Path Property 按钮，打开 Create Security Path Property 对话框
2. 可选：在 Name 字段填写属性名
3. 在 From 字段填写源信号，即安全数据所在的位置

关于 -to 与 -to_all 的区别：-to 把多个目的信号视为析取（disjunctive）关系，即检查数据能否传播到其中任意一个；-to_all 视为合取（conjunctive）关系，即检查数据能否在同一时钟周期内同时传播到所有指定信号。

Checking Consistency

# 确认安全属性路径上的所有黑盒都已被成功抽象
check_spv -consistency

# 列出所有抽象的名称与 connection specs
check_spv -list connection_specs

Creating Abstractions

SPV 抽象的作用是建立结构连接以允许数据传播，用来避免黑盒造成的假阳性（false positive）。工具会在一组输入和一组输出之间、或针对指定实例/黑盒实例建立连接：

# 抽象指定实例
check_spv -abstract -instances instance_tcl_list -mode mode

# 指定构成抽象起止边界的信号
check_spv -abstract -inputs input_tcl_list -outputs output_tcl_list -mode mode

# 抽象所有在 elaborate 阶段被黑盒化的实例
check_spv -abstract -bbox_instances -mode mode

SPV 安全路径验证界面

安全路径验证方法论

信息流安全的核心思想

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

SPV 的实现机制是污点标记（taint）：证明一条 SPV 属性时，形式引擎会在源信号上注入一个唯一的标记（tag），称为 "taint"，然后检查这个标记能否出现在目的信号上。如果属性失败，反例会展示来自源端的 "tainted" 数据是如何到达目的端的。

建模思路

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

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

四种 Use Model 对比