驗(yàn)證處理器的安全性已成為現(xiàn)代電子系統(tǒng)設(shè)計(jì)中必不可少的步驟。用戶希望確保他們的消費(fèi)類設(shè)備不會(huì)被黑客入侵，并且他們的個(gè)人和財(cái)務(wù)數(shù)據(jù)在云中是安全的。有效的安全驗(yàn)證涉及處理器硬件和在其上運(yùn)行的多層軟件。

本文討論了與硬件安全驗(yàn)證相關(guān)的一些挑戰(zhàn)，并介紹了一種基于形式的方法來解決。實(shí)現(xiàn)流行的RISC-V指令集架構(gòu)（ISA）的設(shè)計(jì)示例展示了這種方法的強(qiáng)大功能。

安全驗(yàn)證概述

對(duì)處理器進(jìn)行全面有效的驗(yàn)證是電子開發(fā)人員面臨的最大挑戰(zhàn)之一。從處理器從成堆的標(biāo)準(zhǔn)部件轉(zhuǎn)向定制芯片的那一刻起，功能驗(yàn)證就變得至關(guān)重要。為修復(fù)遺漏的錯(cuò)誤而重新制造的成本令人生畏，并且在現(xiàn)場(chǎng)更換有缺陷的設(shè)備前景令人恐懼。為硅前功能驗(yàn)證開發(fā)了復(fù)雜的工具和方法，重點(diǎn)團(tuán)隊(duì)補(bǔ)充了芯片設(shè)計(jì)人員。

隨著處理器芯片進(jìn)入安全關(guān)鍵型應(yīng)用，另一只鞋掉了下來：功能安全。即使是 100% 正確的芯片，也會(huì)因環(huán)境條件、α 粒子撞擊和硅老化效應(yīng)而面臨不當(dāng)行為的風(fēng)險(xiǎn)。如果這種故障影響植入式醫(yī)療設(shè)備、武器系統(tǒng)、核電站或自動(dòng)駕駛汽車，可能會(huì)失去生命。出現(xiàn)了一整套安全驗(yàn)證學(xué)科，以確保在安全受到損害之前檢測(cè)到故障并采取適當(dāng)?shù)捻憫?yīng)。

今天，第三只鞋正在掉落——也許三條腿的凳子是一個(gè)更好的比喻——硬件安全的重要性。在此討論的上下文中，安全性意味著惡意代理無法訪問電子系統(tǒng)來收集私人數(shù)據(jù)或控制其操作。每個(gè)需要功能安全的應(yīng)用也需要安全性;顯然，產(chǎn)品設(shè)計(jì)師必須確保心臟起搏器、軍事設(shè)備和自動(dòng)駕駛汽車不會(huì)被意圖造成傷害的人接管。

許多其他應(yīng)用程序也必須是安全的，以便機(jī)密數(shù)據(jù)不會(huì)被盜或被修改。據(jù)估計(jì)，網(wǎng)絡(luò)犯罪經(jīng)濟(jì)至少[]為1.5萬億美元。當(dāng)然，銀行和其他金融機(jī)構(gòu)必須受到保護(hù)，但有價(jià)值的個(gè)人數(shù)據(jù)存在于遍布全球的數(shù)以千計(jì)的系統(tǒng)中。身份盜竊可能代價(jià)高昂且對(duì)個(gè)人造成毀滅性打擊，即使只有幾條個(gè)人數(shù)據(jù)可以通過系統(tǒng)漏洞收集。

傳統(tǒng)上，安全性被認(rèn)為是一個(gè)軟件問題，重點(diǎn)是操作系統(tǒng)中的密碼和特權(quán)模式等技術(shù)。但眾所周知的漏洞，如[Meltdown和Spectre]已經(jīng)表明，硬件 - 處理器本身 - 也存在風(fēng)險(xiǎn)。對(duì)處理器進(jìn)行嚴(yán)格的安全驗(yàn)證是許多應(yīng)用的迫切需要。遺憾的是，對(duì)于處理器，沒有既定的、全面和一致的安全驗(yàn)證方法。

