基于門級信息流分析的安全體系架構設計

胡 偉，慕德俊，黃興利，邰 瑜

(西北工業(yè)大學自動化學院 西安 710072)

基于門級信息流分析的安全體系架構設計

胡 偉，慕德俊，黃興利，邰 瑜

(西北工業(yè)大學自動化學院 西安 710072)

現代處理器架構中的緩存器、分支預測器等部件通常都包含難以檢測的隱通道，成為攻擊者入侵系統(tǒng)的切入點?，F有方法難以有效地檢測硬件相關的隱通道，從而使得這些安全漏洞往往在攻擊造成嚴重損失后才暴露出來。該文構建了一種基于執(zhí)行租賃機制的安全體系架構，以嚴格控制不可信執(zhí)行環(huán)境的影響邊界，保證不同執(zhí)行環(huán)境之間的嚴格隔離，并采用門級抽象層次上的信息流分析方法，建立硬件架構的信息流模型，實現對硬件中全部邏輯信息流的精確度量，通過捕捉有害信息流動來檢測硬件架構中潛在的安全漏洞，進而通過指令集架構的信息流模型向上層提供信息流度量能力，以實現軟硬件聯合安全驗證。

隱通道; 門級信息流分析; 信息流控制; 安全體系架構; 安全漏洞

為提高處理速度，現代計算機普遍采用多核結構，并引入緩存器、分支預測器等高性能部件。這些結構和部件在顯著提高運算效率的同時也往往會引發(fā)一些不確定性的系統(tǒng)行為和不期望干擾，造成難以檢測的隱通道，并成為系統(tǒng)的安全脆弱點。例如，文獻[1]構建了一種多核處理器下共享緩存隱通道的預測模型，并準確估測了AES和Blowfish算法實現潛在的隱通道；文獻[2]給出了一種通過緩存器時序攻擊破解AES密碼算法密鑰的方法；文獻[3]則提出了一種通過觀測分支預測器狀態(tài)來分析得到密碼算法密鑰的方法。大量安全事件表明：以安全脆弱點、隱通道、內嵌惡意代碼等安全漏洞為切入點對系統(tǒng)發(fā)起攻擊通常比直接破解密碼算法或突破訪問控制機制更為有效，并且這些安全漏洞難以檢測，往往在攻擊造成嚴重損失之后才暴露出來。

傳統(tǒng)計算架構在設計階段并未充分考慮安全性問題，因此現有計算系統(tǒng)大多采用被動防御機制來保障系統(tǒng)安全，如密碼算法、訪問控制、虛擬化和隔離技術等。然而，密碼算法無法防止敏感數據在運算過程中發(fā)生泄露以及算法執(zhí)行硬件平臺中安全漏洞所導致的密鑰泄露；訪問控制可有效管理數據的分發(fā)，但無法進一步監(jiān)控數據的傳播，也無法防止旁路效應所引發(fā)的信息泄露；虛擬化和隔離技術能夠防止不同執(zhí)行環(huán)境之間的相互干擾，但無法消除由共享部件(如緩存器)所引發(fā)的不期望交互。并且，上述機制大多位于軟件層面，無法捕捉到底層硬件中的隱通道，如硬件相關的時間隱通道(timing channel)和存儲器隱通道(storage channel)。

由于信息流分析方法在漏洞檢測方面具有特有的優(yōu)勢，本文擬構建基于門級信息流分析的安全體系架構設計與驗證方法，在設計階段即檢測和消除硬件架構中潛在的安全漏洞，特別是硬件相關的隱通道，自硬件底層為系統(tǒng)構建一個可靠的安全基礎，為解決上層軟件的安全問題提供一種安全屬性的度量與驗證能力，進而實現軟硬件聯合安全驗證。

1 門級信息流分析方法

文獻[4]首先提出了信息流的概念，以及一種通過靜態(tài)驗證來強化信息流安全策略的方法。信息流分析方法通常采用格模型(lattice model)來描述信息流的信道與策略。任何一個信息流策略都可采用一個形如L=(SC,)的安全格(security lattice)來描述。其中，SC是客體安全類的集合；是定義在該安全類集上的偏序關系，規(guī)定了不同安全類之間許可的數據流向，即只允許信息在同一安全類之內或者向更高級別的安全類流動。定義函數L:O→SC返回對象O的安全類。給定任意對象a和b，若L(a)L(b)，則信息從a流向b是安全的。

