基于信息流分析的密碼核設(shè)計(jì)安全驗(yàn)證與漏洞檢測(cè)

馬藝新, 唐時(shí)博, 譚靜, 李雪霏, 胡偉

(西北工業(yè)大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院, 陜西 西安 710072)

密碼技術(shù)是網(wǎng)絡(luò)與信息安全的重要支撐性技術(shù),是用于保障信息機(jī)密性和完整性等關(guān)鍵屬性的重要手段。密碼算法在數(shù)學(xué)上的安全性與其實(shí)現(xiàn)的安全性是2個(gè)截然不同的問題。雖然密碼算法的安全性已經(jīng)從數(shù)學(xué)上得到證明,但是,密碼算法核實(shí)現(xiàn)會(huì)由于設(shè)計(jì)錯(cuò)誤、旁路信道[1]、調(diào)試接口[2]或后門程序[3]等原因引入安全漏洞。這些安全漏洞一旦被攻擊者挖掘與利用,將能夠在較低時(shí)間和空間復(fù)雜度條件下完全恢復(fù)算法保密密鑰。攻擊者可進(jìn)一步利用密鑰竊取更多有價(jià)值的信息,使得密碼算法核以及計(jì)算設(shè)備的安全性受到嚴(yán)重威脅。

在密碼核硬件電路設(shè)計(jì)過程中,驗(yàn)證的時(shí)間開銷往往達(dá)到總工作量的40%～70%[4]。功能驗(yàn)證的局限性在于:覆蓋率依賴于測(cè)試激勵(lì)信號(hào)，導(dǎo)致驗(yàn)證覆蓋率低、驗(yàn)證不充分;設(shè)計(jì)規(guī)模很大或要模擬的情況很多時(shí)通常會(huì)導(dǎo)致模擬時(shí)間會(huì)很長(zhǎng),驗(yàn)證效率低。密碼算法核中的高隱蔽性安全漏洞,單純依靠有限次的功能測(cè)試很難保證可以覆蓋。由此可見,功能驗(yàn)證難以滿足密碼算法核的安全驗(yàn)證需求。

信息流跟蹤(information flow tracking,IFT)方法通過為存儲(chǔ)對(duì)象添加安全標(biāo)簽，并通過計(jì)算與跟蹤存儲(chǔ)對(duì)象的標(biāo)簽執(zhí)行信息流安全策略去驗(yàn)證、控制整個(gè)硬件系統(tǒng)的信息流動(dòng)[5]。信息流跟蹤方法具有良好的信息流監(jiān)控能力,可以防止有害的信息流動(dòng)。Tiwari等[6]提出了門級(jí)信息流跟蹤(gate level information flow tracking,GLIFT)方法。GLIFT方法通過為每個(gè)二進(jìn)制位數(shù)據(jù)分配一比特的標(biāo)簽精確地監(jiān)控每個(gè)二進(jìn)制位信息的流動(dòng),是一種細(xì)粒度的信息流控制方法,能夠通過捕捉有害的信息流動(dòng)來檢測(cè)和消除設(shè)計(jì)中潛在的安全漏洞。Ferraiuolo等[7]設(shè)計(jì)了一種帶類型系統(tǒng)的安全Verilog語言SecVerilog,通過在設(shè)計(jì)編譯階段靜態(tài)檢查不同安全級(jí)別數(shù)據(jù)之間的信息流安全屬性,給出了一種驗(yàn)證處理器架構(gòu)中安全域和非安全域之間隔離特性的方法。Jin等提出了一種基于攜帶證明代碼的硬件安全驗(yàn)證框架,硬件知識(shí)產(chǎn)權(quán)(intellectual property,IP)核攜帶了安全屬性相關(guān)的定理,可利用Coq進(jìn)行安全定理證明,從而檢測(cè)第三方IP核中潛在的木馬設(shè)計(jì)[8-9]。Ardeshiricham等[10]提出了寄存器傳輸級(jí)信息流跟蹤(register transfer level information flow tracking,RTLIFT)方法,它能夠直接在寄存器傳輸級(jí)(register transfer level,RTL)代碼的基礎(chǔ)上生成精確的IFT邏輯,進(jìn)行安全驗(yàn)證。