評(píng)估安全漏洞

評(píng)估知識(shí)產(chǎn)權(quán)（IP）設(shè)計(jì)（包括處理器）中的漏洞有一種既定的方法。第一步是在寄存器傳輸級(jí) （RTL） 設(shè)計(jì)中確定每個(gè)資產(chǎn)，即在 IP 中使用、生產(chǎn)或保護(hù)的任何有價(jià)值或重要的資產(chǎn)。要確定必須保護(hù)這些資產(chǎn)的對(duì)象，下一步是確定可能試圖破壞這些資產(chǎn)的對(duì)手和可能的攻擊面，即可以應(yīng)用威脅的訪問點(diǎn)集。

最后一步是確定必須驗(yàn)證哪些資產(chǎn)，哪些資產(chǎn)來自**哪些對(duì)手的攻擊。這包括確定每個(gè)資產(chǎn)的所有權(quán)以及資產(chǎn)的機(jī)密性、完整性和可用性 （[CIA] 目標(biāo)。這個(gè)過程提供了一種系統(tǒng)的方法來解決理論上無限的負(fù)面行為和后果空間，并識(shí)別處理器設(shè)計(jì)中的漏洞。

美國(guó)國(guó)家標(biāo)準(zhǔn)與技術(shù)研究院 （NIST） 通過定義通用漏洞評(píng)分系統(tǒng) （[CVSS]） 來對(duì)發(fā)現(xiàn)的漏洞的嚴(yán)重性進(jìn)行定量評(píng)估，從而進(jìn)一步有序地執(zhí)行該過程。如圖 1 所示，[CVSS v3.1]規(guī)范定義了三個(gè)指標(biāo)組：基本、臨時(shí)和環(huán)境。在本文的討論范圍內(nèi)，僅需要考慮 Base 組，該組表示漏洞的內(nèi)在品質(zhì)，這些特性在一段時(shí)間內(nèi)和跨用戶環(huán)境中保持不變。[CVSS 計(jì)算器]提供漏洞的總體分?jǐn)?shù)。

點(diǎn)擊查看全尺寸圖片*圖 1：CVSS 規(guī)范提供了對(duì)漏洞嚴(yán)重性的定量評(píng)估。資料來源：美國(guó)國(guó)家情報(bào)研究院

正式的論據(jù)

形式化技術(shù)長(zhǎng)期以來在功能驗(yàn)證中發(fā)揮著重要作用，近年來它們變得至關(guān)重要。沒有仿真測(cè)試平臺(tái)和測(cè)試集，甚至運(yùn)行生產(chǎn)代碼的在線仿真，都可以保證沒有錯(cuò)誤?？偸怯锌赡軓奈从|發(fā)過一些潛伏的設(shè)計(jì)錯(cuò)誤，或者從未檢測(cè)到其影響。基于模擬的方法本質(zhì)上是概率性的;他們只能探索可能的設(shè)計(jì)行為的極小百分比。

形式核查由于其詳盡無遺的性質(zhì)而根本不同。屬性的正式證明保證任何可能的設(shè)計(jì)行為都不能違反該屬性所表達(dá)的設(shè)計(jì)意圖。因此，與該屬性相關(guān)的設(shè)計(jì)中不可能有錯(cuò)誤。

指定一組可靠的屬性并正式證明它們可以實(shí)現(xiàn)其他方法無法提供的確定性級(jí)別。由于處理器是一些最大和最復(fù)雜的芯片設(shè)計(jì)，因此形式驗(yàn)證早在它成為整個(gè)行業(yè)的主流技術(shù)之前就已應(yīng)用于其驗(yàn)證。

