RISC-V处理器的安全验证

处理器的安全性验证已经成为现代电子系统设计过程中的重要一环。用户希望确保他们的消费设备不会被黑客入侵，并且个人信息和财务数据在云中也是安全的。有效的安全性验证涉及处理器硬件和在上面运行的多层软件。

如何对处理器进行全面有效的验证，是开发人员面临的最大挑战之一。自从处理器从成堆的标准部件转向定制芯片的那一刻起，功能性验证就变得至关重要。修复漏洞缺陷所需的重新制造成本是令人望而生畏的，而现场更换缺陷设备的前景更令人担忧。为了流片前的功能性验证，业界开发了许多复杂的工具和方法，而专业验证团队则可弥补芯片设计人员的不足。

随着处理器芯片进入安全关键应用领域，另一只鞋子已经落下：即功能性安全。即使是百分之百正确设计的芯片，也会由于环境条件、α粒子撞击和硅老化效应而存在不当行为的风险。如果这种故障影响到所植入的医疗设备、武器系统、核电站或自动驾驶汽车，甚至可能会伤害到生命。业界因此推出了一整套安全性验证规程，用以确保在安全受到威胁之前，能够检测出故障并采取适当的应对措施。

今天，随着硬件安全重要性越来越突出，第三只鞋正在落下——也许三条腿的凳子是更好的比喻。本文中的安全性意思是恶意代理无法访问电子系统，来获取私人数据或控制其操作。每个要求功能安全性的应用本身也需要安全；显然，产品设计者必须确保起搏器、军事装备和自动驾驶汽车不会被意图制造伤害的人操控。

许多附加应用也必须是安全的，这样机密数据就不会被窃取或篡改。据估计，全球网络犯罪经济规模至少为1.5万亿美元。当然，银行和其他金融机构必须受到保护，但世界各地成千上万的系统中，都存在着宝贵的个人数据，即使只有少数个人数据因系统漏洞被窃取，这种身份窃取行为也会造成巨大的损失和个人灾难。

之前，安全性一直被认为是软件问题，人们经常把重点放在操作系统中的密码和授权模式等技术上。但Meltdown和Spectre等广为人知的漏洞表明，像处理器自身及其他硬件也存在风险。对处理器进行严格的安全性验证是许多应用的迫切需要。遗憾的是，目前在处理器方面还没有成熟、全面和一致的安全性验证方法。

评估知识产权(IP)设计(包括处理器)中的漏洞有一种既定的方法。名列前茅步是在寄存器转移级(RTL)设计中识别每个资产，即IP中使用、生产或保护的任何有价值或重要的东西。确定这些资产必须保护的对象，下一步是识别可能试图破坏这些资产的黑客以及可能的攻击面，即可能受到威胁的一组接入点。

最后一步是确定对这些资产应该验证什么、这些资产会受到哪些黑客的何种攻击，包括确定每个资产的所有权以及资产的机密性、完整性和可用性(CIA)目标。这一过程提供了一种系统方法，来应对理论上无限的负面行为和后果空间，并识别处理器设计中的漏洞。

通过定义通用漏洞评分系统(CVSS)，美国国家标准与技术研究所(NIST)对所发现漏洞的严重程度进行定量评估，从而为上述过程进一步确定了顺序。如图1所示，CVSS v3.1规范定义了三个度量组：基本组、临时组和环境组。就本文内容而言，只需要考虑基本组，该组描述了不会随时间和用户环境变化而改变的漏洞内在特性。CVSS计算器用于提供漏洞的总体得分。

图1：CVSS规范提供了对漏洞严重性的定量评估。来源：NIST

长期以来，形式技术在功能验证中发挥着重要作用，近年来已成为必不可少的技术。任何模拟测试台和测试集、甚至是运行生产代码的电路仿真，都不能保证没有缺陷(bug)。总是有这样的可能性，即一些潜在的设计错误从未被触发、或者其影响从未被检测到。仿真本质上是基于概率的，只能探索很小一部分的可能设计行为。

形式验证则因其详尽的性质而有本质的区别。一种属性的形式验证，可确保没有任何设计行为会违反该属性所表达的设计意图，因此与该属性相关的设计中，就不可能存在任何缺陷。

规定一组健壮的属性，并对其进行形式化验证，可以达到其他方法无法提供的确定程度。由于处理器是最大和最复杂的芯片设计，形式验证在成为整个行业的主流技术之前，就已经成功应用于处理器的验证了。

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

可以将成熟的CVSS分类方法和强大的形式化方法结合起来，形成一种新的处理器安全验证方法。关键环节是定义处理器的资产，并编写用于检查这些资产是否受损的属性。然后通过对这些属性的形式验证，识别任何可能的设计缺陷；一旦这些缺陷得到修复，它们就能证明设计的安全性。

