驗證處理器的安全性已成為現代電子系統設計中必不可少的步驟。用戶希望確保他們的消費類設備不會被黑客入侵，并且他們的個人和財務數據在云中是安全的。有效的安全驗證涉及處理器硬件和在其上運行的多層軟件。

本文討論了與硬件安全驗證相關的一些挑戰，并介紹了一種基于形式的方法來解決。實現流行的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）所需的嚴謹性，這些設計用于安全性至關重要的應用。