基于安全風險的RTL級硬件木馬驗證研究

趙劍鋒,史 崗

基于安全風險的RTL級硬件木馬驗證研究

趙劍鋒1,2,史 崗2

1中國科學院大學 網絡空間安全學院 北京 中國 1000492中國科學院信息工程研究所 第五實驗室 北京 中國 100093

信息時代使得信息安全變得日益重要。攻擊方為了獲取想要的信息, 除了使用軟件方面的手段, 如病毒、蠕蟲、軟件木馬等, 也使用硬件手段來威脅設備、系統和數據的安全, 如在芯片中植入硬件木馬等。如果將硬件木馬植入信息處理的核心--處理器, 那將風險更高、危害更大。然而, 硬件木馬位于信息系統底層核心的層面, 難以被檢測和發現出來。硬件木馬是國內外學術界研究的熱點課題, 尤其是在設計階段結合源代碼的硬件木馬檢測問題, 是新問題, 也是有實際需要的問題。在上述背景下, 圍繞源代碼中硬件木馬的檢測和驗證展開了研究?；谟布抉R危害結果屬性, 在學術上提出基于安全風險的模型和驗證規則, 給出相應的描述形式, 從理論上說明安全驗證規則在減少驗證盲目性、縮小可疑代碼范圍、提高評估效率的作用, 實驗表明, 基于安全風險規則的驗證, 可以避免驗證的盲目性和測試空間向量膨脹的問題, 有效驗證疑似硬件木馬的存在和危害, 對源代碼安全評估是有一定效果的。

芯片; RTL級硬件木馬; 安全風險; 驗證規則

1 引言

信息安全深刻影響著世界的政治、經濟、軍事等領域。信息安全包括軟件安全和硬件安全, 除了人們熟知的軟件安全威脅, 如病毒、木馬和蠕蟲外, 攻擊方已經滲透到硬件安全, 尤其作為信息處理核心的處理器芯片的安全, 更是重中之重[1-4]。

由芯片的設計與制造的流程可以看出, 芯片生產設計制造的復雜程度為芯片安全埋下了隱患, 導致芯片的安全性變得越來越脆弱。

2007年, IBM沃森研究中心聯合伍斯特理工學院首次提出了硬件木馬的概念[5]。之后, 經過國外相關研究人員, 如D．Jia[6], X. Wang和M.Tehranipoor, Yier Jin[7]等以及國內(如西北工業大學、中國科學院信息工程研究所等高校和研究機構)硬件木馬研究人員[8-9]的多方面深入地拓展研究, 形成了硬件木馬的一般概念: 硬件木馬主要是指在集成電路芯片(可以在設計、制造、生產的各個階段)中故意植入含有惡意功能的邏輯電路, 并且某種特定條件下觸發該惡意邏輯功能, 以達到攻擊方非法的目的(如信息泄漏、拒絕服務、毀壞芯片、系統權限提升等)。

硬件木馬研究作為國內外學術界關注的焦點, 涉及多個研究方面, 包括硬件木馬設計、檢測、驗證及防范等[10-15]。其中, 關于第三方源代碼安全評估問題(由于芯片設計與制造過程相分離, 導致第三方源代碼安全不可控, 特別是對于國防、政府、金融、交通等敏感領域而言, 更是如此), 是熱點問題, 同時也是難點問題。

文章圍繞RTL(Register Transfer Level)級源代碼(硬件描述語言書寫的)中硬件木馬的問題展開了研究。主要貢獻: 針對RTL級硬件木馬尚未在學術上給出一般安全風險模型和指導規則, 結合對標準集的分析結果, 提出相應的模型和定義, 給出安全風險模型和描述形式, 在安全風險模型的基礎上, 提出了安全風險驗證規則, 從理論上說明基于安全風險驗證規則, 可以減少驗證盲目性、縮小可疑代碼范圍、提高源代碼評估效率。實驗表明, 基于安全風險的驗證, 對RTL級源代碼評估是有一定效果的。

文章主要包括以下部分: 第2小節, 給出當前常見的評估驗證方法; 第3小節, 在硬件木馬集的基礎上抽象出硬件木馬一般模型和定義、安全風險模型, 并提出安全風險驗證規則, 指導驗證工作; 第4小節給出實驗; 最后是總結與展望部分, 對研究內容進行總結, 并提出了下一步的研究方向。

2 相關方法

如今, 集成電路設計與制造技術發展越來越快, 規模也是越來越大, 要對日益龐大的集成電路進行完整地驗證, 其難度也是與日俱增。有研究數據指出, 要開發一款芯片, 驗證付出的時間占整個工程周期的3/4左右, 而驗證人員也比設計人員要多一倍。驗證時間的長短和效率在一定程度上決定芯片的上市日期, 也決定了企業、公司的前途和命運, 這就對驗證工作的效率提出了迫切的需求。

當前, 驗證方法主要分成形式化方法和非形式化方法。

形式化方法是嚴格基于數學理論的方法, 采用相應形式化語言來描述目標系統性質, 根據嚴格的數學符號和相應法則, 對系統結構、行為進行簡潔高效的描述、分析、推理和演算, 以此為系統屬性的說明、開發、驗證設計了框架, 能夠輔助發現目標系統設計需求中的不一致性、不完備性等非正常情況。形式化方法主要包括三種方式, 分別是等價性驗證、模型檢驗和定理證明。

形式化等價檢查提供了一種等價檢測機制, 能夠驗證RTL與RTL, RTL與netlist或者netlist與netlist之間的等價性。該方法的優點是利用邏輯等價性加快驗證速度, 同時能夠保證能夠提供100%的覆蓋率, 該方法最大的優點是不需要外部輸入的測試向量, 故而可以節約測試時間, 縮短測試周期。這種方法在工業界已經得到廣泛的應用。如乘法器件、GPU等中的應用。模型驗證就是比較已設計的產品的行為和用戶定義的邏輯特征是否相符合。模型檢驗的方法目前己經開始為工業界所接受, 其優點是完全自動化, 當系統不滿足給定的性質時, 檢驗結果會給出反例, 來幫助驗證人員發現錯誤。定理證明一般采用交互式的定理輔助證明器來對系統問題進行抽象描述, 并以數學公式定理的方式表達系統的功能和安全性。采用數學定理推導演算的方法進行驗證, 目前未被業界廣泛采用。

非形式化方法主要是模擬驗證方法, 內建自測方法。