对处理器来说，架构上可见的状态元素正是这些资产的合理抽象。其中包括：

·程序计数器(PCR)

·寄存器文件(REG)

·控制状态寄存器(CSR)

·数据存储器(DMR)

算术逻辑单元(ALU)、移位器、解码器和其他处理单元不被视为资产。这些是允许访问资产的计算单元。如果他们处于遭受安全攻击的路径上，最终影响的将是资产，而这也正是检查是否违背属性的地方。

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

这种方法可用于任何处理器设计，但RISC-V ISA尤其令人感兴趣，因为它在整个电子工业中得到了广泛应用。ISA有许多可作为开源RTL使用的实现，并为任何新的验证工具或方法提供了大量真实世界的测试用例。图2显示了如何使用formalISA验证各种RISC-V RTL处理器设计的安全性。formalISA是一款可以与任何商用的形式验证工具一起使用的安全分析器。

图2：利用安全分析器对RISC-V RTL处理器设计进行形式验证。资料来源：Axiomise

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

图3：本图上方示例显示了带CVSS指标的一个安全属性。资料来源：Axiomise

确定并列出要编写的安全属性相当于定义了一个验证计划，在概念上类似于要编写的传统模拟测试列表。与仿真测试一样，安全属性的形式化分析结果可以后向标注到计划中，用以显示验证进度。

图4所示为CV32E40P和零风险RISC-V处理器的安全验证计划片段，其中就显示了PCR属性。表中包含的形式结果表明所有属性均通过了(完全验证)，并且在处理器上运行软件时，未发现与所需处理器操作相关的漏洞。

图4：安全验证计划的一部分。其中突出展示了CV23E40P和零风险内核的PCR属性和验证结果。资料来源：Axiomise

除了PCR以外，上述安全验证计划对该内核的其他资产也编写了安全属性，并进行了分析。对来自RISC-V定义的R型、I型和U型分类的所有实现指令，均进行了REG分析。对六条CSR指令、同步异常和异步异常进行了CSR分析。对STORE指令进行了DMR分析。作为评估DMR的一部分，还确认了不会发生非法内存访问。另外还编写并验证了其他属性，确保非分支/跳转指令按预期增加PCR。

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

对图3所示属性的形式分析揭示了Ibex内核中的错误行为：当在第5周期执行BEQ指令时，由于第6周期中启动了外部调试，在第7周期中PCR值会被错误篡改。这将导致意外指令的执行，进而可能会执行未经授权的访问或其他危及安全的行为。

在CV32E40P内核中也发现了一个严重的缺陷。非特权指令(STORE)可能会阻止对特权指令(EBREAK)的访问，从而影响完整性和可用性。CVSS评分高达7.9，表明这是设计中的一个重要漏洞。图5显示了最终问题，只有当有限状态机(FSM)控制器处于DECODE状态时，传入的调试请求才会触发该问题。这个缺陷在任何其他状态下不会出现，因此动态模拟很难捕捉到这个缺陷，从而可能导致未经形式验证的安全漏洞。

图5：CV23E40P内核中的这个缺陷与指令特权有关。资料来源：Axiomise

理想情况下，如果没有获得内存返回有效信息，那么LOAD或STORE是不会正常工作的，这不算是功能性缺陷。但是，当内存返回有效被阻止、且有一个正在运行的LOAD/STORE指令时，那就不应该阻止(导致死锁)特权指令的执行，特别是链接到外部调试的指令，因为这是较高特权指令。

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

图6显示了PCR是如何在WARP-V内核中受损的。在执行JAL指令时PCR没有得到正确更新。由于错误的跳转，异常必定会发生。字节对齐检查必须使用目标地址，而不是目标偏移量。这种缺陷会影响该设计的多个变量：6级、4级和2级。不过这种缺陷的严重程度适中，会影响到完整性，CVSS得分为5分。

图6：图中显示WARP-V内核中PCR是如何受损的。资料来源：Axiomise

图7是一个意外代码的示例，这段代码会导致零风险内核中的一个安全性问题，而该问题用形式验证无法发现。这是一个特别麻烦的缺陷，会影响机密性、完整性和可用性，然而，CVSS评分较高可达10分。这是一个严重的缺陷，将导致正常LOAD指令无法正常工作，原因是设计中的自定义修改利用REG-REG加载指令覆盖了正常LOAD指令的行为。尽管这段自定义代码是意外留下的，但设计很可能受到了黑客的故意入侵。不过在任何一种情况下，都可以使用形式方法来解决此类问题。