验证处理器的安全性，已成为现代电子系统设计中必不可少的一步。用户希望确保他们的消费类设备不会被黑客入侵，并且他们的个人和财务数据在云端是安全的。有效的安全验证涉及处理器硬件和运行在其上的多层软件。
本文讨论了一些与硬件安全验证相关的挑战，并提出了一种基于形式的方法来提供解决方案。实现RISC-V流行指令集架构(ISA)的设计示例，展示了这种方法的强大功能。
对处理器进行全面有效的验证，是电子开发人员面临的最大挑战之一。从处理器从成堆的标准器件转向定制芯片的那一刻起，功能验证就变得至关重要。为修复遗漏的错误而进行再制造会耗费巨大的成本，现场更换有缺陷的设备也非常耗时耗力。业界为硅前功能验证开发了复杂的工具和方法，重点团队与芯片设计人员也相辅相成。
随着处理器芯片进入安全关键型应用，另一个问题出现了：功能安全。即使是100%正确的芯片，也存在因环境条件、α粒子命中和硅片老化效应而出现错误行为的风险。如果此类故障影响到植入式医疗设备、武器系统、核电站或自动驾驶汽车，则可能会导致丧生。业界出现了一整套安全验证规则，以确保在安全受到威胁之前检测到故障并采取适当的响应。
今天，第三个问题又出现了——硬件安全的重要性。在此讨论的背景中，安全意味着使恶意代理无法访问电子系统而获取私人数据或控制其操作。每个需要功能安全的应用也需要安全性，显然，产品设计人员必须确保心脏起搏器、军用设备和自动驾驶汽车不会被坏人接管而造成伤害。
许多其他应用也必须做到安全，这样机密数据才不会被窃取或修改。网络犯罪经济估计至少达到1.5万亿美元。当然，银行和其他金融机构必然受到保护，但有价值的个人数据存在于遍布全球的无数系统中。即使只能通过系统漏洞获取少量个人数据，身份盗窃也可能会造成高昂代价并对个人造成毁灭性打击。
传统上，安全被认为是一种软件问题，重点是操作系统中的密码和特权模式等技术。但是，诸如Meltdown和Spectre等广为人知的漏洞表明，硬件(处理器本身)也存在风险。对处理器进行严格的安全验证，是许多应用的迫切需求。不幸的是，目前还没有针对处理器的成熟、全面和一致的安全验证方法。
有一种既定方法可用于评估包括处理器在内的知识产权(IP)设计中的漏洞。第一步是在寄存器传输级(RTL)设计中识别每项资产，即在IP中所使用、生产或保护的任何有价值或重要的东西。为了确定必须保护这些资产免受谁的攻击，下一步是确定可能试图破坏这些资产的对手和可能的攻击面，即可以应用威胁的访问点集。
最后一步是确定必须对资产针对来自哪些对手的哪些攻击验证哪些内容。这包括识别每项资产的所有权以及资产的机密性、完整性和可用性(CIA)目标。这个过程提供了一种系统的方法来解决理论上无限的负面行为和后果空间，并识别处理器设计中的漏洞。
美国国家标准与技术研究院(NIST)通过定义通用漏洞评分系统()对已发现漏洞的严重性进行定量评估，进一步规范了流程。如图1所示，CVSS v3.1规范定义了三个度量组：基本、时间和环境。在本文的范围内，只需要考虑基本组——它代表了随着时间的推移和跨用户环境而保持不变的漏洞的内在特性。提供了漏洞的总分。
图1：CVSS规范提供了对漏洞严重性的定量评估。(图片来源：NIST)
长期以来，形式化技术在功能验证中发挥着重要作用，并且近年来变得必不可少。没有任何软件仿真测试平台和测试集，甚至在线硬件仿真运行生产代码，能够保证没有错误。我们始终能遇到一些潜伏的设计错误从未被触发或者其影响从未被检测到的情况。基于软件仿真的方法本质上是概率性的，它们只能探索很小一部分可能的设计行为。
形式验证由于其详尽的性质而有根本上的不同。属性的形式证明能够保证任何可能的设计行为都不会违反该属性所表达的设计意图。因此，与该属性相关的设计中就不可能有错误。
指定一组鲁棒的属性并对其进行形式证明，可以达到其他方法所无法提供的确定性级别。由于处理器属于一些最大、最复杂的芯片设计，形式验证在成为整个行业的主流技术之前就已应用于其验证。
如前所述，功能安全是确定性至关重要的另一个领域。许多行业和应用的安全标准要求能够正确检测和处理大部分可能的故障。形式化安全验证是从数学上证明处理器设计符合ISO 26262等相关标准要求的唯一方法。不出所料，形式化方法也提供了唯一在数学上严谨的方法来实现安全验证的确定性。尽管功能正确性、安全性和保密性存在差异，但形式验证是所有三个领域的通用解决方案。
可以将已建立的CVSS分类方法和形式化方法的强大功能组合成一种用于验证处理器安全性的新颖方法。关键环节是定义处理器的资产并编写属性来检查这些资产是否受到任何危害。然后就可以对这些属性进行形式验证以识别任何设计错误，而一旦将它们修复，它们就证明了设计的安全性。
对于处理器，架构上可见的状态元素是资产的正确抽象级别。它们包括：
算术逻辑单元(ALU)、移位器、解码器和其他处理元件不被视为资产。它们是能够访问资产的计算元素。如果它们处于安全攻击的路径中，则最终影响将会发生在资产上，也即属性提供威胁检查的地方。
所有输入/输出(I/O)接口都被视为处理器的攻击面。从内存接口、中断引脚和调试端口读取的指令，都是对手攻击的有效位置。对于本文的分析，任何不是给定资产合法所有者的指令，都会自动被视为对手。由于对手的总数、每个时钟周期交换资产所有权的频率以及管道的并发性(管道深度的函数)，处理器安全验证尤其具有挑战性。
这种方法可用于任何处理器设计，但RISC-V ISA因其在整个电子行业的广泛采用而受到特别关注。有许多ISA实现可用作开源RTL，为任何新的验证工具或方法提供大量真实世界的测试用例。图2显示了如何使用formalISA安全分析器(可与任何商业形式验证工具一起使用)验证任何RISC-V RTL处理器设计的安全性。
图2：安全分析器执行RISC-V RTL处理器设计的形式验证。(图片来源：Axiomise)
这些属性指定了可以修改资产的合法方式，因此资产属性集的证明可保证不会出现意外结果。图3显示了Ibex RISC-V设计和标准BEQ(等分)指令的属性示例。ISA规定，将使用有效的BEQ指令对两个寄存器进行比较，如果它们相等，则将PCR值设置为使用指令中包含的偏移量所计算的新地址。CVSS指标已经过评估，属性则使用这些指标值的缩写字符串来命名。
图3：以上示例显示了具有CVSS指标的安全属性。(图片来源：Axiomise)
确定并列出要编写的安全属性，定义了一个验证计划，在概念上类似于要编写的传统软件仿真测试列表。与软件仿真测试一样，可以将安全属性的形式分析结果反向标注到计划中以显示验证进度。
图4显示了CV32E40P和zeroriscy RISC-V处理器的安全验证计划片段，其中对PCR属性进行了显示。形式化结果已包含在此表中，这表明所有属性均已通过(完整证明)，并且未发现与处理器操作(将通过处理器上运行的软件执行)相关的漏洞。
图4：安全验证计划的一个片段突出显示了CV23E40P和zeroriscy内核的PCR属性和结果。(图片来源：Axiomise)
除了PCR之外，还为该内核的其他资产编写了安全属性并进行了分析。对REG的分析，用于查找来自RISC-V所定义的R型、I型和U型的所有已实现指令。对CSR的分析，则用于六个CSR指令、同步异常和异步异常。对DMR的分析，则用于STORE指令。作为DMR评估的一部分，还确定了不会发生非法内存访问。其他属性的编写和证明，可确保非分支/跳转指令按预期使PCR增加。
该方法已应用于众多开源和专有RISC-V实现，并发现了许多与安全相关的错误。
对图3中所示属性的形式分析，揭示了Ibex内核中的错误行为：在周期5中执行BEQ指令时，由于在周期6中启动的外部调试，PCR值在周期7中被错误地更改。这将导致意外指令的执行，从而可能会执行未经授权的访问或以其他方式危及安全性。
在CV32E40P内核中也发现了一个严重的错误。非特权指令(STORE)可能会阻止对特权指令(EBREAK)的访问，从而损害完整性和可用性。CVSS 7.9的高分表明这是设计中的一个重大漏洞。图5显示了由此产生的问题，它仅在有限状态机(FSM)控制器处于解码状态时由传入的调试请求触发。该错误不会以任何其他状态出现，这使得该错误很难通过动态软件仿真捕获，因而可能导致未经形式验证的安全漏洞。
图5：CV23E40P内核中的错误与指令权限有关。(图片来源：Axiomise)
理想情况下，如果内存返回有效没有到达，则LOAD或STORE预计不会正常工作，这不是功能错误。但是，当内存返回有效受到阻塞时，并且有一个正在运行的LOAD/STORE指令，则它不应阻塞(导致死锁)特权指令的执行，尤其是链接到外部调试的特权指令，这是最高的特权指令。
图6和图7提供了安全分析器在著名的RISC-V设计中所发现的两个额外示例。
图6显示了PCR如何在WARP-V内核中受到损害。PCR未针对JAL指令正确更新。对于未对齐的跳转，必然会引发异常。必须使用目标地址而不是目标偏移量来检查字节对齐。此错误会影响此设计的多个变体：6级、4级和2级。但是，此错误的严重程度为中等，它会损害完整性，CVSS得分为5分。
图6：PCR在WARP-V内核中被破坏的方式。(图片来源：Axiomise)
图7显示了一个意外代码在zeroriscy内核中导致安全问题而未被形式验证所发现的示例。这是一种特别麻烦的错误，会影响机密性、完整性和可用性，最高CVSS得分为10。这是一种严重的缺陷，因为设计中的自定义修改覆盖了正常LOAD指令对REG-REG负载的行为，而导致常规LOAD指令无法正常工作。虽然自定义代码是意外留下的，但这很可能是在设计中故意被黑客攻击的。在任何一种情况下，都可以使用形式化方法捕获诸如此类的问题。
图7：意外代码在zeroriscy内核中导致安全问题的方式。(图片来源：Axiomise)
虽然形式验证提供确定性和证据的独特能力显然很有价值，但一些用户可能想知道执行的详尽分析是否会花费太长时间。图8应该可以消除任何此类担忧，这表明在几秒钟内就可在多个RISC-V处理器内核中发现从轻微到非常危险的问题。
图8：验证结果还概述了查找RISC-V内核问题所花费的时间。(图片来源：Axiomise)
一段时间以来，验证处理器设计的功能正确性和功能安全性一直依赖于形式化工具，现在这种方法正在扩展到安全性。本文介绍了一种使用形式化方法进行处理器安全验证的方法：
该解决方案可与任何形式化工具互操作，并自动生成可在软件仿真和硬件仿真中重用的覆盖属性。本文概述的方法还为安全性至关重要的应用提供了处理器设计(包括RISC-V)所需的严格性。
Axiomise的首席执行官兼创始人Ashish Darbari，精通形式化方法的各个方面，包括定理证明、属性检查和等价性检查。
（原文刊登于EDN美国版，参考链接：A closer look at security verification for RISC-V processors，由Franklin Zhao编译。）
本文为《电子技术设计》2023年6月刊杂志文章，版权所有，禁止转载。免费杂志订阅申请点击这里。
最前沿的电子设计资讯
