硬件安全門級細粒度形式化驗證方法

秦茂源，慕德俊，胡 偉，毛保磊

(西北工業大學 深圳研究院，廣東 深圳 518057)

近年來硬件安全問題頻頻發生，造成的后果日益嚴重，例如伊朗核電站震網事件，攻擊者通過網絡激活事先植入的硬件木馬使電機轉子超負荷運轉燒毀．然而，現今硬件設計仍缺乏有效的安全驗證方法檢測，導致硬件設計中存在潛在的安全漏洞、木馬、惡意程序等[1]．現有的安全驗證技術主要包含仿真和形式化驗證技術，但是仿真技術存在覆蓋率難以保證的問題．

形式化驗證技術采用嚴格的數學定義描述電路規范，形式化檢查硬件行為特征．現有的形式化驗證技術包括模型檢驗和定理證明．模型檢驗采用搜索算法驗證設計是否滿足設計規范，但會因設計規模的增大導致狀態空間爆炸．雖然引入符號執行后解決了狀態空間爆炸問題，但仍可能導致路徑爆炸．而定理證明是采用形式化語言描述程序規范和性質，用演繹的方法交互式地驗證程序的規范和性質[2]．PCH(Proof-Carrying Hardware)框架[3-4]首次提出了硬件可攜帶證明代碼的機制描述和驗證現場可編程門陣列(Field Programmable Gate Array，FPGA)的比特流文件．PCH-IP(Proof-Carrying Hardware-IP)框架[5-7]在PCH框架上進一步提出了IP核安全性可驗證框架．HiFV(Hierarchy-preserving Formal Verification)框架[8]和Enhanced PCH(Enhanced Proof-Carrying Hardware)框架[9]將IP核的驗證擴展至片上系統(System on Chip，SoC)的安全性驗證．以上方法皆采用形式化語言描述電路的設計規范和安全屬性傳播規則，通過定理證明的方式驗證電路的安全性，但都采用了保守的安全屬性傳播規則，引入了誤報，導致驗證結果不精確．

針對現有硬件設計形式化安全驗證技術的問題，筆者結合門級信息流跟蹤[10]與定理證明的方法，使用形式化語言描述硬件的規范和安全標簽傳播策略，將硬件設計轉化為包含信息流跟蹤邏輯的電路語義模型，繼而結合霍爾三元組理論構造驗證模型安全性的定理；然后使用證明策略驗證定理的合理性．

1 門級信息流跟蹤概述

門級信息流跟蹤是為電路分配表示安全屬性的污染標簽．考慮受污染的輸入對輸出的影響，構造可用于追蹤信息流動的與、或、非等邏輯門的跟蹤邏輯[10]:

其中，a、b和o分別為二輸入邏輯與門的輸入和輸出，at、bt和ot分別為其安全標簽．定義邏輯“1”表示受“污染”，邏輯“0”表示“非污染”．假設邏輯與門的輸入a被標記為“污染”(at為“1”)，輸入b被標記為“非污染”(bt為“0”)，當輸入b為“0”時，輸出o始終為“0”，輸入a對輸出沒有影響，則ot為“0”．如果輸入b為“1”，那么輸入a的變化便會導致o發生變化，則ot為“1”，因而可以推導出邏輯與門的追蹤邏輯．同理可推導或門、非門的追蹤邏輯，如式(2)和式(3)所示．

圖1 硬件安全門級細粒度形式化驗證方法的流程

2 電路語義模型的生成和驗證

硬件安全門級細粒度形式化驗證方法包括語義邏輯庫的生成、電路語義模型的生成、定理生成和證明生成4個步驟，如圖1所示．語義邏輯庫定義了用于描述原始電路和跟蹤邏輯的語法語句和計算函數；電路語義模型的生成是使用語義邏輯庫中的語法語句將硬件設計轉化為電路語義模型;定理生成則是使用霍爾三元組理論將電路語義模型轉變成待證明的定理;證明生成是使用證明策略和公理開發合理性的證明．

2.1 語義邏輯庫的生成

邏輯語義庫是對原始電路及其信息流跟蹤邏輯的語義描述，其包括原始語義庫及追蹤語義庫．原始語義庫定義了描述原始電路的語義語句，該庫包括了邏輯值、信號、邏輯值函數、原始表達式、表達式函數、原始賦值表達式、原始賦值函數的定義．而追蹤語義庫定義了跟蹤邏輯的語義語句，該庫包括了安全屬性、安全標簽、安全屬性傳播函數、追蹤表達式、追蹤表達式函數、追蹤賦值表達式、追蹤賦值函數的定義．

