验证RISC-V处理器的安全性

验证处理器的安全性已成为现代电子系统设计中必不可少的步骤。用户希望确保他们的消费类设备不会被黑客入侵，并且他们的个人和财务数据在云中是安全的。有效的安全验证涉及处理器硬件和在其上运行的多层软件。

本文讨论了与硬件安全验证相关的一些挑战，并介绍了一种基于形式的方法来解决。实现流行的RISC-V指令集架构（ISA）的设计示例展示了这种方法的强大功能。

安全验证概述

对处理器进行全面有效的验证是电子开发人员面临的最大挑战之一。从处理器从成堆的标准部件转向定制芯片的那一刻起，功能验证就变得至关重要。为修复遗漏的错误而重新制造的成本令人生畏，并且在现场更换有缺陷的设备前景令人恐惧。为硅前功能验证开发了复杂的工具和方法，重点团队补充了芯片设计人员。

随着处理器芯片进入安全关键型应用，另一只鞋掉了下来：功能安全。即使是 100% 正确的芯片，也会因环境条件、α 粒子撞击和硅老化效应而面临不当行为的风险。如果这种故障影响植入式医疗设备、武器系统、核电站或自动驾驶汽车，可能会失去生命。出现了一整套安全验证学科，以确保在安全受到损害之前检测到故障并采取适当的响应。

今天，第三只鞋正在掉落——也许三条腿的凳子是一个更好的比喻——硬件安全的重要性。在此讨论的上下文中，安全性意味着恶意代理无法访问电子系统来收集私人数据或控制其操作。每个需要功能安全的应用也需要安全性;显然，产品设计师必须确保心脏起搏器、军事设备和自动驾驶汽车不会被意图造成伤害的人接管。

许多其他应用程序也必须是安全的，以便机密数据不会被盗或被修改。据估计，网络犯罪经济至少[]为1.5万亿美元。当然，银行和其他金融机构必须受到保护，但有价值的个人数据存在于遍布全球的数以千计的系统中。身份盗窃可能代价高昂且对个人造成毁灭性打击，即使只有几条个人数据可以通过系统漏洞收集。

传统上，安全性被认为是一个软件问题，重点是操作系统中的密码和特权模式等技术。但众所周知的漏洞，如[Meltdown和Spectre]已经表明，硬件 - 处理器本身 - 也存在风险。对处理器进行严格的安全验证是许多应用的迫切需要。遗憾的是，对于处理器，没有既定的、全面和一致的安全验证方法。

评估安全漏洞

评估知识产权（IP）设计（包括处理器）中的漏洞有一种既定的方法。第一步是在寄存器传输级 （RTL） 设计中确定每个资产，即在 IP 中使用、生产或保护的任何有价值或重要的资产。要确定必须保护这些资产的对象，下一步是确定可能试图破坏这些资产的对手和可能的攻击面，即可以应用威胁的访问点集。

最后一步是确定必须验证哪些资产，哪些资产来自**哪些对手的攻击。这包括确定每个资产的所有权以及资产的机密性、完整性和可用性 （[CIA] 目标。这个过程提供了一种系统的方法来解决理论上无限的负面行为和后果空间，并识别处理器设计中的漏洞。

美国国家标准与技术研究院 （NIST） 通过定义通用漏洞评分系统 （[CVSS]） 来对发现的漏洞的严重性进行定量评估，从而进一步有序地执行该过程。如图 1 所示，[CVSS v3.1]规范定义了三个指标组：基本、临时和环境。在本文的讨论范围内，仅需要考虑 Base 组，该组表示漏洞的内在品质，这些特性在一段时间内和跨用户环境中保持不变。[CVSS 计算器]提供漏洞的总体分数。

点击查看全尺寸图片*图 1：CVSS 规范提供了对漏洞严重性的定量评估。资料来源：美国国家情报研究院

正式的论据

形式化技术长期以来在功能验证中发挥着重要作用，近年来它们变得至关重要。没有仿真测试平台和测试集，甚至运行生产代码的在线仿真，都可以保证没有错误。总是有可能从未触发过一些潜伏的设计错误，或者从未检测到其影响。基于模拟的方法本质上是概率性的;他们只能探索可能的设计行为的极小百分比。

