馬文輝+郭云川+張會兵

摘要：無干擾是安全信息流的一個重要需求，安全多執(zhí)行（SME）是實施無干擾的一種重要方式。本文通過實例指出了反應(yīng)系統(tǒng)中SME模型在并發(fā)調(diào)度下可能違背運行無干擾特性，分析了導(dǎo)致這種情況的原因，提出了相應(yīng)的解決方案。

關(guān)鍵詞：無干擾；安全多執(zhí)行；反應(yīng)系統(tǒng)

中圖分類號：TP311.1

文獻標(biāo)識碼：A

DOI：10.3969/jissti.1003-6970.2015.06.015

本文著錄格式：馬文輝，郭云川，張會兵，等，安全多執(zhí)行機制的無干擾性研究[J].軟件，2015，36（6）：83-87

ResearchonFacial-IightingNormalizationMethods

MAWen-hui1，GUOYun_chuan2，ZHANGHui-bing3

[Abstract]：SecureMulti-Execution（SME）isanimportantapproachforenforcingnon-interference，whichisacriticalrequirementinthefieldofsecureinformationflow.Inthispaper，RS-SMEsupportingasynchronousI/O，isanalyzed.TheresultshowsthatRS-SMEviolatesnon-interferencewhenexecutedinaconcurrentenvironment.Thereasonanditscorrespondingsolutionareproposed.

[Keywords]：Non-interference；Securemulti-execution；Reactivesystem

0引言

信息流（InformationFlow）控制通過規(guī)定系統(tǒng)中不同客體間的信息流動關(guān)系來保證信息的合法流動，同傳統(tǒng)方法相比，信息流控制不僅可以約束信息的顯式流動，而且可以控制信息的隱式流動（實際上信息流中顯式流動為隱式流動的一個實例），從而防止相互影響而帶來的非法信息流，在信息安全領(lǐng)域中信息流控制是一種較為基礎(chǔ)的方法。信息流控制的目標(biāo)為：防止攻擊者通過分析觀測某種（些）操作而導(dǎo)致的系統(tǒng)上下文環(huán)境改變來推斷信息，其核心技術(shù)手段是增加不確定性。如攻擊者Bob希望獲取Alice的信息，但受訪問策略等的約束，Bob不能直接讀取Alice的信息，在這種情況下Bob可通過觀測Alice的操作對上下文環(huán)境的改變來推斷Alice相關(guān)信息，其防護方法是增加Alice操作的不確定性。

無干擾是保障信息流安全的基本方式，目前有三種基本機制：限制計算[1]、緩解（Mitigation）[2]及安全多執(zhí)行（SecureMulti-Execution，SME）機制[3]。限制計算是通過對計算進行某種方式的約束（如約束程序語言中的條件及循環(huán)語句），從而避免泄露信息；與限制方式不同，緩解方式的基本假設(shè)是現(xiàn)實系統(tǒng)中完全避免信息泄露是不可能的，只要信息泄露量（或泄露帶寬）在容許范圍內(nèi)即可。在這兩種機制中，限制計算提供了無干擾性質(zhì)，但由于對計算進行了約束，因此其表達能力受到限制；雖然緩解方式未約束計算行為，但其允許信息泄漏，因此，不是真正意義上無干擾。針對這兩種方式的不足，2010年研究者提出了一種全新的保障無干擾機制SME[3]，其核心思想是每個安全級主體均調(diào)度執(zhí)行程序，不同安全級執(zhí)行時保證只能接收同等或低安全級的輸入，并在同等安全級輸出。該方式的主要優(yōu)點是任意程序（包括不滿足無干擾的程序）均能以無干擾方式執(zhí)行，同時不改變無干擾程序的行為。

由于SME的內(nèi)在優(yōu)點使得研究者圍繞SME在安全策略、安全語言及安全實施等方面展開了眾多研究，代表性的工作包括：在安全策略方面，針對[3]的全序執(zhí)行策略，[4]指出該策略只能保障可比較級上的弱無干擾，對于不可比較級不能保障任何無干擾，并提出了格模式執(zhí)行策略，該策略能夠保障可比較標(biāo)簽上的強無干擾及不可比較級上的弱無干擾。在安全語言方面，[5]借鑒SME在動態(tài)信息流環(huán)境中針對JavaScript引入方面值（FacetedValue），利用單進程模擬高低安全級的多執(zhí)行，該方法保證最小開銷，同時不依賴以前動態(tài)方式的阻塞執(zhí)行，以此獲得無干擾性質(zhì)。在安全實施方面，[6]首次設(shè)計了針對Haskell語言的SME庫核。[8，9]擴展了概率.時間進程代數(shù)，設(shè)計時間.概率無干擾的一致性建模方法，并以此為基礎(chǔ)給出了度量方法[10，11]給出了面向機密性和完整性的融合模型。

