java抽油機(jī)應(yīng)用隔離與共享機(jī)制的形式化分析

java抽油機(jī)應(yīng)用隔離與共享機(jī)制的形式化分析

0跨集合的對象訪問機(jī)制java智能機(jī)器人平臺是一個廣泛的多應(yīng)用智能機(jī)器人平臺，可以減少用戶隨身攜帶的卡數(shù)的數(shù)量，節(jié)省發(fā)送者的市場引入時間，延長卡的使用周期。Java智能卡的應(yīng)用隔離與對象共享機(jī)制,一方面保證了卡內(nèi)不同應(yīng)用提供方開發(fā)的應(yīng)用相互隔離互不干擾,另一方面也為多個合作方的應(yīng)用在卡內(nèi)進(jìn)行數(shù)據(jù)交換提供了技術(shù)支持。Java智能卡技術(shù)規(guī)范規(guī)定的應(yīng)用防火墻機(jī)制本質(zhì)上是將卡內(nèi)對象劃分為以應(yīng)用上下文(context)為標(biāo)簽的多個集合。同一集合內(nèi)的對象間訪問是合法的,而不同集合間的對象訪問是有條件的。這個跨集合的對象訪問規(guī)則就是共享接口對象訪問機(jī)制。通過對對象共享機(jī)制中所涉及的Java智能卡API進(jìn)行分析可知,獲取共享接口對象引用的安全檢查在服務(wù)器Applet中進(jìn)行,但當(dāng)客戶Applet獲得了共享對象的引用后服務(wù)器Applet無法控制該對象引用的使用,這就是Java卡規(guī)范中規(guī)定的共享接口對象訪問機(jī)制的安全漏洞。文獻(xiàn)提出了一種基于偏序網(wǎng)格的分級對象共享機(jī)制。為了控制信息流向,可以為卡內(nèi)所有應(yīng)用產(chǎn)生的對象指定一個等級,信息只可以從等級低的對象流向等級高的對象。這一方法有兩個問題:一是如何為Java智能卡中的對象指定等級,尤其是如果新下載的應(yīng)用要訪問卡內(nèi)原有應(yīng)用的共享接口時,虛擬機(jī)如何為新創(chuàng)建的共享對象指定等級;二是如果每次對象訪問都要比較訪問者與被訪問者的等級關(guān)系,那會大大降低智能卡的運(yùn)行效率。本文使用形式化分析方法對Java智能卡對象共享機(jī)制的安全性進(jìn)行分析,得出僅依靠應(yīng)用提供方的應(yīng)用級安全策略不能保證對象安全共享的結(jié)論,提出以增加卡內(nèi)全局訪問控制機(jī)制來防止未經(jīng)授權(quán)的信息流動這一安全策略設(shè)計(jì)思路,并給出一個由Java卡運(yùn)行環(huán)境和卡內(nèi)應(yīng)用共同約束對象共享的示例。1java互聯(lián)共享機(jī)制的安全策略設(shè)計(jì)1.1服務(wù)器土壤中安裝aindApplet應(yīng)用程序通過創(chuàng)建實(shí)現(xiàn)抽象接口Shareable的類的實(shí)例對象,可向其他Applet提供在該類中設(shè)計(jì)的服務(wù),流程圖如圖1所示。1)客戶Applet調(diào)用JCSystem.getsherableAppletlnterface方法,向JCRE提出共享接口服務(wù)請求,并指明服務(wù)器Applet的AID。2)JCRE收到客戶Applet的申請后,查找指定的服務(wù)器Applet,然后調(diào)用服務(wù)器Applet的getshareableAppletInterfaceobject方法將客戶Applet的請求轉(zhuǎn)發(fā)給服務(wù)器Applet,并指明客戶Applet的AID。3)服務(wù)器Applet判斷是否向客戶Applet提供共享接口中包含的服務(wù),如果可以則將共享接口對象的引用通過JCRE返回給客戶Applet。4)客戶Applet使用共享接口對象就可以調(diào)用該共享接口提供的服務(wù)。在第3)步中服務(wù)器Applet是通過檢查客戶Applet的AID是否符合自身的安全策略來決定是否提供共享接口服務(wù)的。也就是說,對象共享機(jī)制是受應(yīng)用級的安全策略保護(hù),這對兩個Applet之間的對象共享是有效的(前提是傳遞的客戶Applet的AID是真實(shí)的),但對兩個以上Applet之間的安全對象共享就存在問題。1.2質(zhì)量表sioJava智能卡內(nèi)的對象共享機(jī)制可以使用信任關(guān)系模型表示,在這個模型中主要考慮信任關(guān)系的建立以及信任關(guān)系的傳遞。類似于文獻(xiàn)的模型,本文對Java智能卡內(nèi)的信任模型進(jìn)行如下形式化分析。定義三個基本集合:1)APPLET表示Java智能卡內(nèi)已安裝的所有Applet的集合。2)SIO表示所有共享接口對象的集合。3)POLICY表示Applet的對象共享策略。共享策略定義了信任方評價受信方是否值得信任的評價標(biāo)準(zhǔn)、受信方必須具備的相關(guān)屬性,以及對信任事件所處環(huán)境的要求等。如第一部分所述,對象共享策略屬于應(yīng)用級安全策略。定義邏輯謂詞:Trust(server,client,sioS)serverclient∈APPLETsioS∈SIO表示信任關(guān)系,當(dāng)且僅當(dāng)server信任client,并向client提供sio時該謂詞為真。其中server是服務(wù)器Applet,client是客戶Applet,sioS是服務(wù)器Applet創(chuàng)建的共享接口對象。定義邏輯條件:Satisfy(policyS,client)policyS∈POLICYclient∈APPLETS表示共享策略檢查,當(dāng)且僅當(dāng)客戶Applet滿足服務(wù)器Applet的共享策略時該條件為真。信任策略可以表示為:Trust(server,client,sioS)?Satisfy(policyS,client)(1)即當(dāng)且僅當(dāng)客戶Applet滿足服務(wù)器Applet的共享策略時,服務(wù)器Applet對客戶Applet的信任關(guān)系成立。假設(shè)AppletA可向AppletB提供共享接口服務(wù),而AppletB可向AppletC提供共享接口服務(wù),即存在如下關(guān)系:Trust(AppletA,AppletB,sioA)Trust(AppletB,AppletC,sioB)如果AppletC想通過AppletB獲得AppletA的共享接口服務(wù),則可以認(rèn)為:sioA≡sioB≡sio那么,由式(1)可知,Trust(AppletA,AppletB,sio)∧Trust(AppletB,AppletC,sio)→Trust(AppletA,AppletC,sio)(2)等價于Satisfy(policyA,AppletB)∧Satisfy(policyB,AppletC)→Satisfy(policyA,AppletC)(3)根據(jù)連接符“→”的真值表,當(dāng)Satisfy(policyA,AppletB)∧Satisfy(policyB,AppletC)與Satisfy(policyA,AppletC)均為真時,式(3)為真,從而可知式(2)為真,即若AppletC想通過AppletB間接獲得AppletA的共享接口服務(wù),必須要進(jìn)行三次應(yīng)用級安全策略的驗(yàn)證:1)驗(yàn)證AppletC是否滿足AppletB的共享策略;2)驗(yàn)證AppletB是否滿足AppletA的共享策略;3)驗(yàn)證AppletC是否滿足AppletA的共享策略。這就是多應(yīng)用間對象共享的安全策略,顯然這個安全策略屬于Java智能卡的平臺級安全策略,必須由Java卡運(yùn)行環(huán)境執(zhí)行。2terface回歸對第1章描述的對象共享機(jī)制進(jìn)行調(diào)整,以三個Applet(客戶Applet、中介Applet和服務(wù)器Applet)間對象共享為例,在JCSystem.getsherableAppletlnterface方法中增加對客戶Applet是否滿足服務(wù)器Applet共享策略的驗(yàn)證,流程如圖2所示。圖2中的流程沒有包括中介Applet與服務(wù)器Applet間的交互,這是假設(shè)中介Applet已通過了服務(wù)器Applet的安全驗(yàn)證并獲得了共享接口對象的引用,該流程與圖1一致。JCRE需要在收到中介Applet的正確返回后,根據(jù)中介Applet的AID查找向其提供共享接口服務(wù)的服務(wù)器Applet,對于簡單的情況可以從中介Applet的導(dǎo)入包中找到服務(wù)器Applet。然后驗(yàn)證客戶Applet是否滿足服務(wù)器Applet的安全策略,通過后才可以返回共享對象引用給客戶Applet。3基于卡域的安全策略本文使用形式化方法對Java智能卡的對象共享機(jī)制進(jìn)行分析,通過建立信任模型來表示多應(yīng)用間的對象共享,以信任關(guān)系的建立條件分析對象共享安全策略的實(shí)質(zhì),以信任關(guān)系可傳遞性的限制分析多應(yīng)用間對象共享機(jī)制的信息流向,指出如果要阻止應(yīng)用間非授權(quán)信息傳遞,僅依靠應(yīng)用級的安全策略是不夠的,必須在卡片范圍內(nèi)制定保護(hù)策略,并在最后給出了一個簡單環(huán)境下該策略的實(shí)現(xiàn)流程。這種安全策略實(shí)現(xiàn)相對文獻(xiàn)中的方式,只需為共享對象設(shè)定相關(guān)安全屬性,并由J