2.1.1 原始語義庫的生成

在Coq環境下，定義level類型，其構造子“hi”和“lo”表示邏輯“1”和邏輯“0”，如式(4)所示．因為數字電路中信號的邏輯值總是伴隨著時鐘發生變化，所以構造以自然數t為時間離散單元的一元函數bus表示信號，如式(5)所示．任何聲明為bus的信號都可以時間為參數返回該時間節點的邏輯值，例如，信號key被聲明為bus(key: bus)，則t時間下的邏輯值可表示為 keyt．邏輯值函數描述了與、或、非等基本邏輯門的邏輯運算規則，例如式(6)是以兩個level類型為參數，按照模式匹配返回一個level類型的與邏輯值函數and．其余或門(or)、非門(not)等邏輯值函數也可按照以上方法定義．

在定義函數類型bus及邏輯值函數的基礎上，引入原始表達式Exprorig類型，以“樹”型結構定義與邏輯構造子、或邏輯構造子、非邏輯構造子和類型轉換構造子，分別描述信號之間的與、或、非和類型變換邏輯操作．例如式(7)的類型轉換構造子SVorig可將bus類型的信號a以(SVoriga)的方式轉換為Exprorig類型的表達式．再如式(8)中的與邏輯構造子ExprAndOrig表示信號a、b的與邏輯操作，先將信號a、b轉換為Exprorig類型后，代入到ExprAndOrig中得到式(9)的一個復雜表達式．其計算可通過表達式函數Evalorig以模式匹配的方式將表達式規約為邏輯值函數．例如，將式(9)代入到Evalorig中得到式(10)，而后被規約至式(11)所示的邏輯值函數and．

由于硬件描述語言中賦值行為是一種隱含操作，而Coq并不具備實現這種隱含的操作能力，為此需要定義一種賦值表達式類型以命題邏輯的方式代替表示兩個信號之間的賦值行為．定義組合邏輯賦值類型Combine及時序邏輯賦值類型Sequence描述表達式之間的組合邏輯賦值及時序邏輯賦值，如式(12)和式(13)所示．例如Sequence (SVorigo)(ExprAndOrig(SVoriga)(SVorigb))表示了表達式(SVorigo)和表達式(ExprAndOrig(SVoriga)(SVorigb))之間的時序邏輯賦值，將其代入到原始賦值函數update中得到式(14)，繼而被規約為式(15)所示的等價命題邏輯．

2.1.2 追蹤語義庫的生成