現(xiàn)有的安全驗(yàn)證方法需要設(shè)計(jì)者用新的語言重新編寫硬件模型,或者需要設(shè)計(jì)新的驗(yàn)證框架,或者由于抽象層次低不能擴(kuò)展到大的設(shè)計(jì)。本文從信息流安全的角度研究密碼算法核安全驗(yàn)證與漏洞檢測(cè)方法,基于信息流分析的安全驗(yàn)證方法只需要掌握密碼算法核的RTL級(jí)源碼或門級(jí)網(wǎng)表,在RTL級(jí)源碼或者門級(jí)網(wǎng)表的基礎(chǔ)上描述信息流和標(biāo)簽的傳播,不需要設(shè)計(jì)者學(xué)習(xí)新的硬件安全語言。本文利用可實(shí)現(xiàn)形式化驗(yàn)證功能的綜合工具Yosys,它支持自定義信息流安全屬性,在定義不同信息流關(guān)系時(shí)更加靈活,例如,顯式流還是隱式流,并且在較高的抽象層次上工作會(huì)提高驗(yàn)證速度。

本文通過對(duì)Aoki Laboratory[11]發(fā)布的密碼算法核中全部邏輯信息流進(jìn)行精確度量,對(duì)機(jī)密性、完整性等安全屬性進(jìn)行形式化驗(yàn)證,可捕捉到電路中的有害信息流,對(duì)密碼算法核中的安全漏洞以及時(shí)間側(cè)信道有很好的檢測(cè)效果。

1 背景

1.1 硬件信息流分析

信息流是指信息的流動(dòng)和傳播,在本文中信息流均代表與硬件設(shè)計(jì)系統(tǒng)邏輯狀態(tài)密切相關(guān)的邏輯信息流。硬件信息流分析中,數(shù)據(jù)通常被賦予一個(gè)標(biāo)簽,該標(biāo)簽表征數(shù)據(jù)的安全屬性,如可信/不可信或保密/非保密。在數(shù)據(jù)運(yùn)算過程中標(biāo)簽隨之在電路中傳播,硬件信息流分析中標(biāo)簽傳播策略是根據(jù)當(dāng)前操作類型、輸入以及輸入標(biāo)簽來確定輸出的標(biāo)簽,通過靜態(tài)分析或動(dòng)態(tài)檢查輸出的標(biāo)簽,可以有效防止違反信息流安全策略的運(yùn)算操作,防止有害信息流的流動(dòng),例如:保密信息流向了電路中非保密區(qū)域數(shù)據(jù)寄存器,可信區(qū)域程序計(jì)數(shù)器中接收到了來自以太網(wǎng)的不可信數(shù)據(jù)。

如表1所示,以密碼算法核為例詳細(xì)介紹標(biāo)簽傳播規(guī)則。密碼算法核中密鑰與輸入進(jìn)行與操作,密鑰與輸入均為一比特,密鑰為K,輸入為M,輸出為O=K&M,kt,mt和ot為密鑰、輸入和輸出的標(biāo)簽。K,M∈{0,1},kt,mt,ot∈{LOW,HIGH},其中標(biāo)簽“LOW”代表密碼算法核中低安全級(jí)別屬性非保密或者可信,標(biāo)簽“HIGH”代表密碼算法核中高安全級(jí)別安全屬性保密或者不可信。

