基于操作語義的磁臂隱通道分析

摘要：深入分析磁臂隱通道的產(chǎn)生及產(chǎn)生的原因，發(fā)現(xiàn)目前基于系統(tǒng)頂級描述和基于系統(tǒng)源代碼搜索方法難以找出這類隱通道，提出一種基于操作語義的方法來研究磁臂隱通道，將磁臂調度過程中的進程看做一個抽象機，以Plotkin的結構化操作語義給出電梯調度算法的推導規(guī)則；根據(jù)推導規(guī)則得到進程抽象機所有狀態(tài)以及進程抽象機狀態(tài)的動態(tài)變化歷史，這樣就構成完整的信息傳導操作語義模型。研究與分析兩個高低安全級進程抽象機狀態(tài)變遷及狀態(tài)變遷序列，從而找到其中存在的磁臂隱通道。

關鍵詞：隱通道； 磁臂隱通道； 信息傳導； 結構化操作語義

中圖分類號：TP309.2文獻標志碼：A

文章編號：1001-3695(2007)11-0157-04

隱通道是指系統(tǒng)的一個用戶在安全模型的監(jiān)控下，通過違反系統(tǒng)安全策略的方式傳送信息給另一用戶的機制。它一般通過系統(tǒng)原本不用于數(shù)據(jù)傳送的資源來傳送信息，并且這種通信方式往往難以被系統(tǒng)的安全機制所檢測和控制。所以隱通道能在安全系統(tǒng)中長期潛伏工作，危害巨大[1]。

自隱通道問題被提出以來，各國的信息安全專家以及計算機、數(shù)學、通信等方面的相關學者對隱通道分析進行了廣泛的研究，主要工作集中在隱通道的定義、搜索、審計和消除四個方面。其中搜索是隱通道分析中最為關鍵也是最為困難的一環(huán)[2]。已發(fā)表的隱通道搜索方法大致可以分為兩類：a)基于系統(tǒng)頂級描述的搜索方法，如隱蔽流樹法[3]、無干擾分析法[4] 和信息流分析法[5]；b)基于系統(tǒng)源代碼的搜索方法，如共享資源矩陣法[6]和源代碼分析法[7]。 與頂級描述方法相比，源代碼搜索復雜、難懂，但它卻真實地體現(xiàn)了系統(tǒng)實現(xiàn)的細節(jié)，并且精度也高于基于頂級描述的搜索方法。可是這些算法只是從某個側面反映了隱通道的特性，它們都需要輔之以手工操作。顯然對于較大規(guī)模的TCB來說，使用這類分析法不大可行，并且很容易出錯。而且這類方法屬系統(tǒng)實現(xiàn)后的分析，不便于重新設計系統(tǒng)或者修改部分設計以消除或限制隱通道。