信息流分析方法能夠監(jiān)控信息的傳播，防止敏感信息泄露，并能有效檢測以安全漏洞為切入點的攻擊。然而，現有的信息流分析方法大多采用粗粒度(字或字節(jié)粒度)的標簽和保守的標簽傳播策略，簡單地以所有源操作數安全類的最小上界作為輸出的安全類，未考慮輸入對輸出的實際影響，因此無法對系統(tǒng)中實際存在的信息流進行準確地度量。此外，現有信息流分析方法大多針對程序語言/編譯器[5]、操作系統(tǒng)[6]和指令集架構等抽象層次[7-8]。在上述抽象層次上，硬件的實現細節(jié)和一些特性(如寄存器間時序)是完全透明的，因此上述方法無法檢測到硬件相關的隱通道。

為有效捕捉硬件相關的時間隱通道，文獻[9]提出了門級信息流跟蹤(gate level information flow tracking, GLIFT)方法，從邏輯門級抽象層次準確地度量每個二進制位信息的流動，能夠有效捕捉硬件電路中全部的邏輯信息流，包括顯式流、隱式流以及硬件相關時間隱通道和存儲器隱通道所引發(fā)的有害信息流動。該方法針對二級線性安全格LOWHIGH。完整性分析中，可信非可信；機密性分析中，非保密保密。以二輸入與門(AND-2)為例，表1定義了門級信息流跟蹤方法下AND-2的安全標簽傳播規(guī)則。由表格的第二行和第二列，若AND-2的任一輸入為(LOW,0)，則其輸出固定為(LOW,0)，與另一個輸入無關，而非簡單地以全部輸入安全類的最小上界作為輸出的安全類。可見，門級信息流分析方法以信息流的定義為基礎，考慮了輸入對輸出的實際影響，因而能夠更準確地對系統(tǒng)中實際存在的信息流進行度量。

以A，B和O來表示與門的輸入和輸出，以at，bt和ot來分別表示它們的安全標簽，并假定當at=0時，L(a)=LOW，當at=1時，L(a)=HIGH 。則由表1可推導出AND-2的門級信息流分析邏輯如式(1)?？梢姡T級信息流分析方法在計算輸出的安全標簽時不僅考慮輸入的安全標簽at和bt，還考慮了輸入的值A和B對輸出O的實際影響，因此比傳統(tǒng)保守的信息流分析方法更為準確。

類似地，可進一步推導或門、非門、異或門等基本邏輯單元的信息流分析邏輯，從而構建一個基本邏輯單元信息流分析邏輯庫。基于該信息流分析邏輯庫，即可離散式地為復雜硬件電路中的每一個邏輯單元實例化信息流分析邏輯，從而產生復雜硬件電路的門級信息流分析邏輯，實現對硬件電路中全部邏輯信息流的精確度量。

在門級抽象層次上，所有的邏輯信息流，如顯式流、隱式流以及時間隱通道所引發(fā)的信息流都具有統(tǒng)一的數學描述，并均以二進制位為單位顯式地流動。因此，門級信息流分析方法能夠通過捕捉有害信息流動來檢測硬件中潛在的安全漏洞?，F有工作中，文獻[10-11]對門級信息流分析方法的基本理論進行了深入研究，主要包括信息流分析邏輯的性質定理、形式化描述、生成算法及復雜度理論等。文獻[12-13]給出了利用門級信息流分析檢測共享總線(I2C、USB和Wishbone)架構中時間隱通道的方法，并構建了一種采用門級信息流分析方法檢測和消除SoC系統(tǒng)中不同信任級別IP核之間有害信息流的測試框架[14]。本文研究了基于門級信息流分析的安全體系架構設計與驗證方法，并提出一種基于門級信息流分析的軟硬件安全聯合驗證方法。

2 安全體系架構設計與驗證