假定L(a)為信號(hào)a的信息流跟蹤邏輯,當(dāng)at=1時(shí),L(a)=HIGH,當(dāng)at=0時(shí),L(a)=LOW。在運(yùn)算操作中對(duì)輸出起關(guān)鍵決策作用的輸入的標(biāo)簽決定了輸出的標(biāo)簽,例如輸入A的標(biāo)簽為HIGH,A=0,輸入B的標(biāo)簽為L(zhǎng)OW,B=1,A為0決定了輸出為0,所以輸出標(biāo)簽由A安全級(jí)別決定,輸出標(biāo)簽為HIGH。由表1可以推導(dǎo)出密碼算法核中二輸入與門的信息流跟蹤邏輯為(1)式。

表1 密碼算法核中與操作的標(biāo)簽傳播規(guī)則

ot=Mkt+Kmt+ktmt

(1)

類似地,可以得到密碼算法核中其他基本邏輯門如非門、或門和異或門等基本邏輯單元的信息流模型,從而可以構(gòu)建信息流模型庫。根據(jù)信息流模型庫可以為密碼算法核的每一個(gè)邏輯單元離散式地生成信息流模型,從而為整個(gè)密碼算法核設(shè)計(jì)生成信息流模型。

1.2 信息流安全驗(yàn)證

安全驗(yàn)證是一種在流片前對(duì)硬件設(shè)計(jì)進(jìn)行的基于屬性的邏輯驗(yàn)證,安全驗(yàn)證能夠證明一些被定義好的安全屬性在硬件設(shè)計(jì)中是否一直成立。根據(jù)具體方法的不同,進(jìn)行安全驗(yàn)證的硬件設(shè)計(jì)可能是RTL級(jí)代碼或者邏輯門級(jí)網(wǎng)表。

基于硬件信息流分析的安全驗(yàn)證是檢測(cè)密碼算法核安全漏洞的一種手段。假設(shè)密碼算法核中包含安全漏洞,密碼算法核正常運(yùn)行產(chǎn)生正確的運(yùn)算結(jié)果,并不會(huì)觀察到安全漏洞,只有在罕見的情況下,例如違反電路機(jī)密性(如密鑰泄露至輸出)時(shí),安全漏洞才會(huì)被觀察到。安全漏洞難以通過有限次的功能驗(yàn)證被覆蓋,信息流分析方法則可取得更好的檢測(cè)效果。

在安全屬性的定義中,機(jī)密性屬性主要是保證高安全級(jí)別敏感信息不會(huì)流向密碼算法核中可公開觀測(cè)的區(qū)域。標(biāo)準(zhǔn)硬件描述語言Verilog和VHDL只能描述功能屬性,不能用于描述安全屬性。信息流分析中關(guān)注信息的流動(dòng),更好地描述了機(jī)密性、完整性等安全屬性,安全屬性可采用斷言語言描述。

圖1描述了信息流安全驗(yàn)證方法。密碼算法核可以作為安全驗(yàn)證的檢測(cè)對(duì)象,該方法分析了密碼算法核中需滿足的通用安全屬性,如機(jī)密性、完整性、隔離特性以及一些模式相關(guān)的屬性等。將安全屬性映射至密碼算法核的安全驗(yàn)證模型上,主要進(jìn)行屬性相關(guān)信號(hào)安全級(jí)別的劃分和安全屬性標(biāo)簽的實(shí)例化,以及安全屬性中斷言語句向功能性驗(yàn)證語言的轉(zhuǎn)化。完成安全屬性的映射之后,即可結(jié)合密碼算法核的信息流模型,采用形式化驗(yàn)證工具實(shí)現(xiàn)安全屬性的驗(yàn)證,若驗(yàn)證失敗則表明存在安全漏洞,同時(shí)會(huì)生成一個(gè)反例,可用于漏洞復(fù)現(xiàn)。

圖1 密碼算法核安全驗(yàn)證方法

2 密碼核安全驗(yàn)證與漏洞檢測(cè)方法

2.1 密碼算法核信息流模型的生成

在1.1節(jié)為密碼算法核中基本邏輯門構(gòu)造信息流模型的基礎(chǔ)上,可以構(gòu)造一個(gè)功能完備的信息流模型庫,通過為密碼算法核中更復(fù)雜的功能單元生成信息流模型,最終生成整個(gè)密碼算法核的信息流模型。