特別地，[7]在輕量級Firefox瀏覽器中實施了基于反應(yīng)系統(tǒng)（ReactiveSystem，RS）的SME（稱之為RS-SME），并替換和完善了SOP策略（SameOriginPolicy）。同[3，4]的I/O同步執(zhí)行不同，‘71采用異步SME執(zhí)行，由于取消了同步等待機制，因此其效率優(yōu)于[3，4]。雖然[7]證明了多執(zhí)行機制的無干擾性，但其關(guān)注的無干擾只涉及反應(yīng)系統(tǒng)本身的輸入與輸出。本文通過分析指出：RS-SME的多執(zhí)行機制在并發(fā)調(diào)度下會對運行環(huán)境（CPU及內(nèi)存占用等）帶來不可忽視的影響，從而導(dǎo)致違背運行無干擾（我們稱之為運行無干擾），分析了出現(xiàn)了這種情況的原因，給出了相應(yīng)的解決方案。

1RS-SME模型

RS-SME的總體思想如下：系統(tǒng)行為用反應(yīng)系統(tǒng)來建模，每個反應(yīng)系統(tǒng)中對每個輸入都對應(yīng)一個（系列）輸出，在運行時每個安全級主體均執(zhí)行反應(yīng)系統(tǒng)中的相關(guān)變遷，其執(zhí)行過程采用“封套（wrapper）”進行調(diào)度，以此保障只接受低于自身安全級的輸入，執(zhí)行相同安全的輸出，進而提供無干擾性質(zhì)，下面介紹與RS-SME相關(guān)的概念[7]。

定義.反應(yīng)系統(tǒng)為五元組（ConsumerState，ProducerState，Input，Output，_÷），其中，ConsumerState為所有消費狀態(tài)集合，ProducerState為所有生產(chǎn)狀態(tài)集合，Input和Output分別為輸入和輸出×字母表。令State=ConsumerStateUProducerState，Act=InputUOutput，_÷[StatexActxState為帶狀態(tài)轉(zhuǎn)移集（為了簡潔，后文用帶標(biāo)簽方式來表示），其約束為：

（1）對所有的C∈ConsumerState，若C與Q，則a∈Input，且Q∈ProducerState；

（2）對所有的P∈ProducerState，若P3Q，則a∈Output；

（3）對所有C∈ConsumerState及f∈Input，則存在P∈ProducerState使得C～P；

（4）對所有P∈ProducerState及o∈Output，則存在Q∈State使得P與Q。

約束（1）要求：對所有消費狀態(tài)，如果在該狀態(tài)接受一個動作之后轉(zhuǎn)移到下一個狀態(tài)，則該動作一定是一個輸入動作，下～個狀態(tài)一定是生產(chǎn)狀態(tài)。約束（2）要求：對所有生產(chǎn)狀態(tài)，如果在該狀態(tài)接受一個動作之后轉(zhuǎn)移到下一個狀態(tài)，則該動作一定是一個輸出動作。注意：同約束（1）相比，約束（2）中的下一個狀態(tài)不一定要求是消費狀態(tài)。約束（3）要求：對所有消費狀態(tài)和所有輸入，一定存在一個生產(chǎn)狀態(tài)使得在該消費狀態(tài)接收該輸入之后轉(zhuǎn)移到該生產(chǎn)狀態(tài)。約束（4）要求：對所有生產(chǎn)狀態(tài)和所有輸出，一定存在一個狀態(tài)（不一定要求是消費狀態(tài)）使得在該生產(chǎn)狀態(tài)輸出之后轉(zhuǎn)移到某個狀態(tài)。

給定一個反應(yīng)系統(tǒng)，其流（stream）定義為，其中，s∈Act。用I和0分別表示輸入流和輸出流，令Q（I）0表示在Q狀態(tài)輸入流I對應(yīng)的輸出流為0，其形式定義為：

為保障系統(tǒng)無干擾地執(zhí)行，RS-SME提出了使用“封套”進行調(diào)度，封套是一個二元組（R，L），其中，R：￡：Sta，te，為從安全級到反應(yīng)系統(tǒng)狀態(tài)的映射，c為安全級集合，R（，）表示在安全級，上子執(zhí)行的運行狀態(tài)；三為處于生產(chǎn)狀態(tài)所有子執(zhí)行的調(diào)度表。若三=≯，（月，三）表示封套處于消費狀態(tài)，否則處于生產(chǎn)狀態(tài)。封套的初始狀態(tài)為（月，咖，其中，對所有的l∈￡，R（，）是原反應(yīng)系統(tǒng)的初始狀態(tài)。封套的形式語義如圖1所示。

其中，fbf：，4ct_÷￡為從輸入、輸出到安全級的映射，表示對反應(yīng)系統(tǒng)的輸入或輸出的安全級，DROPc和DROPP中的‘表示不可見動作，如，內(nèi)部動作。Upper：Act_÷2c定義為Upper：Act（a）=（t|t》lbl（a））。LOAD規(guī)則通過將低安全級輸入自動傳輸?shù)礁甙踩?，從而阻對同一輸出的多次?zhí)行。