模擬驗證是集成電路設計驗證經常采用的方法[16]。其原理是: 通過對待驗證電路施加激勵, 將得到的響應與預期結果比較, 來發現設計中的問題。

內建自測方法, 簡稱為BIST(Built-In Self- Test), 實質是在設計一個芯片時, 在其內部加外額外的邏輯功能模塊[17], 通過額外的邏輯功能模塊可以監測芯片內部的信號狀態正常與否。在芯片實際運行當中, 安全的芯片通過BIST電路生成一個簽名, 如果芯片中含有硬件木馬, 則會生成另外一個不同的簽名。

最近幾年, 提出了不少新的驗證研究方法, 如西北工業大學研究團隊提出的門級信息流方法, 還有統計學習方法[18]、SVM(Support Vector Machine)[19]、機器學習[20-21]、自學習[22]、深度學習[23]、多層神經網絡[24]、人工免疫系統及行為分類[24]等多種方法。

對于RTL級源代碼安全性評估和驗證而言, 當前方法存在的主要問題有:

(1) 缺乏一般的安全風險模型和指導規則, 對于龐大的RTL級源代碼安全性評估和驗證而言, 缺少針對性, 即哪些是評估的重點區域, 哪些地方存在安全風險, 不知道這些, 會導致安全評估和驗證具有盲目性[25-29];

(2) 形式化方法中的等價性檢查僅僅驗證RTL與RTL, RTL與netlist或者netlist與netlist之間的等價性, 模型檢驗存在狀態空間爆炸的問題, 定理證明方法尚未被業界廣泛采用;

(3) 非形式化方法中的模驗證方法, 主要從正向來驗證芯片的邏輯功能是否滿足要求, 其目的是驗證芯片是否滿足設計功能, 需要龐大的測試向量, 測試時間長; 內建自測方法需要在芯片中加入額外邏輯功能模塊, 增加硬件開銷;

(4) 門級信息流方法、機器學習方法及自學習方法等, 需要將RTL源代碼轉換成門級網表, 使其邏輯錐龐大, 同樣存在著驗證空間過大的問題。

基于以上方法存在的問題, 在面臨RTL級源代碼安全評估和驗證時, 試圖在分析現有硬件木馬集的基礎上, 給出硬件木馬的一般模型, 提煉出安全風險模型, 以此得出面向安全風險的驗證規則, 來指導RTL級源代碼的安全性評估和驗證工作。

3 安全風險模型及規則

3.1 安全風險模型及規則提出原因

(1) 在芯片設計過程中, 除了自主開發源代碼以外, 會購買集成大量的第三方的IP核(Intellectual Property core), 包括含RTL源碼的IP核。在對其進行安全評估時, 面臨的源文件多, 源代碼量大, 如果只是單純采取傳統驗證分析方法, 必然導致大量的人力、物力、財力消耗, 并且驗證效果也難以保證。因此, 如果能提出相應的安全風險模型和指導規則, 對于RTL源代碼安全性評估和驗證具有重要的工程意義。

(2) 從硬件木馬攻擊者角度出發, 硬件木馬攻擊者為了達到攻擊目的, 必然要設計隱藏性很好的木馬, 才能有效保護自己, 待到特定條件時達到攻擊的目的。它的觸發和激勵的位長有關系, 即位數長, 硬件木馬被觸發的概率小; 位數短, 被觸發的概率大。如果激勵空間不是很大, 在計算量可忍受范圍內, 則通過全覆蓋可以測出。如果激勵空間范圍大, 如在2128個向量中取某個值, 假設向量空間的取值是服從均勻分布的, 則一次觸發硬件木馬的概率為2128分之一, 這個概率幾乎是0。為了發現這種木馬, 就要產生很大的測試向量, 這在時間上耗費太大, 通過正向測試的方法難以發現這樣的硬件木馬, 那么如果通過對源代碼的分析, 結合安全風險模型和指導規則, 并且根據查找到的有關參量位產生測試激勵, 它比盲目產生隨機測試激勵針對性更強。

3.2 基于標準集分析結果

Trust-Hub含有52不同模塊硬件木馬樣本, 包括21個AES加密系列模塊實例, 10個RS232系列模塊, 7個MC8051系列模塊, 4個PIC16F84系列模塊, 4個RSA系列模塊, 3個B19系列模塊, 2個wb_conmax系列模塊和1個memctrl模塊。

Trust-Hub標準集是研究硬件木馬檢測和驗證的樣本庫, 通過對硬件樣本集的分析來抽象硬件木馬的一般概念和安全風險模型, 并在此基礎上提出安全風險驗證規則, 以指導RTL級源代碼安全評估和驗證工作。

對Trust-Hub標準集統計分析可以得到硬件木馬所處位置、危害結果及特征表現的數據。

從表1可以看出, 硬件木馬直接依附于I/O端口的占到69.2%, 依附于狀態機的占到15.4%, 依附于特殊寄存器(如計數器、特權模式設置寄存器等)占到15.4%。

表1 硬件木馬所處位置統計數據[30]

在表2中, 統計出四種危害結果, 包括信息泄漏、功能改變、拒絕服務和破壞芯片, 其所占百分比分別為38.5%、46.2%、9.6%、5.8%, 在后續的論述中, 結合現實情況, 加入了系統權限提升這一危害。

表2 硬件木馬危害結果統計數據[30]

表3給出了危害結果與所處位置之間的統計關系。

表3 危害結果與所處位置的統計關系數據[30]

表4給出了常見硬件木馬的書寫特征表現形式, 可以作為驗證可疑硬件木馬的參考標準。

表4 Trust-Hub硬件木馬特征[31]

3.3 基本定義和安全風險模型

根據3.2節分析結果, 可以給出一個一般性的硬件木馬模型如下圖。

根據圖1模型, 可以給出如下相關定義。

圖1 硬件木馬模型示意圖

Figure 1 Schematic diagram of hardware trojan model

定義1:

芯片IC可以抽象為一個非空集合, IC={I, O, N, A, NF, AF}; 其中:

I: 表示輸入端口集合, I={I1, I2, …, I}, 其中下標表示輸入端口個數;

O: 表示輸出端口集合, O={O1, O2, …, O}, 其中下標表示輸出端口個數;

N: 表示正常狀態的電路集合, N={N1, N2, …,N}, 其中下標表示正常電路集合個數;

A: 表示硬件木馬電路集合, A={A1, A2, …, A}, 其中下標表示硬件木馬電路集合個數;