如圖2所示,生成密碼算法核的信息流模型首先需要構(gòu)建一個(gè)包含基本邏輯單元如與門、或門、非門等的信息模型庫。給定一個(gè)邏輯函數(shù),首先使用邏輯綜合工具將其綜合為由基本邏輯單元描述的門級(jí)網(wǎng)表,例如圖2中將二輸入選擇器邏輯函數(shù)轉(zhuǎn)化為由2個(gè)與門和1個(gè)或門描述的門級(jí)網(wǎng)表;然后將門級(jí)網(wǎng)表映射至基本邏輯單元信息流模型庫中,為門級(jí)網(wǎng)表中的各個(gè)邏輯單元實(shí)例化信息流模型,生成了邏輯函數(shù)的信息流模型。圖2中生成了二輸入選擇器的信息流模型;當(dāng)使用信息流模型生成算法為邏輯函數(shù)生成信息流模型后,將邏輯函數(shù)的信息流模型集成至基本邏輯單元信息流模型庫中,將基本信息流模型庫擴(kuò)充至復(fù)雜信息流模型庫;對(duì)密碼算法核而言,可使用同樣的方法,經(jīng)過邏輯綜合生成門級(jí)網(wǎng)表,將門級(jí)網(wǎng)表中各個(gè)邏輯單元映射至復(fù)雜硬件信息流模型庫,為密碼算法核中各個(gè)邏輯單元實(shí)例化地附加信息流模型,由此生成整個(gè)密碼算法核的信息流模型。

圖2 密碼算法核信息流模型的生成

2.2 安全屬性

對(duì)密碼算法核進(jìn)行安全驗(yàn)證的前提是分析電路所需遵循的安全屬性,如機(jī)密性、完整性、隔離特性以及時(shí)間信道等。首先需要描述所需驗(yàn)證的安全屬性,通常借鑒SystemVerilog Assertion等斷言描述語言的語義,并拓展安全相關(guān)的特性。安全屬性描述語言常用的關(guān)鍵字,主要包含安全級(jí)別的設(shè)置、安全屬性的斷言、斷言條件的設(shè)置以及許可路徑的設(shè)定。關(guān)鍵字set用來設(shè)置信號(hào)安全級(jí)別,如保密、公開、可信、不可信等,關(guān)鍵字assert用來斷言信號(hào)安全級(jí)別。

在安全屬性描述語言的基礎(chǔ)上,可以對(duì)密碼算法核中通常需要滿足的安全屬性進(jìn)行描述。完整性屬性保證高安全級(jí)別的不可信信號(hào)不會(huì)流向低安全級(jí)別的可信區(qū)域;機(jī)密性屬性保證高安全級(jí)別的保密信號(hào)不會(huì)流向可公開觀測(cè)的區(qū)域。在機(jī)密性驗(yàn)證中將保密信號(hào)設(shè)置為高安全級(jí)別HIGH,并斷言其不會(huì)流向低安全級(jí)別LOW的輸出。例如,斷言密鑰不應(yīng)該流向中間數(shù)據(jù)寄存器,描述如下:

set key=HIGH

assert data-reg==LOW

將安全屬性描述語言轉(zhuǎn)化為形式化驗(yàn)證工具Yosys可以識(shí)別的安全約束,即進(jìn)行安全標(biāo)簽的設(shè)置,以及屬性相關(guān)信號(hào)安全級(jí)別的劃分與設(shè)置,具體如下所示:

assign key-t= 1′b1

assert data-reg-t== 1′b0

2.3 安全驗(yàn)證與漏洞檢測(cè)

Yosys是種基于Verilog的開源綜合與驗(yàn)證工具,該工具在命令行窗口下啟動(dòng)和運(yùn)行。它可以將Verilog代碼綜合為邏輯門級(jí)網(wǎng)表,內(nèi)置用于檢查安全屬性和功能的布爾可滿足性(boolean satisfiability problem,SAT)求解器。