如前所述，功能安全是確定性至關(guān)重要的另一個(gè)領(lǐng)域。許多行業(yè)和應(yīng)用的安全標(biāo)準(zhǔn)要求可以正確檢測(cè)和處理大部分可能的故障。形式安全驗(yàn)證是從數(shù)學(xué)上證明處理器設(shè)計(jì)符合相關(guān)標(biāo)準(zhǔn)（如 ISO 26262）要求的唯一方法。不出所料，形式化方法也提供了實(shí)現(xiàn)安全驗(yàn)證確定性的唯一數(shù)學(xué)嚴(yán)謹(jǐn)方法。盡管在功能正確性、安全性和安全性方面存在差異，但形式驗(yàn)證是所有三個(gè)領(lǐng)域共有的解決方案。

處理器安全性的形式驗(yàn)證

CVSS分類的既定方法和形式化方法的強(qiáng)大功能可以組合成一種新的方法來驗(yàn)證處理器的安全性。關(guān)鍵鏈接是定義處理器的資產(chǎn)并寫入檢查這些資產(chǎn)的任何危害的屬性。然后可以正式驗(yàn)證這些屬性以識(shí)別任何設(shè)計(jì)錯(cuò)誤，一旦這些錯(cuò)誤得到修復(fù)，它們就會(huì)證明設(shè)計(jì)的安全性。

對(duì)于處理器，體系結(jié)構(gòu)上可見的狀態(tài)元素是資產(chǎn)的正確抽象級(jí)別。其中包括：

• 程序計(jì)數(shù)器 （PCR）* 寄存器文件 （REG）* 控制狀態(tài)寄存器 （CSR）* 數(shù)據(jù)存儲(chǔ)器

算術(shù)邏輯單元 （ALU）、移位器、解碼器和其他處理元素不被視為資產(chǎn)。這些是允許訪問資產(chǎn)的計(jì)算元素。如果它們處于安全攻擊的路徑中，則凈效應(yīng)將發(fā)生在資產(chǎn)上，這是屬性提供入侵檢查的地方。

所有輸入/輸出 （I/O） 接口都被視為處理器的攻擊面。從內(nèi)存接口、中斷引腳和調(diào)試端口讀取的指令都是攻擊者攻擊的有效位置。對(duì)于本文的分析，任何不是給定資產(chǎn)合法所有者的指令都將自動(dòng)被視為對(duì)手。由于攻擊者總數(shù)、與每個(gè)時(shí)鐘周期交換資產(chǎn)所有權(quán)的頻率以及管道的并發(fā)性（這是管道深度的函數(shù)），處理器安全驗(yàn)證尤其具有挑戰(zhàn)性。

應(yīng)用于RISC-V設(shè)計(jì)

這種方法可用于任何處理器設(shè)計(jì)，但RISC-V ISA因其在整個(gè)電子行業(yè)中的廣泛采用而特別令人感興趣。ISA 有許多實(shí)現(xiàn)可作為開源 RTL 使用，為任何新的驗(yàn)證工具或方法提供了大量實(shí)際測(cè)試用例。圖 2 顯示了如何使用 formalISA 驗(yàn)證任何 RISC-V RTL 處理器設(shè)計(jì)的安全性，[FormalISA]是一種可與任何商業(yè)形式驗(yàn)證工具配合使用的安全分析器。

點(diǎn)擊查看全尺寸圖像圖 2：安全分析器對(duì) RISC-V RTL 處理器設(shè)計(jì)執(zhí)行形式驗(yàn)證。來源： 公理

屬性指定可以修改資產(chǎn)的合法方式，因此為資產(chǎn)設(shè)置的屬性證明保證不會(huì)發(fā)生意外結(jié)果。圖 3 顯示了 Ibex RISC-V 設(shè)計(jì)和標(biāo)準(zhǔn) BEQ（如果相等則分支）指令的屬性示例。ISA指定有效的BEQ指令將比較兩個(gè)寄存器，如果它們相等，則將PCR值設(shè)置為使用指令中包含的偏移量計(jì)算的新地址。已評(píng)估 CVSS 指標(biāo)，并使用這些指標(biāo)值的縮寫字符串來命名屬性。