形式核查由于其详尽无遗的性质而根本不同。属性的正式证明保证任何可能的设计行为都不能违反该属性所表达的设计意图。因此，与该属性相关的设计中不可能有错误。

指定一组可靠的属性并正式证明它们可以实现其他方法无法提供的确定性级别。由于处理器是一些最大和最复杂的芯片设计，因此形式验证早在它成为整个行业的主流技术之前就已应用于其验证。

如前所述，功能安全是确定性至关重要的另一个领域。许多行业和应用的安全标准要求可以正确检测和处理大部分可能的故障。形式安全验证是从数学上证明处理器设计符合相关标准（如 ISO 26262）要求的唯一方法。不出所料，形式化方法也提供了实现安全验证确定性的唯一数学严谨方法。尽管在功能正确性、安全性和安全性方面存在差异，但形式验证是所有三个领域共有的解决方案。

处理器安全性的形式验证

CVSS分类的既定方法和形式化方法的强大功能可以组合成一种新的方法来验证处理器的安全性。关键链接是定义处理器的资产并写入检查这些资产的任何危害的属性。然后可以正式验证这些属性以识别任何设计错误，一旦这些错误得到修复，它们就会证明设计的安全性。

对于处理器，体系结构上可见的状态元素是资产的正确抽象级别。其中包括：

• 程序计数器 （PCR）* 寄存器文件 （REG）* 控制状态寄存器 （CSR）* 数据存储器

算术逻辑单元 （ALU）、移位器、解码器和其他处理元素不被视为资产。这些是允许访问资产的计算元素。如果它们处于安全攻击的路径中，则净效应将发生在资产上，这是属性提供入侵检查的地方。

所有输入/输出 （I/O） 接口都被视为处理器的攻击面。从内存接口、中断引脚和调试端口读取的指令都是攻击者攻击的有效位置。对于本文的分析，任何不是给定资产合法所有者的指令都将自动被视为对手。由于攻击者总数、与每个时钟周期交换资产所有权的频率以及管道的并发性（这是管道深度的函数），处理器安全验证尤其具有挑战性。

应用于RISC-V设计

这种方法可用于任何处理器设计，但RISC-V ISA因其在整个电子行业中的广泛采用而特别令人感兴趣。ISA 有许多实现可作为开源 RTL 使用，为任何新的验证工具或方法提供了大量实际测试用例。图 2 显示了如何使用 formalISA 验证任何 RISC-V RTL 处理器设计的安全性，[FormalISA]是一种可与任何商业形式验证工具配合使用的安全分析器。

点击查看全尺寸图像图 2：安全分析器对 RISC-V RTL 处理器设计执行形式验证。来源： 公理

属性指定可以修改资产的合法方式，因此为资产设置的属性证明保证不会发生意外结果。图 3 显示了 Ibex RISC-V 设计和标准 BEQ（如果相等则分支）指令的属性示例。ISA指定有效的BEQ指令将比较两个寄存器，如果它们相等，则将PCR值设置为使用指令中包含的偏移量计算的新地址。已评估 CVSS 指标，并使用这些指标值的缩写字符串来命名属性。

点击查看全尺寸图像*图 3：上面的示例显示了具有 CVSS 指标的安全属性。来源： 公理

确定并列出要写入的安全属性可以定义一个验证计划，在概念上类似于要编写的传统模拟测试列表。与模拟测试一样，安全属性的正式分析结果可以反向注释到计划中，以显示验证进度。