2安全分析

RS-SME模型提供無干擾的核心規(guī)則包括兩條：（1）通過LOAD規(guī)則保障僅當(dāng)子程序的運行安全級大于等于輸入安全級時，才能接收輸入進而轉(zhuǎn)移到后繼狀態(tài)，否則，子程序只能處于原狀態(tài)；（2）通過DROPc和DROPP規(guī)則保障僅當(dāng)子程序的運行安全級等于輸出安全級時才能輸出。在單核處理器中，封套只能通過分時復(fù)用CPU來執(zhí)行子執(zhí)行，在每個時間片內(nèi)只能運行單個子程序，這使得不能通過區(qū)分子程序運行的數(shù)量來違反無干擾性。然而，在多核處理器中子程序可以同時運行，這使得可通過運行不同數(shù)量的子執(zhí)行來區(qū)分信息，從而違反無干擾性，下面以實例來說明。

例.給定反應(yīng)系統(tǒng)RSo，如圖2所示，其中，ConsumerState={Co，Cl}，ProducerState={P}，Input={ai，a2，a3}，OutPut=，初始狀態(tài)為Co。令Co=令={l1，l2，l3}，，并滿足，1≤l2≤l3，lbl定義為f6，（a1）=l1bl，（a2）=f2、f6，（a3）=f3、l6l（6）=l2。

為了便于描述，將圖2所示的反應(yīng)系統(tǒng)RSo拆分為RSl-RS3，分別如圖3圖5所示，下面對封套的狀態(tài)進行分析：

（1）依據(jù)封套的定義，RSl-RS3的初始狀態(tài)均為（R，φ），其中，R（，1）=R（，2）=R（，3）=C0；

（2）初始狀態(tài)下唯一能采用的規(guī)則是LOAD規(guī)則，依據(jù)LOAD規(guī)則，不同的輸入導(dǎo)致封套的狀態(tài)（R，L）不同，如下：（2.1）對于RS1，相應(yīng)的狀態(tài)遷移為：（2.2）對于RS2，相應(yīng)的狀態(tài)遷移為：

（2.3）對于RS3，相應(yīng)的狀態(tài)遷移為：，其中，

（3）在（2）中三種封套均處于生產(chǎn)狀態(tài)，對于每種生產(chǎn)狀態(tài)，不同的調(diào)度策略有不同的調(diào)度行為，假設(shè)調(diào)度策略采用文[4]的順序策略Sequential-2，即，優(yōu)先執(zhí)行最低安全級，且在該執(zhí)行終止之前不執(zhí)行其它子執(zhí)行，下面以RSi為例進行分析：

（3.1）在/l級執(zhí)行時，由于f6，（6）≠，l，因此唯一能采用的規(guī)則為DROPc，此時，為不可見輸m，相應(yīng)的狀態(tài)遷移為：（R'，l1：：{l2，l3））_÷（R''，{l2，l3））），其中，R''（l1）=C1、R''（l2）=R''（l3）=P.