點(diǎn)擊查看全尺寸圖像*圖 3：上面的示例顯示了具有 CVSS 指標(biāo)的安全屬性。來源： 公理

確定并列出要寫入的安全屬性可以定義一個(gè)驗(yàn)證計(jì)劃，在概念上類似于要編寫的傳統(tǒng)模擬測(cè)試列表。與模擬測(cè)試一樣，安全屬性的正式分析結(jié)果可以反向注釋到計(jì)劃中，以顯示驗(yàn)證進(jìn)度。

圖4顯示了[CV32E40P]和[零RISC-V處理器的安全驗(yàn)證計(jì)劃片段，顯示了PCR屬性。此表中已包含正式結(jié)果，顯示所有屬性都已通過（完全證明），并且未發(fā)現(xiàn)與將通過處理器上運(yùn)行的軟件執(zhí)行的處理器操作相關(guān)的漏洞。

點(diǎn)擊查看全尺寸圖像*圖 4：安全驗(yàn)證計(jì)劃的片段突出顯示了 CV23E40P 和零芯的 PCR 屬性和結(jié)果。來源： 公理

針對(duì) PCR 之外的此核心的其他資產(chǎn)編寫和分析了安全屬性。分析了REG中所有由RISC-V定義的R型，I型和U型類實(shí)現(xiàn)的指令。分析了CSR的6條CSR指令、同步異常和異步異常。分析DMR以獲取STORE指令。作為評(píng)估 DMR 的一部分，還確定不會(huì)發(fā)生非法內(nèi)存訪問。編寫并驗(yàn)證了其他屬性，以確保非分支/跳轉(zhuǎn)指令按預(yù)期增加PCR。

在RISC-V中發(fā)現(xiàn)的錯(cuò)誤示例

該方法已應(yīng)用于許多開源和專有的RISC-V實(shí)現(xiàn)，并且已經(jīng)發(fā)現(xiàn)了許多與安全相關(guān)的錯(cuò)誤。

對(duì)圖3所示屬性的正式分析揭示了Ibex核心中的錯(cuò)誤行為：在周期5中執(zhí)行BEQ指令時(shí)，由于在周期7中啟動(dòng)的外部調(diào)試，PCR值在周期6中被錯(cuò)誤地更改。這將導(dǎo)致執(zhí)行意外指令，這些指令可能會(huì)執(zhí)行未經(jīng)授權(quán)的訪問或以其他方式損害安全性。

在CV32E40P內(nèi)核中也發(fā)現(xiàn)了一個(gè)嚴(yán)重的錯(cuò)誤。非特權(quán)指令 （STORE） 可能會(huì)阻止對(duì)特權(quán)指令 （EBREAK） 的訪問，從而損害完整性和可用性。CVSS的高分7.9表明這是設(shè)計(jì)中的一個(gè)重大漏洞。圖 5 顯示了由此產(chǎn)生的問題，僅當(dāng)有限狀態(tài)機(jī) （FSM） 控制器處于 DECODE 狀態(tài)時(shí)，傳入的調(diào)試請(qǐng)求才會(huì)觸發(fā)該問題。該錯(cuò)誤不會(huì)以任何其他狀態(tài)顯示，這使得動(dòng)態(tài)模擬難以捕獲此錯(cuò)誤，并且可能導(dǎo)致未經(jīng)正式驗(yàn)證的安全漏洞。

點(diǎn)擊查看全尺寸圖像內(nèi)核中的錯(cuò)誤與指令權(quán)限有關(guān)。*來源： 公理

理想情況下，如果內(nèi)存返回有效未到達(dá)，則 LOAD 或 STORE 不應(yīng)正常工作，這不是功能錯(cuò)誤。但是，當(dāng)內(nèi)存返回有效被阻止，并且存在正在進(jìn)行的 LOAD/STORE 指令時(shí)，它不應(yīng)阻止（導(dǎo)致死鎖）特權(quán)指令的執(zhí)行，尤其是鏈接到外部調(diào)試的指令，這是最高特權(quán)指令。

圖6和圖7提供了安全分析儀在眾所周知的RISC-V設(shè)計(jì)中發(fā)現(xiàn)的兩個(gè)附加示例。

圖6顯示了PCR在WARP-V核心中是如何受到損害的。對(duì)于日航指令，PCR 未正確更新。對(duì)于未對(duì)齊的跳躍，必須引發(fā)異常。必須使用目標(biāo)地址而不是目標(biāo)偏移量檢查字節(jié)對(duì)齊。此錯(cuò)誤會(huì)影響此設(shè)計(jì)的多種變體：6 階段、4 階段和 2 階段。但是，此錯(cuò)誤的嚴(yán)重性中等，會(huì)影響完整性并獲得 CVSS 分?jǐn)?shù) 5。