2.1 安全體系架構設計

為防止由不同執(zhí)行環(huán)境之間相互干擾所引發(fā)的有害信息流動，需嚴格限制不同執(zhí)行環(huán)境的時間和空間邊界。如圖1所示，本文向現有硬件體系架構中引入執(zhí)行租賃單元。該租賃架構下，每個進程都有特定的安全級別(HIGH/LOW)、執(zhí)行時間定時器值(timer)和存儲器邊界(memory)。進程啟動時，租賃單元設置PC，加載定時器和存儲器邊界值。進程執(zhí)行時，租賃單元負責存儲器訪問中的安全屬性和邊界檢查。當定時器溢出后，當前進程被掛起，直至再次調度并加載定時器時重新啟動；執(zhí)行租賃單元重置PC，并實施環(huán)境切換和清理，以防止執(zhí)行環(huán)境的相互干擾和敏感信息泄露。

在上述租賃架構下，當定時器溢出時，執(zhí)行租賃單元將取得控制權，從而限定了進程執(zhí)行的時間邊界，防止惡意進程長時間占用處理器資源。若進程每次啟動時采用隨機或固定長度的定時器值，則可消除程序執(zhí)行狀態(tài)所引發(fā)的有害時間信息流(timing flow)，如不同條件分支執(zhí)行時間差異所導致的信息泄露。進程在訪問存儲器時將受到嚴格的安全類型和邊界檢查，保證其只能訪問同一或更低安全級別的數據，并禁止其越界訪問共享資源。因此，不可信進程的影響邊界將被嚴格限制在該進程的時間片和存儲器資源范圍之內，從而可防止由緩存等共享部件引發(fā)的信息泄露。

2.2 安全體系架構的測試與驗證方法

本文采用門級信息流分析方法對執(zhí)行租賃架構的安全性進行測試與驗證。圖2給出了安全體系架構測試與驗證方法的基本原理。

如圖2所示，給定采用硬件設計語言(VHDL或Verilog)描述的租賃架構，首先需采用邏輯綜合工具(如Synopsys Design Compiler)將設計轉化為門級網表，然后，可采用文獻[10-11]中所提出的算法為設計生成相應的門級信息流分析邏輯。門級信息流分析邏輯具有良好的數學形式，可在其基礎上對設計中的全部邏輯信息流進行準確地度量，從而檢測信息流安全策略是否被違反。若信息流安全策略被違反，則門級信息流分析邏輯將捕捉到相應的有害信息流動，通過分析有害信息流的傳播路徑，即可檢測到設計中的安全漏洞，從而為設計修改提供指導。門級信息流分析方法能夠充分利用底層硬件實現的細節(jié)信息，捕捉包括硬件相關時間隱通道在內的全部邏輯信息流，因此，上述設計與驗證方法能夠有效檢測和消除硬件架構中潛在的安全漏洞。

此外，還可采用布爾邏輯對租賃架構的門級信息流分析邏輯進行描述，從而使得體系架構的信息流分析邏輯可隨原始設計后端物理實現，在系統(tǒng)運行中實時地捕捉系統(tǒng)中的有害信息流動。當檢測到有害信息流時，即可觸發(fā)中斷和異常處理，從而防止敏感信息泄露或關鍵數據被非法篡改。

3 軟硬件聯合安全驗證方法

在上述安全架構的基礎上，可進一步構建基于門級信息流分析的軟硬件聯合安全驗證方法。如圖3所示，該方法從邏輯門級抽象層次開始構建硬件的信息流模型，進而構造功能單元、控制邏輯、存儲器的信息流模型，并進一步建立指令集架構的信息流模型。指令集架構的信息流模型可對軟件中每條指令所包含的信息流進行準確描述，從而可為上層軟件提供一種信息流度量能力。在上述驗證方法中，信息流度量能力從邏輯門級抽象層次向上傳遞至上層軟件，而系統(tǒng)的安全屬性(如保密性和完整性)則向下傳遞至硬件層面得到驗證。

4 實驗結果

4.1 仿真實驗