圖3描述了密碼算法核安全驗(yàn)證與漏洞檢測(cè)方案。首先將密碼算法核通過Yosys綜合生成邏輯門級(jí)網(wǎng)表,然后根據(jù)2.1節(jié)的信息流模型生成方法,對(duì)門級(jí)網(wǎng)表進(jìn)行分析,對(duì)門級(jí)網(wǎng)表中的邏輯單元進(jìn)行處理,包括信號(hào)端口定義、基本邏輯門、寄存器、觸發(fā)器以及賦值語句等,為門級(jí)網(wǎng)表中的每個(gè)邏輯單元實(shí)例化信息流模型,最終生成整個(gè)密碼算法核的信息流模型。

圖3 密碼算法核安全驗(yàn)證與漏洞檢測(cè)方案

密碼算法核信息流模型是安全驗(yàn)證的基礎(chǔ)。通過對(duì)密碼算法核進(jìn)行安全需求分析,建立密碼算法核安全屬性庫,將密碼算法核需滿足的安全規(guī)范使用安全屬性描述語言進(jìn)行描述,然后對(duì)密碼算法核中屬性相關(guān)信號(hào)進(jìn)行安全等級(jí)的劃分,其次通過信號(hào)安全標(biāo)簽的設(shè)置,指定允許或禁止的信息流,通常采用斷言語句進(jìn)行信息流的禁止或許可。這些安全屬性斷言被寫入密碼算法核信息流模型中,用于驗(yàn)證信息流安全流動(dòng)。例如,機(jī)密性驗(yàn)證中需要將保密信號(hào)設(shè)置為高安全級(jí)別HIGH,并禁止它流向低安全級(jí)別LOW的輸出。假設(shè)密鑰不應(yīng)該被泄露,將密鑰安全屬性標(biāo)記為HIGH,其他信號(hào)安全屬性標(biāo)記為L(zhǎng)OW,因?yàn)檫@是一個(gè)關(guān)于機(jī)密性的屬性,需要檢查密文有效信號(hào)是否始終為L(zhǎng)OW,這種安全屬性的驗(yàn)證描述如下:

set key-t HIGH

set DEAFAULT-LABEL LOW

assert cipher-ready-t LOW

將安全屬性轉(zhuǎn)化為Yosys可識(shí)別的安全約束腳本或文件,結(jié)合寫入安全屬性斷言的信息流模型,調(diào)用Yosys驗(yàn)證工具進(jìn)行安全驗(yàn)證,分析密碼算法核安全驗(yàn)證模型中安全屬性以及敏感信息的流動(dòng),觀察待驗(yàn)證的安全屬性標(biāo)簽信號(hào)值。根據(jù)Yosys驗(yàn)證的結(jié)果判斷是否存在違反信息流安全規(guī)范的信息流動(dòng),若驗(yàn)證成功則不存在安全漏洞,若驗(yàn)證失敗則通過分析驗(yàn)證失敗時(shí)相關(guān)信號(hào)的值,對(duì)安全漏洞特征進(jìn)行分析以及定位,結(jié)合驗(yàn)證工具給出的反例對(duì)信息流模型進(jìn)行功能測(cè)試,可獲得密碼算法核中安全漏洞的泄露途徑以及漏洞行為。

3 實(shí)驗(yàn)與分析

3.1 實(shí)驗(yàn)環(huán)境與方案

硬件環(huán)境為英特爾i7處理器,16 GB內(nèi)存。軟件環(huán)境為64位Ubuntu 20.04.1操作系統(tǒng),編譯器為gcc 9.3.0。實(shí)驗(yàn)如圖4所示,包含3個(gè)部分:設(shè)計(jì)輸入、安全驗(yàn)證和驗(yàn)證輸出分析。實(shí)驗(yàn)驗(yàn)證的對(duì)象是加密算法IP核,來自Aoki Laboratory[11]。