图4显示了[CV32E40P]和[零RISC-V处理器的安全验证计划片段，显示了PCR属性。此表中已包含正式结果，显示所有属性都已通过（完全证明），并且未发现与将通过处理器上运行的软件执行的处理器操作相关的漏洞。

点击查看全尺寸图像*图 4：安全验证计划的片段突出显示了 CV23E40P 和零芯的 PCR 属性和结果。来源： 公理

针对 PCR 之外的此核心的其他资产编写和分析了安全属性。分析了REG中所有由RISC-V定义的R型，I型和U型类实现的指令。分析了CSR的6条CSR指令、同步异常和异步异常。分析DMR以获取STORE指令。作为评估 DMR 的一部分，还确定不会发生非法内存访问。编写并验证了其他属性，以确保非分支/跳转指令按预期增加PCR。

在RISC-V中发现的错误示例

该方法已应用于许多开源和专有的RISC-V实现，并且已经发现了许多与安全相关的错误。

对图3所示属性的正式分析揭示了Ibex核心中的错误行为：在周期5中执行BEQ指令时，由于在周期7中启动的外部调试，PCR值在周期6中被错误地更改。这将导致执行意外指令，这些指令可能会执行未经授权的访问或以其他方式损害安全性。

在CV32E40P内核中也发现了一个严重的错误。非特权指令 （STORE） 可能会阻止对特权指令 （EBREAK） 的访问，从而损害完整性和可用性。CVSS的高分7.9表明这是设计中的一个重大漏洞。图 5 显示了由此产生的问题，仅当有限状态机 （FSM） 控制器处于 DECODE 状态时，传入的调试请求才会触发该问题。该错误不会以任何其他状态显示，这使得动态模拟难以捕获此错误，并且可能导致未经正式验证的安全漏洞。

点击查看全尺寸图像内核中的错误与指令权限有关。*来源： 公理

理想情况下，如果内存返回有效未到达，则 LOAD 或 STORE 不应正常工作，这不是功能错误。但是，当内存返回有效被阻止，并且存在正在进行的 LOAD/STORE 指令时，它不应阻止（导致死锁）特权指令的执行，尤其是链接到外部调试的指令，这是最高特权指令。

图6和图7提供了安全分析仪在众所周知的RISC-V设计中发现的两个附加示例。

图6显示了PCR在WARP-V核心中是如何受到损害的。对于日航指令，PCR 未正确更新。对于未对齐的跳跃，必须引发异常。必须使用目标地址而不是目标偏移量检查字节对齐。此错误会影响此设计的多种变体：6 阶段、4 阶段和 2 阶段。但是，此错误的严重性中等，会影响完整性并获得 CVSS 分数 5。

点击查看全尺寸图像图 6：这就是 PCR 在 WARP-V 核心中受到损害的方式。来源： 公理

图 7 显示了一个意外代码的示例，该代码导致形式验证发现的 zeroriscy 核心中的安全问题。这是一个特别麻烦的错误，影响了机密性、完整性和可用性，CVSS 的最高分数为 10。这是一个严重的缺陷，因为常规 LOAD 指令无法正常工作，因为设计中的自定义修改覆盖了 REG-REG 加载的正常 LOAD 指令的行为。尽管自定义代码是偶然留下的，但这很可能是在设计中故意被黑客入侵的。无论哪种情况，都可以使用正式方法解决此类问题。

点击查看全尺寸图像图 7：这就是意外代码在零点核心中导致安全问题的方式。来源： 公理

虽然形式验证提供确定性和证据的独特能力显然很有价值，但一些用户可能会怀疑所执行的详尽分析是否花费了太长时间。图8应该可以消除任何此类担忧，表明在几秒钟内在多个RISC-V处理器内核中发现了从轻微到非常危险的问题。

点击查看全尺寸图像 图 8：验证结果还概述了查找 RISC-V 内核问题的时间。来源： 公理

用于处理器安全验证的正式工具

一段时间以来，验证处理器设计的功能正确性和功能安全性一直依赖于正式工具，这种方法现在正在扩展到安全性。本文介绍了一种使用形式化方法进行处理器安全验证的方法，方法如下：

• 以 CIA 安全目标为指导，构建强大的处理器安全验证计划。* 使用 CVSS 评分系统计算每个漏洞的漏洞分数。* 使用抽象驱动的方法进行形式验证，以获得 100% 的证明收敛。

该解决方案可与任何正式工具互操作，并自动生成可在仿真和仿真中重复使用的覆盖属性。本文概述的方法还提供了处理器设计（包括RISC-V）所需的严谨性，这些设计用于安全性至关重要的应用。