NF: 表示芯片正常的功能集合, NF={ NF1, NF2, …, NF}, 其中下標表示正常電路功能個數;

AF: 表示硬件木馬的危害功能集合, AF={AF1, AF2, …, AF}, 其中下標表示硬件木馬電路功能個數。

定義2:

設X為要安全評估和驗證的RTL級源代碼, 同樣為一個非空集合X={I, O, N, A, NF, AF}, 對其進行安全評估和驗證, 依據定義1, 當滿足:

定義3: 將定義1中危害功能集合AF={AF1, AF2, …, AFs}定義為安全風險集合, 每一個危害功能與一個安全風險相對應, 結合3.2節分析及現實情況, 安全風險集合S={Ileakage, Fchange, Dservice, Cdestroy, Sempower}, 其中:

Ileakage表示信息泄漏安全風險;

Fchange表示功能改變安全風險;

Dservice表示拒絕服務安全風險;

Cdestroy表示破壞芯片安全風險;

Sempower表示提升權限安全風險。

定義4: 將3.2節中表3.1中硬件木馬位置定義為安全風險位置, 安全風險位置集合L={Pio, Smachine, Rin}, 其中:

Pio表示處于輸入或輸出端口位置;

Smachine表示處于狀態機位置;

Rin表示處于內部特殊寄存器位置。

定義5: P表示安全風險位置集合L中第個元素出現的概率, 則由概率論基礎知識可知, 0≤P≤1, 其中, 1≤≤||, 其中| |表示取集合元素的個數。

在定義5的基礎上, 借助于信息熵的概念, 提出安全風險熵H=－log2(1/P);

H取值大表示安全風險位置出現的概率小, 檢測和驗證相對困難;

H取值小表示安全風險位置出現的概率大, 檢測和驗證相對容易。

定義6: 定義安全風險評估分類集合E為定義3中的安全風險集合S與定義4中的安全風險位置集合L的笛卡爾積, 集合E中每一元素表示安全風險評估的一個類別, 即安全風險位置是什么, 對應的安全風險危害是什么。

硬件木馬在位置、危害、特征表現上各不相同, 根據3.2節標準集分析結果及以上定義, 可以給出以下安全風險模型及相應的形式描述。

(1) 安全風險模型一

如圖2所示, 圖中帶箭頭實線表示正常在狀態轉換, 虛線表示轉移到安全風險狀態。

Figure 2 Schematic diagram of security risk model one

圖2安全風險模型一的形式化表示為一個四元組(S, I, O, T), 其中:

S: 有窮非空狀態集{S0, S1, S2, Ileakage, Fchange, Dservice, Cdestroy}, 其中S0, S1, S2表示正常狀態, Ileakage表示信息泄漏安全風險狀態, Fchange表示功能改變安全風險狀態, Dservice表示拒絕服務安全風險狀態, Cdestroy表示破壞芯片安全風險

I: 有窮非空輸入集{I1, I2, I3, I4, I5, I6, I7, I8}

O:有窮非空輸出集{ O1, O2, O3, O4, O5, O6, O7, O8}

T: 表示在輸入I集中某元素時, S狀態集中某兩個狀態之間的轉換函數

=>: 表示狀態轉換

狀態描述如下:

S0+ I1=> S1+ O1表示當前狀態為S0, 在輸入I1的情況下, 轉換到狀態S1, 輸出為O1;

S1+ I5=> S2+ O5表示當前狀態為S1, 在輸入I5的情況下, 轉換到狀態S2, 輸出為O5;

S0+ I7=> S2+ O7表示當前狀態為S0, 在輸入I7的情況下, 轉換到狀態S2, 輸出為O7;

S2+ I2=> S0+ O2表示當前狀態為S2, 在輸入I2的情況下, 轉換到狀態S0, 輸出為O2;

S1+ I4=> CDestroy+ O4表示當前狀態為S1, 在輸入I4的情況下, 轉換到狀態CDestroy, 輸出為O4;

S1+ I3=> FChange+ O3表示當前狀態為S1, 在輸入I3的情況下, 轉換到狀態FChange, 輸出為O3;

S0+ I6=> DService+ O6表示當前狀態為S0, 在輸入I6的情況下, 轉換到狀態DService, 輸出為O6;

S2+ I8=>ILeakage+ O8表示當前狀態為S2, 在輸入I8的情況下, 轉換到狀態ILeakage, 輸出為O8。

(2) 安全風險模型二

如圖3所示, 圖中帶箭頭實線表示正常在狀態轉換, 虛線表示轉移到非法狀態。

圖3 安全風險模型二

Figure 3 Schematic diagram of security risk model two

圖3安全風險模型二的形式化表示為一個四元組(S, I, O, T), 其中:

S: 有窮非空狀態集{S0, S1, S2, HTs0, HTs1, HTs2, HTs3}, 其中S0, S1, S2表示正常狀態, HTs0, HTs1, HTs2為過渡態, 不具有危害, 只有連續依次經過HTs0, HTs1, HTs2三種狀態, 才能達到安全風險狀態HTs3={Ileakage, Fchange, Dservice, Cdestroy, Sempower},

Ileakage表示信息泄漏安全風險狀態, Fchange表示功能改變安全風險狀態, Dservice表示拒絕服務安全風險狀態, Cdestroy表示破壞芯片安全風險, Sempower表示提升權限安全風險

I: 有窮非空輸入集{I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11}

O: 有窮非空輸出集{ O1, O2, O3, O4, O5, O6, O7, O8, O9, O10, O11}

T: 表示在輸入I集中某元素時, S狀態集中某兩個狀態之間的轉換函數

=>: 表示狀態轉換

狀態描述如下:

S0+ I1=> HTs0+ O1表示當前狀態為S0, 在輸入I1的情況下, 轉換到狀態HTs0, 輸出為O1; 在這種情況下, 如果下一個輸入為I9, 則又轉入到正常狀態S0;

HTs0+ I2=> HTs1+ O2表示當前狀態為HTs0, 在輸入I2的情況下, 轉換到狀態HTs1, 輸出為O2; 在這種情況下, 如果下一個輸入為I10, 則又轉入到正常狀態S0;

HTs1+ I3=> HTs2+ O3表示當前狀態為HTs1, 在輸入I3的情況下, 轉換到狀態HTs2, 輸出為O3; 在這種情況下, 如果下一個輸入為I11, 則又轉入到正常狀態S0;

注意: 不存在以下轉換關系