圖4 實(shí)驗(yàn)方案

3.2 AES密碼算法核安全驗(yàn)證

1) 對(duì)下載的密碼算法核使用Yosys綜合工具進(jìn)行綜合,具體是使用綜合腳本和script命令,例如對(duì)于AES密碼算法核,對(duì)其進(jìn)行綜合,產(chǎn)生門級(jí)網(wǎng)表。

2) 對(duì)綜合后產(chǎn)生的邏輯網(wǎng)表進(jìn)行處理,對(duì)邏輯網(wǎng)表中的每一個(gè)邏輯單元進(jìn)行分析,包括端口定義、基本邏輯門、寄存器、觸發(fā)器以及賦值語句等,實(shí)例化每一個(gè)邏輯單元的信息流模型,最后生成密碼算法核的信息流模型。

3) 對(duì)密碼算法核的信息流模型進(jìn)行分析,根據(jù)密碼算法核中的信號(hào)與安全標(biāo)簽的傳播以及電路安全規(guī)范對(duì)需要驗(yàn)證的安全屬性進(jìn)行分析,對(duì)屬性相關(guān)信號(hào)進(jìn)行安全級(jí)別劃分,以及安全標(biāo)簽的設(shè)置,實(shí)現(xiàn)信息流規(guī)則描述。例如在AES-Comp IP核中對(duì)密鑰信號(hào)進(jìn)行分析,根據(jù)機(jī)密性安全屬性中禁止高安全級(jí)別的保密信號(hào)流向可公開觀測(cè)的區(qū)域,使用安全屬性描述語言進(jìn)行描述,并斷言密鑰信號(hào)不會(huì)直接流向可公開觀測(cè)的密文輸出,具體描述如下:

set key-t HIGH

set DEFAULT-LABEL LOW

assert Dout-t LOW

將安全屬性編譯為Yosys可識(shí)別的安全約束,即安全驗(yàn)證腳本。在安全驗(yàn)證中,不對(duì)明文、密文、密鑰和其他狀態(tài)信號(hào)的安全級(jí)別進(jìn)行細(xì)致的劃分,將除密文外所有信號(hào)的安全標(biāo)簽置為0,重點(diǎn)關(guān)注密鑰泄露問題。為了在輸出結(jié)果中更直觀地體現(xiàn)出密鑰的流動(dòng),得到更直觀的驗(yàn)證結(jié)果,將部分密鑰位的安全標(biāo)簽設(shè)置為1,部分位的污染標(biāo)簽設(shè)置為0。例如將密鑰污染標(biāo)簽最低位設(shè)置為1,剩余位設(shè)置為0,即Kin-t=128 ′h01。為了捕捉密鑰泄露安全漏洞,需要設(shè)置反例,向信息流模型中加入安全斷言,設(shè)置一條賦值語句,當(dāng)輸出信號(hào)安全標(biāo)簽等于密鑰安全標(biāo)簽時(shí),即輸出信號(hào)為高安全級(jí)別時(shí),將證明信號(hào)proof-f的安全標(biāo)簽賦值為1,具體如下:

assign proof-t=(Dout-t==128 ′h01)? 1∶0;

Yosys中集成了SAT求解器,在安全腳本中添加SAT形式化驗(yàn)證語句,從而形式化地驗(yàn)證證明信號(hào)的值是否始終為0,是則驗(yàn)證成功,否則驗(yàn)證失敗。可分析安全漏洞的存在,使用SAT形式化驗(yàn)證進(jìn)行安全驗(yàn)證的腳本為sat -prove proof-t 1′b0。得到的驗(yàn)證結(jié)果如圖5所示,可以看出寄存器AES-Comp-ENC.Drg-t的值等于Kin-t的值。

圖5 AES-Comp密碼算法核形式化驗(yàn)證結(jié)果