為便于邏輯電平和安全屬性的邏輯計算，將安全屬性、安全標簽、邏輯值、信號統一定義為式(4)和式(5)．安全屬性傳播函數描述了追蹤邏輯的邏輯結構，如式(16)所示的或門安全屬性傳播函數org．追蹤表達式類型Exprg按照“樹形”結構逐個定義與、或、非等追蹤邏輯．例如式(17)所示的“或”追蹤邏輯構造子ExprOrg，該構造子表示了4個Exprg類型之間的或跟蹤邏輯表達式．該表達式的可被追蹤表達式函數Evalg規約至“或”安全屬性邏輯函數org．而追蹤賦值表達式類型同樣采用等價命題的方式表示追蹤邏輯表達式之間的賦值．例如使用式(18)的追蹤組合邏輯賦值表達式Combineg類型構造(SVgot)和(ExprOrg(SVga)(SVgb)(SVgat)(SVgbt)之間賦值，得到式(19)所示追蹤組合邏輯表達式．該表達式可通過追蹤賦值函數assigng將式(19)規約為式(20)．

2.2 電路語義模型生成

電路語義模型的生成是依據語義邏輯庫將電路網表映射為電路語義模型．該模型是由多個簡單合取命題組成的蘊含式，表示條件蘊含關系．每個簡單合取命題由追蹤賦值函數和原始賦值函數組成，通過合取連接詞連接表示必須同時成立．例如式(21)表示了一個輸入為a、b、c，輸出為o1t的電路語義模型．

2.3 定理生成和證明生成

定理生成依據霍爾邏輯三元組理論，將輸入和輸出的標簽定義作為定理的前條件{P}和后條件{Q}，電路語義模型作為程序C，生成該模型的待證明的定理．對于有多位輸出的電路，可首先構造多個單位比特輸出的電路語義模型．而后定義相應的子定理，以合取符號連接表示多位輸出電路語義模型的定理，如式(22)．子定理的證明即是良性定理的證明，借助輔助證明策略開發滿足安全策略的證明．如果所有子定理是良性的，那么定理是良性的，反之定理是非良性的．

定理：子定理1∧子定理2∧…∧子定理n．

(22)

3 實驗結果及其分析

3.1 實驗設計

采用硬件安全門級細粒度形式化驗證方法(Fine-granularity Gate level formal Verification method for hardware security，FGV)和具有保守傳播策略的硬件驗證方法(security verification method based on Conservative Security Property transition rules， CSP)驗證JTAG(Joint Test Action Group)調試接口程序和IWLS(International Workshop on Logic & Synthesis)測試基準，通過統計驗證結果，分析FGV精確性的原因和量化兩種方法所產生的精確度的差異．

3.2 硬件安全門級細粒度形式化驗證方法精確性的原因

JTAG調試接口的輸入、輸出分別由數據(data)、調試(debug)、選通(En)和輸出(out)組成．其工作原理是當En為“hi”時，選通data將數據傳輸到out，反之選通debug將數據傳輸到out．在明確功能的基礎上，分別為輸入、輸出分配安全標簽datat、Ent、debugt、outt，按照不可信的數據不能影響可信信息系統的完整性安全策略(被標記為“hi”的輸入不能將該屬性傳遞至outt)，采用FGV和CSP驗證JTAG調試接口程序，結果如表1所示．可以得出，當datat或者debugt為“hi”，或兩者皆為“hi”時，采用CSP所得到結果outt皆為“hi”， 輸出out總是不可信的．而采用FGV驗證時， 僅有部分情況會導致輸出不可信．例如表1第3行中data 為“lo”、datat為“lo”、En為“hi”、Ent為“lo”、debug為“lo”、debugt為“hi”的輸入組合，其驗證后輸出的安全標簽 outt為 “lo” (即輸出是安全的)． 分析原因是 FGV 保證了安全標簽傳播計算與電路實際工作狀態相符合，考慮En信號對支路的選擇，阻止了不可信信號在未選通的情況下將不可信的安全屬性傳遞到輸出，消除了誤報，提高了驗證精度．

表1 JTAG接口程序驗證部分真值表

3.3 FGV和CSP的精度對比

為對比FGV和CSP兩種方法的精確度，遵照秘密的信息不能流向輸出的機密性原則(即被標記為“hi”的輸入不能流向輸出)分別驗證IWLS測試集中9Symmel、cordic、frg1、decod、c432、Cm163a、count、cht這8組設計的安全性，將驗證得出的非良性子定理的數目作為量化驗證精度的指標，表2即為兩類方法驗證精度的對比統計．

表2 FGV和CSP驗證IWLS測試集非良性子定理數目

統計結果表明，在相同約束條件下，CSP得出的非良性子定理數目遠超出FGV所得出的非良性子定理數目．例如采用CSP驗證decod所得出的非良性子定理數目為480個，等同于子定理總數；而采用FGV驗證得到的非良性子定理數目為0．從而得知采用CSP驗證，其結果必然存在大量誤報．再如將9Symmel驗證的子定理總數從162個增加到512個，雖然FGV所驗證出的非良性子定理數目有所增長，但仍遠小于CSP所驗證出的非良性子定理數目．此外，CSP驗證cht得出的非良性子定理數目僅占子定理總數的8.6%，但仍舊在數目上遠高于FGV所驗證出的72個非良性子定理．因而可以得出FGV較之CSP有更高的精度．

4 總 結

筆者提出了硬件安全門級細粒度形式化驗證方法，可將硬件代碼構造為邏輯門層面上的電路語義模型，繼而結合霍爾定理生成可用于電路安全性驗證的定理和證明．通過對比硬件安全門級細粒度形式化驗證方法和保守傳播策略的硬件驗證方法驗證JTAG接口調試程序的結果，得出了硬件安全門級細粒度形式化驗證方法精確性的原因．而后選用IWLS測試集進行驗證，統計兩類方法所驗證出的非良性子定理的數目，量化分析精確性的差異．實驗表明，硬件安全門級細粒度形式化驗證方法能夠精確地驗證電路的安全屬性，有效地提高了驗證覆蓋率．