本文以Trsut-Hub測試基準AES為例來驗證門級信息流分析方法在檢測硬件安全漏洞方面的有效性。如圖4所示，當木馬激活信號Tj_Trig觸發(fā)后，木馬程序會通過Antenna信號泄露密鑰。此時，僅通過觀測Antenna信號的值無法發(fā)現其隱含了密鑰信息，但門級信息流分析邏輯信號Antenna_t置位(Antenna_t=1)區(qū)域則顯示密鑰流向了Antenna，即準確捕捉到了密鑰泄露。

本文進一步以OpenCores測試基準RSA為例來驗證所提出的安全架構在消除硬件相關隱通道方面的有效性。RSA密碼算法的流程受密鑰控制。密鑰當前位分別為邏輯‘1’和邏輯‘0’時，算法所需執(zhí)行的操作不同，完成操作所需的時間也相應存在差異，這將導致一個硬件相關的時間隱通道，并可引發(fā)密鑰泄露[15]。本文通過狀態(tài)機控制RSA密碼算法核的執(zhí)行，并引入計時器timer1和timer2分別對引入安全架構前后的算法執(zhí)行時間進行測量，以模擬時序分析攻擊，同時為RSA密碼算法核產生門級信息流分析邏輯，通過仿真實驗分析密鑰泄露情況。仿真實驗結果如圖5所示。

由圖5可知，密鑰key的信息流分析邏輯key_t = FFFFFFFF，表征密鑰屬于敏感信息。未引入租賃架構時，timer1測量到的算法執(zhí)行時間依賴于密鑰，因此，仿真結果中timer1的信息流分析邏輯timer1_t = FFFFFFFF。在本文所提出的租賃架構下，算法分多個時間片執(zhí)行，每個時間片的長度是隨機的，與密鑰無關，因此，仿真結果中timer2的信息流分析邏輯timer2_t = 00000000。仿真實驗表明：未引入租賃架構時，算法執(zhí)行上的延遲差異會造成時間隱通道，導致密鑰泄露，而本文所提出的安全架構可消除該時間隱通道。

4.2 設計復雜度分析

為對門級信息流分析方法用于動態(tài)信息流跟蹤時的設計復雜度進行評估，本文選用IWLS測試基準alu2，alu4和DES以及Trust-Hub測試基準PIC16F84，MC8051和AES對信息流分析邏輯的面積和延遲進行了分析。由歸一化平均值可見，信息流分析邏輯(不包含原始設計)平均會引入2.69倍的額外面積開銷和0.93倍的額外延遲開銷。上述結果反映了將體系架構的門級信息流分析邏輯用于動態(tài)信息流安全監(jiān)控時的面積和性能開銷。

由表2可知，門級信息流分析邏輯用于動態(tài)信息流安全監(jiān)控時將帶來較高的面積和性能開銷。在實際應用中，可對設計進行安全劃分，且僅需為安全關鍵模塊附加門級信息流分析邏輯。此外，門級信息流分析方法還可用于靜態(tài)信息流安全驗證，當驗證完成后，即可將額外的信息流分析邏輯移除，從而避免額外的設計開銷。

5 結 束 語

門級信息流分析方法能夠從硬件電路層面上捕捉系統(tǒng)中全部的邏輯信息流，特別是硬件相關時間隱通道所導致的敏感信息泄露。本文構建了一種基于執(zhí)行租賃機制的安全體系架構，并給出了一種基于門級信息流分析的安全體系架構驗證方法。該方法能夠自硬件底層為系統(tǒng)搭建一個可靠的安全基礎，并可向上層軟件提供一種信息流度量與驗證能力，從而實現軟硬件聯合安全驗證。

[1] DOMNITSER L, ABU-GHAZALEH N, PONOMAREV D. A predictive model for cache-based side channels in multicore and multithreaded microprocessors[C]//The 5th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security (MMMACNS'10). Berlin, Heidelberg: Springer-Verlag, 2010: 70-85.

[2] BERNSTEIN D J. Cache-timing attacks on aes[R]. Chicago, USA: University of Illinois at Chicago, 2005.