根據(jù)加密算法擴(kuò)散和混淆的特點(diǎn),密鑰的任何一位都應(yīng)該對(duì)密文的多位存在影響,盡管只有最低位密鑰安全標(biāo)簽為1,加密結(jié)果中至少有一半位的安全標(biāo)簽為1。通過Mentor Graphics ModelSim工具進(jìn)行仿真,得到加密結(jié)果中僅有最低位安全標(biāo)簽為1,功能仿真中未捕捉到密鑰和加密結(jié)果的值相等的波形。

圖6顯示了AES密碼算法核加密模塊的硬件結(jié)構(gòu),如被標(biāo)記為虛線所示,執(zhí)行第一輪密鑰加時(shí),明文與密鑰異或的結(jié)果直接被賦值給密文輸出端口。如圖7所示,將仿真testbench中明文設(shè)置為全0,則在輸出端口上可直接觀測(cè)到密鑰值。因?yàn)橹挥凶畹臀幻荑€受到污染,所以密文輸出中也只有最低位受到污染。經(jīng)過信息流安全驗(yàn)證與功能驗(yàn)證結(jié)合分析得到,在特定明文輸入條件下即明文為全0時(shí)密碼核直接泄露了全部的密鑰,此種安全漏洞屬于由中間加密結(jié)果導(dǎo)致的關(guān)鍵信息泄露。

圖6 AES-Comp密碼算法核加密模塊的硬件結(jié)構(gòu)[11]

圖7 AES密碼算法核密鑰泄露仿真波形

3.3 RSA密碼算法核安全驗(yàn)證

本實(shí)驗(yàn)采用Aoki Laboratory[11]提供的RSA密碼算法核進(jìn)行安全驗(yàn)證和漏洞檢測(cè),在安全驗(yàn)證過程中,不對(duì)明文、模數(shù)、密鑰和其他狀態(tài)信號(hào)的安全級(jí)別進(jìn)行細(xì)致的劃分,將密鑰的安全標(biāo)簽全部置為1,其他信號(hào)的標(biāo)簽置為0。按照3.2節(jié)中的方法對(duì)RSA密碼算法核進(jìn)行邏輯綜合,并產(chǎn)生信息流模型。

對(duì)生成的信息流模型進(jìn)行安全驗(yàn)證,使用Mentor Graphics ModelSim工具進(jìn)行時(shí)序仿真,通過分析仿真產(chǎn)生波形的變化來驗(yàn)證相關(guān)信號(hào)安全標(biāo)簽是否會(huì)產(chǎn)生變化,檢驗(yàn)是否存在安全漏洞。設(shè)置密鑰信號(hào)32′hFFFFFFFF,經(jīng)過一段時(shí)間的仿真后,Dout-t信號(hào)變?yōu)?2′hFFFFFFFF,BSY-t信號(hào)也變?yōu)?。Dout輸出的標(biāo)簽信號(hào)受到污染是毋庸置疑的,因?yàn)槊荑€必然會(huì)影響輸出。BSY信號(hào)是操作完成的標(biāo)志,當(dāng)IP核進(jìn)行加密、解密或者導(dǎo)入數(shù)據(jù)之后,BSY信號(hào)變?yōu)?。通過對(duì)RSA密碼算法核進(jìn)行分析,該密碼算法利用密鑰位進(jìn)行算法流程控制。密鑰位取 1 或者取 0 時(shí)會(huì)導(dǎo)致條件分支語句執(zhí)行,需要執(zhí)行不同的操作,會(huì)導(dǎo)致 RSA模冪運(yùn)算時(shí)間出現(xiàn)差異[12],操作時(shí)間上的差異導(dǎo)致RSA密碼算法核中存在時(shí)間側(cè)信道。

