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

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

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

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

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

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

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

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

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

1磁臂調度問題

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

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

5結束語

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

參考文獻：

[1]SHEN Jian－jun， QING Si－han， 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－hong， 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.

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