[3] JEAN-PIERRE O A, SEIFERT J P, KOC C K. Predicting secret keys via branch prediction[C]//The Cryptographers Track at the RSA Conference. Berlin, Heidelberg: Springer-Verlag, 2007: 225-242.

[4] DENNING D E. Cryptography and data security[M]. Boston, MA, USA: Addison-Wesley Longman Publishing Co Inc, 1982.

[5] SABELFELD A, MYERS A. Language-based informationflow security[J]. IEEE Journal on Selected Areas in Communications, 2003, 21(1): 5-19.

[6] KROHN M, YIP A, BRODSKY M, et al. Information flow control for standard os abstractions[C]//The 21st ACM SIGOPS Symposium on Operating Systems Principles (SOSP’07). New York, USA: ACM, 2007: 321-334.

[7] SUH G E, LEE J W, ZHANG D, et al. Secure program execution via dynamic information flow tracking[C]//The 11th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XI). New York, USA: ACM, 2004: 85-96.

[8] NEWSOME J, SONG D. Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software[C]//The 12th Annual Network and Distributed System Security Symposium (NDSS’05). San Diego, CA, USA: [s.n.], 2005.

[9] TIWARI M, WASSEL H W, MAZLOOM B, et al. Complete information flow tracking from the gates up[C]//The 14th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’09). New York, USA: ACM, 2009: 109-120.

[10] HU W, OBERG J, IRTURK A, et al. Theoretical fundamentals of gate level information flow tracking[J]. IEEE Trans on CAD, 2011, 30(8): 1128-1140.

[11] HU W, OBERG J, IRTURK A, et al. On the complexity of generating gate level information flow tracking logic[J]. IEEE Trans on IFS, 2012, 7(3): 1067-1080.

[12] OBERG J, HU W, IRTURK A, et al. Information flow isolation in i2c and usb[C]//The 48th ACM/EDAC/IEEE Design Automation Conference (DAC). San Diego, CA, USA: IEEE, 2011: 254-259.

[13] OBERG J, MEIKLEJOHN S, SHERWOOD T, et al. A practical testing framework for isolating hardware timing channels[C]//Design Automation and Test in Europe (DATE). San Jose, CA, USA: ACM, 2013: 1281-1284.

[14] OBERG J, SHERWOOD T, KASTNER R. Eliminating timing information flows in a mix-trusted system-onchip[J]. IEEE Design and Test of Computers, 2013, 30(2): 55-62.

[15] KOCHER P C. Timing attacks on implementations of Diffie-Hellman, RSSA, DSS, and other systems[C]// Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO’96). Santa Barbara, CA, USA: Springer-Verlag, 1996: 104-113.

編 輯 蔣 曉

Crafting Verifiably Secure Architecture Through Gate Level Information Flow Analysis

HU Wei, MU De-jun, HUANG Xing-li, and TAI Yu
(School of Automation, Northwestern Polytechnical University Xi’an 710072)

Components such as caches and branch predictors in modern processor architectures tend to include hard-to-detect covert channels, which provide a foot-holder for attackers to perform malicious activities. However, existing methods are inefficient in detecting hardware-specific covert channels. As a consequence, these security holes expose only after significant damages are inflicted. In this paper, a secure architecture based on the execution lease mechanism is built in order to tightly bound the effects of untrusted execution contexts and enforce the strict isolation of execution contexts. Further, the information flow model of the hardware architecture is constructed by using the gate level information flow analysis method, which allows the precise measurement of all digital flows in the underlying hardware and the detection of security vulnerabilities by capturing harmful flows of information. In addition, hardware/software security co-verification can be achieved with the aid of information flow measurement capability provided by the information flow model of the instruction set architecture.

covert channel; gate level information flow analysis; information flow control; secure architecture; security vulnerability

TP309

A

10.3969/j.issn.1001-0548.2015.03.019

2013 ? 09 ? 17；

2014 ? 03 ? 20

國家自然科學基金(61303224)；教育部博士點基金(20126102110036)；中國博士后科學基金面上項目(2013M532081)

胡偉(1982 ? )，男，博士，主要從事硬件安全、可重構計算以及嵌入式系統(tǒng)等方面的研究.