目前，國際上對隱通道傳導信息工作機理的認識尚在探索之中，仍缺乏嚴謹?shù)碾[通道形式語義模型。從已報道的隱通道研究成果來看，進行隱通道分析的方法均是基于系統(tǒng)的程序結構描述之上，尚未發(fā)現(xiàn)有基于操作語義[8]的隱通道分析算法。

本文將磁盤讀寫過程中由于磁臂運動而產(chǎn)生的隱通道稱為磁臂隱通道。在分析磁臂隱通道時，由于磁臂優(yōu)化算法（如電梯調度算法）的應用，發(fā)現(xiàn)磁臂隱通道問題產(chǎn)生的根本原因在于，低安全級進程可通過自己的運行狀態(tài)和周圍環(huán)境來感知高安全級進程的某個信息。而這個感知過程通過分析軟件系統(tǒng)結構或源程序結構的方法是無從發(fā)現(xiàn)的。本文可證明隱通道的發(fā)生正是在不同的語境下操作語義的歧義性所導致的[9]，所以應該基于操作語義上來研究隱通道。

1磁臂調度問題

文獻[10]中提到：系統(tǒng)中假設有一個低安全級的進程L和一個高安全級的進程H。進程L發(fā)出一個讀磁盤柱面55的請

求L1′，然后立即放棄CPU，并等待請求得到服務；接著高安全級進程H占有CPU，它發(fā)出定位于柱面53的請求H1或柱面57的請求H1′，此后立即放棄CPU，并等待請求得到服務。當讀柱面55的請求L1得到服務后，低安全級進程立即同時發(fā)出兩個異步定位請求，即定位于柱面52的請求L2和柱面58的請求L2′。按照電梯算法，若高安全級進程請求的是定位于柱面53的請求H1，則請求服務的次序為圖1所示的路徑1，請求L2比請求L2′先得到服務；反之，若高安全級進程請求的是定位于柱面57的請求H1′，則請求服務的次序為路徑2，請求L2′比請求L2先得到服務。

5結束語

磁臂隱通道是一個典型的隱通道問題，用分析軟件系統(tǒng)結構或源程序結構的方法是難以發(fā)現(xiàn)的。本文可證明磁臂隱通道的發(fā)生正是在不同的語境下操作語義的歧義性所導致的。本文提出了一種基于操作語義的方法來研究磁臂隱通道并從中發(fā)現(xiàn)存在的磁臂隱通道。下一步的工作就是如何采取相應的方法來消除這類隱通道。

參考文獻：

[1]SHEN Jian－jun， QING Si－h(huán)an， SHEN Qing－ni， et al. Covert channel identification founded on information flow analysis[C]//Proc of International Conference on Computataional Inteligence and Security. 2005:381-387.

[2]OH Y H， BAE H Y. Enhancing spatial database access control by eliminating the covert topology channel[C]//Proc of IEEE Internatio￣nal Conference on Intelligence and Security Informatics. Berlin:Sprin￣ger，2005:642-643.

[3]KEMMERER R A. Covert flow trees: a visual approach to analyzing covert storage channels [J]. IEEE Transactions on Software Engineering， 1991，17(11):1166－1185.

[4]TSAI C R， GILGOR V D， CHANDERSEKARAN C S. On the identification of covert storage channels in secure systems[J]. IEEE Transactions on Software Engineering， 1990，16(6):569-580.

[5]HE Jing－sha， GLIGOR V D. Information－flow analysis for covert－channel identification in multilevel secure operating systems[C]//Proc of the 3rd IEEE Computer Security Foundations Workshop. Washington D C:IEEE Computer Society，1990:139-148.

[6]KEMMERER R A. Shared resource matrix methodology:a practical approach to indetifying covert channels [J]. ACM Transa￣ctions on Computer Systems，1983，1(3):256-277.

[7]TSAI C R， GLIGOR V D， CHANDERSEKARAN C S. A formal method for the identification of covert storage channels in source code[C]//Proc of IEEE Symposium on Security and Privacy.Oakland C A:IEEE Computer Society，1987:74-86.

[8]陸汝鈐.計算機語言的形式語義[M].北京：科學出版社，1992.

[9]WANG Chang－da， JU Shi－guang. Searching covert channels by identifying malicious subjects in the time domain[C]//Proc ofthe 5th Annual IEEE SMC Information Assurance Workshop.2004:68-73.

[10]KARGER P A， WRAY J C.Storage channels in disk arm optimization[C]//Proc of IEEE Symposium on Security and Privacy.[S.l.]:IEEE Computer Society，1991:52-61.

[11]馮玉琳，李京，黃濤.對象語義理論和行為約束推理[J].計算機學報， 1993，16(11):823-838.

[12]KHURANA H， GLIGOR V D， LINN J. Reasoning about joint admini￣stration of access policies for coalition resources[C]//Proc of the 22nd International Conference for Distributed Computer System.Washington D C:IEEE Computer Society，2002:429-452.

[13]VANGHN R B， HENNING R， FOX K. An empirical study of industrial security－engineering practices[J]. Journal of Systems and Software，2002，61(3):225-232.

[14]DENNING D. A lattice model of secure information flow[J].Communications of the ACM，1976，19(5):236-243.

[15]SABELFELD A， MYERS A C. Language－based information－flow security[J]. IEEE Journal on Selected Areas in Communications， 2003，21(1):1－15.

[16]ANDREWS G R， REITMAN R P. An axiomatic approach to information flow in programs[J]. ACM Transactions on Programming Languages and Systems， 1980，2(1): 56-76.

[17]JU Shi－guang， SONG Xiao－yu. On the formal characterization of co￣vert channe[C]//Proc of Advanced Workshop on Content Computing. Berlin:Springer， 2004:155－160.

[18]WANG Zheng－h(huán)ong， LEE R B. Capacity estimation of non－synchronous covert channels[C]//Proc of the 2nd International Workshop on Security in Distributed Computing System.Washington D C: IEEE Computer Society，2005:170-176.

[19]WANG Chang－da， JU Shi－guang. The dilemma of covert channels searching[C]//Proc of the 8th International Conference on Information Security and Cryptology.Berlin:Springer， 2006:169-174.

“本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文”