HTs2+ I4=> HTs3+ O4表示當前狀態為HTs2, 在輸入I4的情況下, 轉換到狀態HTs3, 輸出為O4;

只有在當前狀態為S0時, 連續輸入I1、I2、I3、I4時, 才從S0=> HTs0=> HTs1=> HTs2=> HTs3, 這時才達到安全風險狀態。

以下四種狀態均為正常狀態之間的轉換關系:

S0+ I6=> S2+ O6表示當前狀態為S0, 在輸入I6的情況下, 轉換到狀態S2, 輸出為O6;

S2+ I5=> S0+ O5表示當前狀態為S2, 在輸入I5的情況下, 轉換到狀態S0, 輸出為O5;

S2+ I7=> S1+ O7表示當前狀態為S2, 在輸入I7的情況下, 轉換到狀態S1, 輸出為O7;

S1+ I8=> S0+ O8表示當前狀態為S1, 在輸入I8的情況下, 轉換到狀態S0, 輸出為O8。

(3) 安全風險模型三

如圖4所示, 圖中帶箭頭實線表示正常在狀態轉換, 虛線表示轉移到非法狀態。

圖4 安全風險模型三

Figure 4 Schematic diagram of security risk model three

圖4(a)表示系統提權模型, 其形式化表示為一個七元組 (U, S, Sempower, T, P, R, N), 其中:

U: 用戶態

S: 正常情況下的系統態或內核態

T: 表示狀態之間的轉換關系

P: 表示U通過系統調用指令達到系統態S

R: 表示從系統態S返回到用戶態U

N: 表示非正常系統調用, 可以通過后門指令或普通用戶指令組合實現

=>: 表示狀態轉換

狀態描述如下:

U+P=> S, 表示當前為用戶態U, 在P的作用下, 轉換到正常系統態S;

S+R=> U, 表示當前為正常系統S, 在R的作用下, 轉換到用戶態U;

U+N=> Sempower表示當前為用戶態U, 在N的作用下, 轉換到非正常系統態Sempower, 達到權限提升的目的;

Sempower+R=> U, 表示當前狀態為Sempower, 在R的作用下, 轉換到用戶態U。

圖4(b)表示內部計數器觸發硬件木馬模型, 形式化表示為一個四元組(S, I, O, T), 其中:

S: 有窮非空狀態集{S0, S1, Srisk}, 其中S0, S1, S2表示正常狀態, Srisk表示安全風險狀態

I: 有窮非空輸入集{I1, I2, I3, Cclk}, 其中Cclk表示對時鐘計數到某值

O: 有窮非空輸出集{ O1, O2, O3}

T: 表示在輸入I集中某元素時, S狀態集中某兩個狀態之間的轉換函數

=>: 表示狀態轉換

狀態描述如下:

S0+ I1=> S1+ O1表示當前狀態為S0, 在輸入I1的情況下, 轉換到狀態S1, 輸出為O1;

S1+ I2=> S0+ O2表示當前狀態為S1, 在輸入I2的情況下, 轉換到狀態S0, 輸出為O2;

S0+ Crisk=> Srisk表示當前狀態為S0, 在輸入時鐘計數到Crisk的情況下, 轉換到安全風險狀態Srisk;

Srisk+ I3=> S1+ O3表示當前狀態為Srisk, 在輸入I3的情況下, 轉換到狀態S1, 輸出為O3。

3.4 安全風險驗證規則

根據3.2節表1分析結果, 得知硬件木馬直接依附于I/O端口的占到69.2%, 依附于狀態機的占到15.4%, 依附于特殊寄存器(如計數器、特權模式設置寄存器等)占到15.4%; 再結合3.3節相關定義和安全風險模型, 提出以下安全風險驗證規則。

(1) 安全風險驗證規則一

對于可疑硬件木馬位置直接依附位于端口的, 可以掃描出端口相關源代碼語句進行驗證[31]。

圖5 端口語句掃描流程圖

Figure 5 I/O port statement scan flow chart

(2) 安全風險驗證規則二

對于可疑硬件木馬位置位于狀態機的, 可通過相應工具提取出源文件中的狀態機和相關輸入變量進行驗證。

(3) 安全風險驗證規則三

對于可疑硬件木馬位置位于內部寄存器的, 則重點關注內部計數器寄存器、特殊寄存器(如用戶態到系統態轉換的寄存器)。

定義1: 在安全風險規則一、二、三下指導下掃描出的RTL源代碼為可疑硬件木馬語句。

定義2: 可疑硬件木馬語句中含有的輸入變量為觀測變量。

定義3: 對于一條可疑硬件木馬語句, 如果其作用效果可以造成安全風險中的一種或多種, 那么就說這條語句是硬件木馬語句, 否則即為誤判。

命題1: 可疑硬件木馬語句中含有的輸入變量有助于減少搜索向量空間。

證明: 假設輸入變量V[-1:0]的長度是, 則其可以表示的向量空間范圍為2。越大, 向量空間范圍越大。但是當輸入變量中的某一位是確定的, 則其向量空間范圍降為2-1。如果有兩位是確定的, 則其向量空間范圍降為2-2。依次類推, 當所有位都是確定的, 則向量空間范圍變為1, 即只含有一個向量。

如果掃描出的可疑硬件木馬語句中含有輸入端口變量, 則根據含有的輸入端口變量產生向量。提出如下算法。

3.5 基于安全風險的驗證流程

基于安全風險模型和規則, 結合仿真、模型檢驗等驗證方法[32-41], 給出了基于安全風險的驗證流程圖。

表5 基于特定位向量產生算法偽代碼

流程圖主要內容如下:

(1) 模型與規則選取

選取第三方IP核RTL源代碼, 根據結合安全風險模型和規則, 確定待驗證的源代碼范圍。

(2) 驗證方法與激勵選取

根據選取的驗證對象, 確定是采用模擬仿真的方法、還是形式化驗證方法(模型檢驗)。如果是模擬仿真的方式則需要產生激勵, 根據搜索到的RTL源代碼去指導產生相應的激勵。

(3) 具體驗證

依據上一步驟產生的激勵去驗證從正常狀態到異常狀態之間轉換是否成立, 如成立, 說明含有硬件木馬風險, 否則認為是安全的。

4 實驗