（3.2）對于（R''，{l2，l3}），由于采用低安全級優(yōu)先策略，即，l2安全級優(yōu)先執(zhí)行，同時由于，6，（6）=l2，因此，唯一能采用的規(guī)則為OUTc，輸出b，相應(yīng)的變遷為（R'l2：：{l3}）與（R'''，{l3}），其中，R'''（l1）=R'''（l2）=C1、R'''（l3）=P：

（3.3）對于（R'''，{l3}，由于lbl（b）≠l3，因此唯一能采用的規(guī)則為DROPC，此時，為不可見輸出，相應(yīng)的狀態(tài)遷移為：（R'''，l3：：{}）→（R''''，{}）），其中，R''''（l1）=R''''（l2）=R''''（l3）=C1。

在RS1中，對于輸入數(shù)據(jù)a1（安全級為，，）、輸出數(shù)據(jù)b（安全級為，l2），運行級為l1的子程序可接收al但不能輸出數(shù)據(jù)b；運行級為l2的子程序可接收a，、也能輸出數(shù)據(jù)b；運行級為，，的子程序可接收a1、但不能輸出數(shù)據(jù)b。

類似地，在RS2中，對于輸入數(shù)據(jù)a2（安全級為l2））、輸出數(shù)據(jù)6，運行級為，，的子程序不接收a2、也不能輸出數(shù)據(jù)b；運行級為，l2的子程序接收a2、同時輸出數(shù)據(jù)6；運行級為l3的子程序接收a2、但不能輸出數(shù)據(jù)b。

在RS3中，對于輸入數(shù)據(jù)a3（安全級為l3）、輸出數(shù)據(jù)6，運行級為l1和l2的子程序不接收a3、也不能輸出數(shù)據(jù)b；運行級為，l3的子程序接收a2、但不輸出數(shù)據(jù)b。

從上面的分析可以看出；對于無干擾系統(tǒng)（RSi和RS2），SME不改變執(zhí)行結(jié)果，對于違背無干擾的系統(tǒng)（RS3），在串行執(zhí)行情況下可以無干擾方式執(zhí)行。

上面的例子是串行方式中多次執(zhí)行來保障無干擾，然而，子執(zhí)行并發(fā)調(diào)度時可能導(dǎo)致違背無干擾性質(zhì)。假定在共享內(nèi)存的多核處理器中，相同處理器內(nèi)核的安全級相同，不同處理器內(nèi)核的安全級不同。在這種多執(zhí)行方式下若采用異步調(diào)度策略，由于異步策略不等待其它子程序運行終止，因此，可能導(dǎo)致多個子執(zhí)行并發(fā)運行。子執(zhí)行并發(fā)的數(shù)量不同會對程序運行環(huán)境造成影響（如耗用不同的內(nèi)存），這使得即使對于本身滿足無干擾性質(zhì)的程序也可能導(dǎo)致使得并發(fā)多執(zhí)行機制不滿足無干擾性質(zhì)，我們稱這種無干擾為運行無干擾，下面進行分析。

如圖2所示，在RSo中由于對于任意安全級的輸入（ai、a2和a3），總是輸出b，即，輸出的b不能用來確定具體輸入，因此，RSo自身滿足無干擾性質(zhì)。然而在并發(fā)執(zhí)行中對于不同輸入相應(yīng)后繼狀態(tài)可調(diào)度執(zhí)行的子程序數(shù)量不同。假設(shè)RSo在四核處理器上運行，每個內(nèi)核命名為corelcore4，其中，core1、core2和core3的安全級分別為l1，l2及l(fā)3，即，分別以l1、l2及l(fā)3的安全級來執(zhí)行子執(zhí)行，core4用作調(diào)度封套，即調(diào)度core1、core2和core3的執(zhí)行。當(dāng)輸人a1（a1的安全級為l1）后，依據(jù)多執(zhí)行中異步并發(fā)調(diào)度策略，core4將調(diào)度安全級高于l1的內(nèi)核處理器執(zhí)行RSo中P狀態(tài)下的子執(zhí)行，即core1、core2和core3將并發(fā)執(zhí)行P狀態(tài)下的子執(zhí)行；類似地，當(dāng)輸人a2（a2的安全級為l2，）后，core4調(diào)度core2和core3并發(fā)執(zhí)行P狀態(tài)下的子執(zhí)行；當(dāng)輸人a3（a3的安全級為l3）后，core4僅調(diào)度core3執(zhí)行P狀態(tài)下的子執(zhí)行。若每個子執(zhí)行占用相同的內(nèi)存，則輸入a1后內(nèi)存占有量高于輸入a2后內(nèi)存占有量，輸人a2后內(nèi)存占有量高于輸入a3后內(nèi)存占有量，由此，通過觀察內(nèi)存的使用可獲得高安全級的執(zhí)行情況，因此，并發(fā)執(zhí)行時不同輸入可能導(dǎo)致子執(zhí)行的執(zhí)行數(shù)量不同，從而違背無干擾性質(zhì)。

上述未能保障無干擾性質(zhì)的根本原因是沒有對并發(fā)子執(zhí)行的數(shù)量進行約束，這導(dǎo)致安全級輸入并發(fā)子執(zhí)行的數(shù)量不同，從而可能違背無干擾性質(zhì)。為了解決這個問題，一種方式是在任意時刻均使得并發(fā)子執(zhí)行的數(shù)量相同，并分配相同的內(nèi)存。當(dāng)沒有更多的子執(zhí)行需要執(zhí)行時，則執(zhí)行空操作使得低安全級不可區(qū)分，以此保障無干擾性質(zhì)。如，在RSo中輸入a2后，通過core4，增加一個空子執(zhí)行并分配相應(yīng)的內(nèi)存；輸人a3后，通過core4，增加兩個空子執(zhí)行并分配相應(yīng)的內(nèi)存，這樣使得低安全級不可區(qū)分高安全級的輸入。

3結(jié)論

安全信息流是保障信息不被直接或間接泄露的一項關(guān)鍵需求，無干擾是安全信息流的一個重要指標(biāo)。本文通過實例指出了RS-SME在并發(fā)調(diào)度下可能違背運行無干擾，分析了出現(xiàn)了這種情況的原因，指出了相應(yīng)的解決方案。雖然SME在保障安全執(zhí)行方面具有重大優(yōu)勢，但是這種安全多執(zhí)行是非確定的并未考慮概率因素，然而很非確定執(zhí)行下能保障無干擾，并不意味著在概率執(zhí)行情況下也能保障無干擾，這使得需要進一步研究概率執(zhí)行條下如何通過SME機制來保證無干擾。在未來我們將把安全多執(zhí)行機制應(yīng)用到復(fù)雜系統(tǒng)安全分析[12，13]中。

參考文獻

[1]BartheG，RezkT，WarmierM.PreventingTimingLeaksthroughTransactionalBranchingInstructions[C].ElectronicNotesinTheoreticalComputerScience.2006，33—55.

[2]AskarovA，MyersAC，ZhangD.PredictiveBlack-BoxMitigationofTimingChannels[C].ACMConferenceonComputerandCommunicationsSecurity.2010，297-307.

[3]DevrieseD，PiessensF.NoninterferencethroughSecureMulti-Execution[C].IEEESymposiumonSecurityandPrivacy.2010，109-124.

[4]KashyapV，WiedermannB，HardekopfB.Timing-andTermination-SensitiveSecureInformationFlow：ExploringaNewApproach[C].IEEESymposiumonSecurityandPrivacy.2011，413-428.

[5]AustinTH，F(xiàn)lanaganC.MultipleFacetsforDynamicInformationFlow[C].ProceedingsoftheACMSymposiumonPrinciplesofProgrammingLanguages.2012，165-178.

[6]JaskelioffM，RussoA[C].SecureMulti-ExecutioninHaskell.ProceedingsofAndreiErshovInternationalConferenceonPerspectivesofSystemInformatics.2011.

[7]BielovaN，DevrieseD，MassacciF，PiessensF.ReactiveNon-InterferenceforaBrowserModel[C].InternationalConferenceonNetworkandSystemSecurity.2011，97-104.

[8]郭云川，周淵，丁麗，等.基于概率干擾的概率隱蔽通道仿真研究[J].通信學(xué)報，2009，30（2）：59-64.

[9]李超，殷麗華，郭云川.基于ptSPA的概率時間信息流安全屬性分析[J].計算機研究與發(fā)展，2011，48（08）：1370-1380.

[10]SUNDonghong，GUOYunchuan，YINLihu，HUChangzhen.ComparisonofMeasuringInformationLeakageforFullyProbabilisticSystems[J].InternationalJournaloflnnovativeComputingInformationandControl.2012，8（1）：255-268.

[11]郭云川，方濱興，殷麗華，等.一種面向移動計算的機密性與完整性模型[J].計算機學(xué)報，2013，36（7）：1424-1433.

[12]韓丹，郭燕慧，楊義先.復(fù)雜信息系統(tǒng)結(jié)構(gòu)脆弱性分析方法研究[J].新型工業(yè)化，2012，2（10）：35-41.

[13]江連峰，趙佳寶.復(fù)雜事件處理技術(shù)及其應(yīng)用綜述[J].軟件，2014，35（2）：188-192.