信息流安全仿真的結(jié)果表明:受污染的密鑰不僅導(dǎo)致密文輸出受到污染,還導(dǎo)致了操作完成信號(hào)(BSY)受到了污染,這表明了密鑰也流向了BSY信號(hào)。密鑰流向密文信號(hào)是毋容置疑的,因?yàn)槊荑€影響著加密結(jié)果。在本次實(shí)驗(yàn)中,密鑰對(duì)BSY信號(hào)是沒有直接影響的,當(dāng)加密完成后,BSY信號(hào)總會(huì)由0變?yōu)?。事實(shí)上,由BSY信號(hào)的標(biāo)簽BSY-t從0變?yōu)?可以看到密鑰確實(shí)影響了BSY信號(hào)。這是由于密鑰值的變化導(dǎo)致操作時(shí)間存在差異,從而BSY信號(hào)由0置1的時(shí)間也發(fā)生了變化,這屬于時(shí)間信息流。

通過信息流安全驗(yàn)證的方法與工具,可以捕捉到由密鑰信號(hào)到加密完成信號(hào)的時(shí)間隱通道。

圖8 RSA密碼算法核時(shí)間隱通道仿真結(jié)果

3.4 IP核安全驗(yàn)證總結(jié)

對(duì)Aoki Laboratory[11]中的6個(gè)密碼算法核進(jìn)行安全驗(yàn)證,總結(jié)如表2所示。經(jīng)過信息流安全驗(yàn)證和信息流仿真,DES、AES、Camellia、MISTY1和CAST-128密碼核經(jīng)過安全驗(yàn)證以后均發(fā)現(xiàn)有明文或者密鑰通過中間寄存器泄露至輸出的漏洞行為。這是由于上述幾種密碼算法核的設(shè)計(jì)實(shí)現(xiàn)方式導(dǎo)致的,中間寄存器的存在使得關(guān)鍵信息存在泄露風(fēng)險(xiǎn)。RSA密碼核中發(fā)現(xiàn)了由密鑰到操作完成信號(hào)的時(shí)間側(cè)信道。對(duì)密碼算法核進(jìn)行形式化安全驗(yàn)證和功能仿真,形式化驗(yàn)證在Ubuntu平臺(tái)下Yosys中完成；功能仿真在Windows系統(tǒng)下Mentor Graphics ModelSim中完成。對(duì)驗(yàn)證時(shí)間和資源消耗進(jìn)行統(tǒng)計(jì),結(jié)果列于表3?？梢钥闯觯珼ES和MISTY1密碼算法核在功能仿真中沒有捕捉到密鑰或明文泄露。

表2 密碼核安全驗(yàn)證與漏洞檢測(cè)結(jié)果

表3 密碼核驗(yàn)證性能

4 結(jié) 論

由于傳統(tǒng)功能驗(yàn)證方法已經(jīng)無法滿足密碼算法核安全驗(yàn)證的需求,本文提出了利用信息流安全驗(yàn)證的方法進(jìn)行密碼算法核驗(yàn)證。以Aoki Laboratory中的密碼算法核作為測(cè)試基準(zhǔn),信息流安全驗(yàn)證方法通過為每個(gè)信號(hào)添加安全標(biāo)簽的方式為整個(gè)密碼算法核設(shè)計(jì)產(chǎn)生安全驗(yàn)證模型,利用形式化驗(yàn)證工具Yosys進(jìn)行輸出信號(hào)安全級(jí)別的檢測(cè),從而驗(yàn)證是否存在違反信息流安全屬性的有害信息流流動(dòng)。輔助使用仿真工具M(jìn)entor Graphics ModelSim,進(jìn)行信息流仿真,對(duì)敏感信息的泄露行為有了直觀展現(xiàn),并且通過相關(guān)信號(hào)安全標(biāo)簽的變化分析出RSA密碼算法核中時(shí)間側(cè)信道的存在。無論是對(duì)中間寄存器導(dǎo)致的敏感信息泄露還是時(shí)間信息流,信息流安全驗(yàn)證方法都有較好的檢測(cè)效果。需要進(jìn)一步完善的是如何自動(dòng)化書寫高質(zhì)量安全屬性。