實驗意義: 根據標準測試集的分析結果, 目前RTL級硬件木馬主要存在于輸入輸出端口、狀態機和內部寄存器(如計數器、系統提權寄存器), 位于端口的占到69.2%, 如AES-T100、AES-T1000、AES-T1300和AES-T1400模塊等; 直接依附于狀態機的占到15.4%, 如RS232-T600、RS232-T700、RS232-T900和RS232-T901模塊等; 剩下的15.4%是依附在內部寄存器, 如RS232-T200、RS232-T300、AES-T1200、AES-T1500等模塊。因此在進行實驗時, 主要針對這三種情況進行實驗, 實驗具有代表性, 可以覆蓋典型的或大部分RTL級硬件木馬的問題, 對于工程實踐應用具有一定的參考價值和借鑒意義。

實驗對象: 由于Trust-Hub標準測試是有一定局限性(每個測試用例的代碼量少, 并且樣本也少等) 的, 測試集的特點如下: 首先是測試集系列(如21個AES測試用例或10個RS232測試用例系列等)案例相似度過高, 硬件木馬設計變化較小; 其次是測試集中的每個案例RTL源代碼量比較小, 行數不多, 代碼書寫特征變化形式少; 再次是輸入輸出端口數目較少, 硬件木馬的設計位置相對固定。以上這些特點在實驗時會導致誤報率和漏報率等數據的可信性欠缺, 使得實驗數據代表性減弱, 這與工程實際當中的源代碼(如代碼量大、行數多、文件數量多、代碼書寫形式豐富等)安全評估工作環境是有區別的, 所以這些特點反映了Trust-Hub測試集是有一定局限性的。

圖6 基于安全風險驗證流程圖

Figure 6 Verification flowchart based on Security risk

正是由于Trust-Hub硬件木馬集是有一定局限性(代碼量少和樣本少等)原因, 考慮到工程實際情況, 擬結合常見的開源處理器的RTL級源代碼, 針對常見的典型的三種安全風險位置, 設計了三個實驗作為對應。

實驗環境: 操作系統為win7 professional service pack 1, 實驗軟件為modelsim 10.1a, Debussy, SVA斷言, 及模型檢測工具EMBC等。

4.1 實驗一

(1) 實驗一針對依附于端口位置硬件木馬(安全風險模型一和驗證規則一)。

下面實驗對象是開源處理器OR1200的ALU算術邏輯運算單元, 它主要完成或、異或、移位、位擴展、加、減等運算。對于乘除運算, 則有專門的mult_ mac模塊來完成, 它把結果傳送給ALU[35]。OR1200開源處理器的ALU運算單元源文件是or1200_alu.v。

圖7 ALU算術邏輯運算單元連接示意圖

Figure 7 Arithmetic logic unit connection diagram

(2) 在or1200_alu. v源文件中加入硬件木馬(模仿Trust-Hub硬件木馬特征書寫)。將原來的result=a^b, 修改為result=(～(a[31]^b[20]))?a^b:0。該硬件木馬的功能是, 將ALU算術邏輯運算單元輸入的操作數a的a[31]位與輸入操作數b的b[20]位相異或, 異或完之后取反, 如果結果是1, 則硬件木馬功能不觸發, 輸出a^b結果正確; 如果是0, 則觸發硬件木馬, a^b結果取0。

(3) 通過端口掃描出相關可疑硬件木馬語句, result=(～(a[31]^b[20]))?a^b:0, 如果按照傳統的激勵產生方法則需要在232的向量空間內產生數量龐大的測試向量, 而大多數測試激勵對于問題的發現并沒有意義, 在這里只需要產生關鍵比特位a[31]=0, b[20]=1, 或a[31]=1, b[20]=0激勵向量就可以了, 因此使得測試激勵目的性變強, 測試向量空間縮小。

(4) 通過仿真驗證容易發現, 當a[31]=0, b[20]=1, 或a[31]=1, b[20]=0時, 是與原功能相違背的, 因此可以說明這條語句是有安全風險的(改變功能)。

4.2 實驗二

(1) 實驗二主要針對依附于狀態機的硬件木馬(安全風險模型二和驗證規則二)。

實驗對象是Trust-Hub標準集的RS232-T901源代碼u_xmit模塊電路, 提取狀態機得到如下圖7所示。

(2) 該硬件木馬的功能是, 當連續輸入8’hAA, 8’h00, 8’h55和8’hFF四個值時, 造成拒絕服務的安全風險。如果按照傳統驗證方法, 雖然對于8比特長的輸入變量來說, 只有256個向量取值, 完全可以全覆蓋驗證; 但是遇到圖8這種情況是難以奏效的, 因為這是多個值的組合, 而這種排列組合的空間是十分龐大的。所以采用基于安全風險分析的方法, 提取出相應狀態機及有關輸入變量取值, 驗證時, 主要驗證連續輸入8’hAA, 8’h00, 8’h55和8’hFF四個值時的情況, 針對性更強一些。

圖8 u_xmit模塊電路state_DataSend狀態機

Figure 8 state_DataSend state machine of u_xmit

4.3 實驗三

(1) 實驗三主要針對依附于特殊寄存器的硬件木馬(安全風險模型三和驗證規則三)。

OR1200處理器有兩種工作模式, 即用戶模式和特權模式。不同的模式, 對特殊寄存器的訪問權限不同。OR1200處理器的特殊寄存器訪問指令主要有l.mfspr和l.mtspr兩條指令。其中, l.mfspr指令用于讀取特殊寄存器, l.mtspr指令用于寫入特殊寄存器, l.sys 0x01是系統調用指令。