點(diǎn)擊查看全尺寸圖像圖 6：這就是 PCR 在 WARP-V 核心中受到損害的方式。來源： 公理

圖 7 顯示了一個(gè)意外代碼的示例，該代碼導(dǎo)致形式驗(yàn)證發(fā)現(xiàn)的 zeroriscy 核心中的安全問題。這是一個(gè)特別麻煩的錯(cuò)誤，影響了機(jī)密性、完整性和可用性，CVSS 的最高分?jǐn)?shù)為 10。這是一個(gè)嚴(yán)重的缺陷，因?yàn)槌Ｒ?guī) LOAD 指令無法正常工作，因?yàn)樵O(shè)計(jì)中的自定義修改覆蓋了 REG-REG 加載的正常 LOAD 指令的行為。盡管自定義代碼是偶然留下的，但這很可能是在設(shè)計(jì)中故意被黑客入侵的。無論哪種情況，都可以使用正式方法解決此類問題。

點(diǎn)擊查看全尺寸圖像圖 7：這就是意外代碼在零點(diǎn)核心中導(dǎo)致安全問題的方式。來源： 公理

雖然形式驗(yàn)證提供確定性和證據(jù)的獨(dú)特能力顯然很有價(jià)值，但一些用戶可能會(huì)懷疑所執(zhí)行的詳盡分析是否花費(fèi)了太長(zhǎng)時(shí)間。圖8應(yīng)該可以消除任何此類擔(dān)憂，表明在幾秒鐘內(nèi)在多個(gè)RISC-V處理器內(nèi)核中發(fā)現(xiàn)了從輕微到非常危險(xiǎn)的問題。

點(diǎn)擊查看全尺寸圖像 圖 8：驗(yàn)證結(jié)果還概述了查找 RISC-V 內(nèi)核問題的時(shí)間。來源： 公理

用于處理器安全驗(yàn)證的正式工具

一段時(shí)間以來，驗(yàn)證處理器設(shè)計(jì)的功能正確性和功能安全性一直依賴于正式工具，這種方法現(xiàn)在正在擴(kuò)展到安全性。本文介紹了一種使用形式化方法進(jìn)行處理器安全驗(yàn)證的方法，方法如下：

• 以 CIA 安全目標(biāo)為指導(dǎo)，構(gòu)建強(qiáng)大的處理器安全驗(yàn)證計(jì)劃。* 使用 CVSS 評(píng)分系統(tǒng)計(jì)算每個(gè)漏洞的漏洞分?jǐn)?shù)。* 使用抽象驅(qū)動(dòng)的方法進(jìn)行形式驗(yàn)證，以獲得 100% 的證明收斂。

該解決方案可與任何正式工具互操作，并自動(dòng)生成可在仿真和仿真中重復(fù)使用的覆蓋屬性。本文概述的方法還提供了處理器設(shè)計(jì)（包括RISC-V）所需的嚴(yán)謹(jǐn)性，這些設(shè)計(jì)用于安全性至關(guān)重要的應(yīng)用。