對or1200_ctrl.v文件中的原代碼sig_syscall <= (id_insn[31:23]=={`OR1200_OR32_XSYNC, 3'b000})進行修改為如下所示:

sig_syscall<=(id_insn[31:23]=={′OR1200_OR32_XSYNC,3'b000})||((if_insn[31:26]==6'b111000)&&(id_insn[31:26]==6'b000110))。

or1200_ctrl.v原代碼是未加入硬件木馬的, 意思是說遇到系統調用指令l.sys時才產生系統調用信號。加入硬件木馬時, 則是遇到l.movhi(操作碼為6'b000110)和l.add(操作碼為6'b111000)組合指令序列, 考慮到流水線的作用, 當處于譯碼寄存器id_insn[31:26]的是l.movhi指令, 取指寄存器if_insn[31:26]是l.add指令, 則觸發硬件木馬進行系統調用, 以實現提升權限操作。

下邊給出了一段設計程序來說明問題。

.section .text,"ax"

.org 0x100

.global _start

_start:

l.movhi r0,0 #初始化r0-r4寄存器, 全部清零

l.movhi r1,1

l.add r1,r1,r0

l.nop 0x0001

.org 0xc00 #0xc00就是系統調用入口

l.mfspr r1,r0,0x20

l.mfspr r1,r0,0x40

l.nop 0x0001

在以上實驗程序中并沒有含有系統調用指令l.sys。在沒有硬件木馬時, 以上程序不應該產生系統調用操作, 但是在加入硬件木馬時, 則會產生與系統調用指令l.sys相同的功能, 達到提升權限的目的。

(2) 目前指令集一般都含有上百條、甚至幾百條指令, 對一條指令的功能驗證是容易的, 但是對于指令集組合所產生的功能進行驗證, 這個驗證空間是十分龐大的, 為此, 對關鍵寄存器進行關注是十分必要的。

對于(1)中的這種情況, sig_syscall是重點關注的寄存器, 設置了如下斷言:

@(posedge clk) $rose(sig_syscall);

來監測系統調用的次數。在沒有加入硬件木馬時, 斷言監測系統調用的次數為0次; 在加入硬件木馬后, 雖然沒有系統調用指令, 但是監測到還是有1次系統調用的信號, 這說明是硬件木馬觸發的。

通過采用安全風險模型和安全風險驗證規則, 在以上三個實驗基礎上進行了拓展, 以開源CPU代碼or1200(or1200_alu.v和or1200_ctrl.v)、turbo8051(oc8051_alu.v)、M32632(M32632.v)、a-z80(alu.v)的源文件為實驗對象(這些源代碼更接近于真實情況, 對這些代碼仿照標準集木馬, 在源代碼中插入硬件木馬)說明, 如表6所示(TPR表示正檢率, FPR表示誤報率, FNR表示漏報率)。

表6 基于安全風險驗證數據

4.4 分析與比較

基于安全風險驗證可以將評估驗證范圍縮小, 但是不可避免地存在著誤報和漏報的問題。

產生誤報的原因是因為在對端口語句搜索的結果中, 含有和硬件木馬接近的表達邏輯, 所以被誤識別成硬件木馬。例如源文件or1200_ctrl.v的誤報率比源文件or1200_alu.v的高, 主要原因在于or1200_ ctrl.v是CPU的控制器模塊, 它里面含有豐富多樣的控制信號, 如鎖流水線信號wb_freeze、系統調用信號sig_syscall、讀信號ex_spr_read、寫信號ex_spr_ write, 以上信號都是基本上都是由多個變量的組合邏輯表達式構成, 與硬件木馬表現特征近似, 導致誤判, oc8051_alu.v、M32632.v、alu.v也存在同樣的問題。產生漏報的原因是主要是對于狀態機較多、內部寄存器較多的情況, 安全風險模型和驗證規則難以覆蓋到所有的狀態機和內部寄存器。如or1200_ctrl.v文件有數十個狀態機和將近四十個內部寄存器, 對于驗證而言, 哪些是關鍵寄存器, 哪些不是關鍵寄存器, 目前尚欠缺比較明確的劃分方式, 本文重點關注計數器和權限提升寄存器, 并且硬件木馬采用隨機插入方式, 這樣導致在驗證過程中遺漏相關內部寄存器。

對于RTL級硬件木馬問題研究, 由于研究人員觀察角度不同, 所以采用的方法也不同, 因此, 本文在與其他方法(比較典型的是文獻[28]、[29] 、[30])比較時采用了定性分析的方法。

文獻[28]通過采用控制流圖方法來檢測RTL級硬件木馬, 將RTL源代碼中的硬件木馬抽象成cheat code、dead machine、ticking timebomb三類模型, 然后對分析的RTL源代碼提取出相應的代碼段與模型做匹配。這種方法本質是借鑒軟件木馬匹配檢測的方法, 這種方法具有局限性, 主要是因為硬件木馬的設計與軟件木馬具有很大的區別。例如, 軟件木馬是一個相對完整的程序, 它由一個或多個源文件構成, 通過對整個程序或關鍵文件進行哈希匹配運算, 即可得到該軟件木馬的特征。相反地, 硬件木馬在RTL級上的設計不需要像軟件木馬一樣, 它只需在源文件中添加一條語句(甚至只修改原文件中一條語句的參數), 或幾條語句就可以完成植入任務, 進一步而言, 只要修改硬件描述語言中的參數, 而不修改語句的表達式結構, 就在另一個源文件中完成另外一個硬件木馬的植入。因此說可以吸取軟件木馬特征匹配方法的思想, 但是具體到硬件木馬檢測和驗證時, 應該重點關注其結構表達特征。再者, 文獻[28]的提取算法(Extraction Algorithm)和檢測算法(Detection Algorithm)相對比較復雜, 在提取算法中, 需要提取和生成RTL源代碼中的控制流圖, 并且還要生成硬件木馬特征庫, 以便于比較檢測, 這就涉及分析RTL源代碼的邏輯功能, 如if-then(-else)結構, 這將會導致問題復雜化, 不同的RTL源代碼的控制流圖是有很大區別的, 不可避免地導致計算量和耗費開銷增加。而本文方法只是將RTL源代碼作為文本來進行分析, 從文本語義角度進行檢測, 對于不同的RTL源代碼分析方法和復雜程序是一樣的, 分析和檢測算法相對簡單, 適用范圍相對廣泛, 這與工程實際的要求是相吻合的。

文獻[29]主要采用形式化方法, 即模型檢驗來檢測硬件木馬, 關于模型檢驗方法的使用, 會不可避免的遇到狀態空間爆炸問題, 雖然對于某些特定問題可以比較好的解決, 但是對于實際工程中文件數量眾多、變量眾多、狀態空間多的情況則難以適應。如對實驗二的依附于狀態機的硬件木馬的檢測問題, 及實驗三中的組合指令實現系統提權的問題, 則采用模型檢測方法難以奏效。文獻[29]主要用來檢測信息泄漏類型的硬件木馬, 沒有提及到功能改變、芯片破壞、拒絕服務和系統提權等危害類型。進一步而言, 模型檢驗方法本質上也是標準的芯片驗證方法, 主要從正面驗證芯片功能的正確性, 但是, 前而已經提及, 攻擊者設計的木馬類型多樣、隱蔽性強, 一般很難通過常規的、傳統的驗證方法發現。為此, 本文本質上是利用了硬件木馬的分布概率規律, 包括危害類型、安全風險位置、及危害類型和安全風險之間的關系等, 通過利用這些先驗知識, 來減少驗證的盲目性, 提高檢測和驗證硬件木馬的成功率。

文獻[30]設計的硬件木馬是通過破壞RISC處理器的棧指針(stack pointer)來達到攻擊的目的。正常情況下, 主要是CALL調用指令、RET指令和RESET指令來修改棧指針, 該文獻設計的硬件木馬則是, 當指令寄存器的值在0x4～0xB范圍內, 并且這種情況出現100次, 則會觸發硬件木馬。如果從本文的角度來分析, 則屬于第三種安全風險類型, 并且與實驗三很類似。在實驗三中已經提出, 由于指令集一般有上百條指令甚至幾百條指令, 隨機組合的空間更為龐大, 那么在文獻[30]中也存在同樣的問題, 所以按照傳統的驗證方式是難以奏效的。文獻[30]主要是針對一種修改數據的類型的木馬, 需要與指令集、軟件編程仿真相結合, 相對而言, 硬件木馬表現形式比較單一, 危害形式只有一種, 即改變功能, 與工程實際情況差別較大。如果利用本文安全風險模型三, 把棧指針寄存器和指令寄存器當作關鍵的驗證寄存器, 通過對RTL源代碼的分析和驗證, 則評估效率和驗證效率應該會有所提高。

總之, 本文的研究主要是面向源代碼安全性評估的工作, RTL級源文件數量比較多, 在這種情況下, 如果采用傳統的驗證方法難以找到重點, 再加上即使源文件中真得含有安全風險, 一般設計也比較隱蔽, 如果對源代碼不加以區分, 對代碼做安全評估是有困難的。

因此, 本文在分析硬件木馬標準集的基礎上, 給出相關定義, 提煉出安全風險模型和安全風險位置, 制定出相應的安全風險驗證規則, 在以上先驗知識的基礎上, 結合RTL源文件的語義分析, 避開傳統直接驗證的方式方法, 這樣做可以盡量避免狀態空間爆炸、向量空間膨脹等問題, 降低驗證人力、物力、財力和時間成本。與其他方法相比較而言, 適合于對外來第三方IP核源代碼做前期安全性評估, 有助于將可疑代碼范圍縮小, 降低盲目性, 增強針對性, 提高評估效率。當然, 本文的研究還存在精細程度和深入程度還不夠, 如對安全風險規則三當中的重點關注寄存器確定問題, 需要結合相關研究方法進一步提高。

5 總結與展望

當前, 關于第三方IP核源代碼安全評估問題, 即是否含有硬件木馬, 如何進行驗證, 是新的研究點, 同時也是難點。

針對目前RTL級源代碼安全評估及硬件木馬驗證研究缺少安全風險模型和指導規則, 在對硬件木馬集進行分析的基礎上, 給出了相關模型、定義和安全風險驗證規則。

文章試圖在面臨RTL源代碼安全評估時, 提出了基于安全風險模型和安全風險規則的驗證評估, 減少驗證盲目性, 縮小可疑代碼范圍, 提高工作效率。實驗證明, 安全風險模型和規則對RTL級硬件木馬驗證具有一定的效果。

致 謝 本文是在信息工程研究所第五研究室多位老師指導下完成的, 在此表示誠摯感謝。另外, 對于審稿專家的意見和建議, 表示衷心感謝！

[1] Jiang P, Li D J. Information confrontation[M]. Beijing: Tsinghua University Press, 2007: 1-11. (蔣平, 李冬靜. 信息對抗[M]. 北京: 清華大學出版社, 2007: 1-11.)

[2] McAfee Corp. New Paradigm Shift: Comprehensive Security beyond the Operating System., 2012, 2-9.

[3] Kauer B. OSLO: Improving the Security of Trusted Computing[J]., 2007: 229-237.

[4] A.Sanjaya, Hardware Assisted Security: Anticipating Digital Threat and Challenges[C]., 2012: 1-10.

[5] Agrawal D, Baktir S, Karakoyunlu D, et al. Trojan Detection Using IC Fingerprinting[C]., 2007: 296-310.

[6] Di J, Smith S. A Hardware Threat Modeling Concept for Trustable Integrated Circuits[C]., 2007: 354-357.

[7] Wang X X, Tehranipoor M, Plusquellic J. Detecting Malicious Inclusions in Secure Hardware: Challenges and Solutions[C]., 2008: 15-19.

[8] Hu W, Oberg J, Irturk A, et al. On the Complexity of Generating Gate Level Information Flow Tracking Logic[J]., 2012, 7(3): 1067-1080.

[9] Hu W, Oberg J, Irturk A, et al. Theoretical Fundamentals of Gate Level Information Flow Tracking[J]., 2011, 30(8): 1128-1140.

[10] Zhou B, Zhang W, Thambipillai S, et al. Cost-Efficient Acceleration of Hardware Trojan Detection through Fan-out Cone Analysis and Weighted Random Pattern Technique[J]., 2016, 35(5): 792-805.

[11] Liu C, Cronin P, Yang C M. A Mutual Auditing Framework to Protect IoT Against Hardware Trojans[C]., 2016: 69-74.

[12] Dupuis S, Ba P S, Di Natale G, et al. A Novel Hardware Logic Encryption Technique for Thwarting Illegal Overproduction and Hardware Trojans[C]., 2014: 49-54.

[13] Zhou E R, Li S Q, Zhao Z X, et al. Nonlinear Analysis for Hardware Trojan Detection[C].,, 2015: 1-4.

[14] L.W Wang, H.W. Luo and R.H. Yao, A hardware Trojan detection method based on bypass analysis[J] ., 2012, 40(6): 9. (王力緯, 羅宏偉, 姚若河.基于旁路分析的硬件木馬檢測方法[J] ., 2012, 40(6): 9.)

[15] Kumar P, Srinivasan R. Detection of Hardware Trojan in SEA Using Path Delay[C].',, 2014: 1-6.

[16] Moore T D, Jarvis J L. Failure Analysis and Stress Simulation in Small Multichip BGAs[J]., 2001, 24(2): 216-223.

[17] Chakraborty R S, Wolff F, Paul S, et al. MERO: A Statistical Approach for Hardware Trojan Detection[C]., 2009: 396-410.

[18] Cak?r B, Malik S. Hardware Trojan Detection for Gate-Level ICs Using Signal Correlation Based Clustering[C].,, 2015: 471-476.

[19] Bao C X, Forte D, Srivastava A. On Application of One-Class SVM to Reverse Engineering-Based Hardware Trojan Detection[C]., 2014: 47-54.

[20] Hasegawa K, Oya M, Yanagisawa M, et al. Hardware Trojans Classification for Gate-Level Netlists Based on Machine Learning[C]., 2016: 203-206.

[21] Wang C G, Cai Y C, Zhou Q. Automatic Security Property Generation for Detecting Information-Leaking Hardware Trojans[C]., 2017: 321-328.

[22] Lodhi F K, Abbasi I, Khalid F, et al. A Self-Learning Framework to Detect the Intruded Integrated Circuits[C]., 2016: 1702-1705.

[23] Dai Y Y, Braytont R K. Circuit Recognition with Deep Learning[C]., 2017: 162.

[24] Zareen F, Karam R. Detecting RTL Trojans Using Artificial Immune Systems and High Level Behavior Classification[C]., 2019: 68-73.

[25] Zhang J, Xu Q. On Hardware Trojan Design and Implementation at Register-Transfer Level[C]., 2013: 107-112.

[26] Banga M, Hsiao M S. Trusted RTL: Trojan Detection Methodology in Pre-Silicon Designs[C]., 2010: 56-59.

[27] Piccolboni L, Menon A, Pravadelli G. Efficient Control-Flow Subgraph Matching for Detecting Hardware Trojans in RTL Models[J]., 2017, 16(5s): 1-19.

[28] Rajendran J, Dhandayuthapany A M, Vedula V, et al. Formal Security Verification of Third Party Intellectual Property Cores for Information Leakage[C]., 2016: 547-552.

[29] Rajendran J, Vedula V, Karri R. Detecting Malicious Modifications of Data in Third-Party Intellectual Property Cores[C]., 2015: 1-6.

[30] J.F. Zhao, G. Shi. Cheng. Research on RTL level Hardware Trojan., 2020. (趙劍鋒, 史崗.RTL級硬件木馬問題研究[J].,2020.)

[31] Cheng X, Li L, Cheng W. A Detection Method of Hardware Trojans Based on RTL[J]., 2017, 34(3): 56-60. (成祥, 李磊, 程偉. 基于RTL級硬件木馬的檢測方法[J]., 2017, 34(3): 56-60.)

[32] Zhao J F, Shi G. A Survey on the Studies of Hardware Trojan[J]., 2017, 2(1): 74-90. (趙劍鋒, 史崗. 硬件木馬研究動態綜述[J]., 2017, 2(1): 74-90.)

[33] Clarke E M. Automatic Verification of Finite-State Concurrent Systems[C]., 2002: 126.

[34] Allen Emerson E, Halpern J Y. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time[J]., 1985, 30(1): 1-24.

[35] Ehrhard T. Linear logic in computer science[M]. Cambridge: Cambridge University Press, 2004

[36] Lei S L. Step by step “core”: Analysis of internal design of soft core processor[M]. Beijing: Publishing House of Electronics Industry, 2013. (雷思磊. 步步驚“芯”: 軟核處理器內部設計分析[M]. 北京: 電子工業出版社, 2013.)

[37] S. Vijayaraghavan and M. Ramanathan. A practical Guide for System Verilog Assertions[M]., 2005, 1-100.

[38] Damjan Lampret. OpenRISC 1200 IP Core Specification. http:// www.opencore.org. 2017.

[39] OpenRISC 1000 Architecture Manual. http://www.opencore.org. 2017.

[40] Yeung P, Larsen K. Practical Assertion-Based Formal Verification for SoC Designs[C]., 2006: 58-61.

[41] Karunakaran D K, Mohankumar N. Malicious Combinational Hardware Trojan Detection by Gate Level Characterization in 90nm Technology[C].,, 2014: 1-7.

Research on RTL Level Hardware Trojan Verification Based on Security Risk

Zhao Jianfeng1,2, Shi Gang2

1School of Cybersecurity, University of Chinese Academy of Sciences, Beijing 100049, China2Institute of Information Engineering, Chinese Academy of Sciences, Beijing 100093, China

With the advent of the information age, information security has become increasingly important. In order to obtain the desired information, attackers not only use software means, such as viruses, worms, software trojans, but also use hardware means to threaten the security of devices, systems and data, such as hardware Trojans embedded in chips. If the hardware Trojan horse is embedded in the processor, which is the core of information processing, the risk will be higher and the harm will be greater. However, the hardware Trojan horse is located at the bottom of the information system core level, which is difficult to detect and discover. Hardware Trojan Horse is a hot topic in academic circles at home and abroad. Especially in the design stage, the problem of hardware Trojan Horse detection combined with source code is not only a new problem, but also a necessary one. This paper is based on the above background and combined with the actual needs of domestic chip RTL source code security risk assessment to carry out related work, mainly for the detection and verification of hardware Trojan in RTL source code. The main contents and contributions of this paper are as follows. Aiming at the problem that RTL level hardware Trojan has not yet given its characteristic attributes academically, the description form of hardware Trojan's attribute is given Based on the harm result attribute of Hardware Trojan, the model and verification rules based on security risk are put forward academically, and the corresponding description form is given, this paper theoretically explains the role of security verification rules in reducing the blindness of verification, reducing the scope of suspicious code, and improving the efficiency of evaluation, it can avoid the blindness of verification and the expansion of test space vector, and effectively verify the existence and harm of suspected hardware Trojans, which is effective for RTL source code security assessment.

chip; RTL level hardware trojan; security risk; verification rules

TP309.2

10.19363/J.cnki.cn10-1380/tn.2022.12.08

趙劍鋒, 博士研究生, 講師, Email: zhaojianfeng@iie.ac.cn。

本課題得到國家“核高基”科技重大專項基金項目(No.2013ZX01029003-001); 國家“八六三”高技術研究發展計劃基金項目(No.2012AA01A401)資助。

2020-05-03;

2020-06-12;

2022-12-07

趙劍鋒 于2006年在北京理工大學通信與信息系統專業獲得碩士學位?，F在中國科學院信息工程研究所計算機系統結構專業攻讀博士學位。研究領域為計算機系統安全。研究興趣包括: 架構安全。Email: zhaojianfeng@iie.ac.cn

史崗 于2004年在中國科學院計算技術研究所獲得博士學位?，F任中國科學院信息工程研究所第五研究室高級工程師。研究領域為計算機系統安全。研究興趣包括: 嵌入式系統、信息安全。Email: shigang@ iie.ac.cn