移動(dòng)灰箱演算中強(qiáng)干擾問(wèn)題的進(jìn)一步控制

移動(dòng)灰箱演算中強(qiáng)干擾問(wèn)題的進(jìn)一步控制管旭東楊怡玲尤晉元上海交通大學(xué)計(jì)算機(jī)科學(xué)與工程系(200030){guan-xd,yang-yl,you-jy}@摘要：為了消除灰箱演算(MA)中的強(qiáng)干擾問(wèn)題，Levi等人在灰箱演算的基礎(chǔ)上引入了反動(dòng)作的概念，并提出了一套安全灰箱演算系統(tǒng)(SA)。然而，SA所引入的反動(dòng)作卻帶來(lái)了安全上的隱患。本文提出的魯棒灰箱演算系統(tǒng)(ROAM)在依靠反動(dòng)作解決強(qiáng)干擾問(wèn)題的同時(shí)，根據(jù)反動(dòng)作的參數(shù)明確了該反動(dòng)作的使用對(duì)象，以消除SA中引入的不安全因素。通過(guò)對(duì)防火墻跨越和多元異步-演算的描述顯示ROAM依然保留了MA和SA較強(qiáng)的表達(dá)能力。同時(shí)本文就ROAM的類(lèi)型問(wèn)題作了初步的探討，給出并證明了一套R(shí)OAM演算的類(lèi)型系統(tǒng)。該類(lèi)型系統(tǒng)可以表達(dá)進(jìn)程和能力的移動(dòng)性和線(xiàn)程數(shù)兩個(gè)屬性。關(guān)鍵詞:進(jìn)程代數(shù)，移動(dòng)灰箱演算，安全移動(dòng)灰箱演算，魯棒灰箱演算，類(lèi)型FurtherControlontheGraveInterferenceinMobileAmbientsXudongGuan,YilingYang,YinyuanYouDept.ofCompuerSci.&Eng.,ShanghaiJiaotongUniv.,China,200030{guan-xd,yang-yl,you-jy}@Abstract.MobileSafeAmbients(SA)wasproposedinordertoremovethegraveinterferenceintheMobileAmbientcalculus.ButthecoactionsintroducedinSAalsobringsomesecuritybreaches.Inthispaper,asimilarcalculuscalledRobustAmbients(ROAM)wasproposedasamorerationalsubstituteforSA.Throughsepcifiyingtheparametersofthecoactions,theambientsinROAMaremorerobustagainstmalicioustampering.Theencodingofpolyadicasynchronous-calculusinROAMshowsthatROAMdoesnotlossthestrongexpressivenessofitsancestors.AfundamentaltypesystemforROAMwithboththreadcountandmobilityattributeswasalsoproposedandprovedinthepaper.Keywords.processalgebra,MobileAmbient,MobileSafeAmbient,RobustAmbient,typeCardelli和Gordon在文獻(xiàn)[1]中首先提出了可以統(tǒng)一描述移動(dòng)計(jì)算中的計(jì)算平臺(tái)移動(dòng)性和計(jì)算代碼移動(dòng)性的移動(dòng)灰箱（MobileAmbient-MA）演算（箱字取自其整體移動(dòng)性，灰字取自其內(nèi)部結(jié)構(gòu)部分可見(jiàn)、部分不可見(jiàn)之意——發(fā)生歸約的部分可見(jiàn)，其余不可見(jiàn)）?；蚁洌╝mbient）是一個(gè)可以整體移動(dòng)的計(jì)算場(chǎng)所?；蚁渲g表現(xiàn)為樹(shù)狀嵌套關(guān)系，可以直觀地描述互聯(lián)網(wǎng)上的自治域及防火墻、自治域中的子域及計(jì)算設(shè)備、移動(dòng)代理運(yùn)行環(huán)境及其內(nèi)部的移動(dòng)代理程序等。無(wú)論是一個(gè)企業(yè)Intranet網(wǎng)絡(luò)、一臺(tái)便攜式計(jì)算機(jī)，還是一個(gè)移動(dòng)代理，在MA中都統(tǒng)一地被形式化為一個(gè)灰箱。同時(shí)，灰箱的邊界具有保護(hù)作用，只有穿越邊界進(jìn)入某灰箱的內(nèi)部，才能與之發(fā)生信息交換。MA對(duì)移動(dòng)計(jì)算中的計(jì)算性和移動(dòng)性描述有很好的形式化支持。隨著研究的不斷深入[2,3,4,5]，MA也暴露出一些設(shè)計(jì)上的不足。文獻(xiàn)[2,3,4]試圖從類(lèi)型的角度進(jìn)行彌補(bǔ)，但是引入了太多的條件限制，且效果不理想。Levi等人在文獻(xiàn)[6]中首次指出MA在語(yǔ)法上存在強(qiáng)干擾（graveinterference）問(wèn)題——由于灰箱移動(dòng)的單方參與性，歸約順序的不同將會(huì)導(dǎo)致完全不同的結(jié)果。例如以下的MA表達(dá)式：h[]|n[inh|m[outn.P]] (1)可歸約為（首先灰箱n經(jīng)inn動(dòng)作進(jìn)入h，之后灰箱m經(jīng)outn動(dòng)作移出n，即：先in后out）h[n[m[outn.P]]]h[n[]|m[P]] (2)也可歸約為（先out后in）h[]|n[inh]|m[P]h[n[]]|m[P] (3)由于存在(2)(3)兩種不同歸約結(jié)果，P無(wú)法判斷m的具體位置，從而影響后續(xù)的歸約。文獻(xiàn)[6]在指出強(qiáng)干擾問(wèn)題的同時(shí)，也提出了一種解決方法，通過(guò)引入移動(dòng)的雙方參與性來(lái)約束歸約的順序，即為每個(gè)動(dòng)作（action）配置相應(yīng)的反動(dòng)作（coaction），這種改進(jìn)的演算被稱(chēng)為安全灰箱（safeambient-SA）演算。然而，SA演算雖然解決了MA中的強(qiáng)干擾問(wèn)題，但同時(shí)卻引入了不安全的因素。其反動(dòng)作很容易被第三方挪用，從而使雙方的移動(dòng)協(xié)議失效。例如以下的兩個(gè)SA表達(dá)式：n[inm.n.P]|m[m.openn.Q]|h[inm] (4)m[m.inn.P|n[outm.n.Q]|h[outm]] (5)在表達(dá)式(4)中，n希望進(jìn)入m后被打開(kāi)，同樣m等待n的進(jìn)入并對(duì)其執(zhí)行打開(kāi)操作。但是，這個(gè)協(xié)議很容易被與n同層的灰箱h所破壞：只要h也發(fā)出一個(gè)進(jìn)入m的請(qǐng)求，m中的m動(dòng)作就有可能先同h中的inm動(dòng)作發(fā)生歸約并讓h進(jìn)入，從而無(wú)法正常完成打開(kāi)n的協(xié)議。表達(dá)式(5)中也存在類(lèi)似的問(wèn)題。針對(duì)以上問(wèn)題，本文提出了一種可以限定反動(dòng)作對(duì)象的抗干擾魯棒灰箱(RObustAMbient-ROAM)演算，在克服MA中強(qiáng)干擾問(wèn)題的同時(shí)，也不存在SA中的安全漏洞。并在此基礎(chǔ)上，給出了一套基本的ROAM演算類(lèi)型規(guī)則。在表達(dá)能力上，ROAM與MA、SA同樣可以達(dá)到描述多元異步-演算[7]的能力，文章結(jié)尾給出了一種編碼方案。ROAM語(yǔ)法的取舍分析SA帶來(lái)的反動(dòng)作挪用問(wèn)題的根源在于SA中沒(méi)有限制反動(dòng)作的歸約對(duì)象。為了達(dá)到與MA相同的表達(dá)能力，SA將反動(dòng)作的參數(shù)統(tǒng)一設(shè)置為包含該反動(dòng)作的灰箱的名字。這樣，對(duì)任何MA表達(dá)式，只要在所有的灰箱x中增加進(jìn)程!x|!x|!x，就可轉(zhuǎn)化成等價(jià)的SA表達(dá)式。但是這種表達(dá)能力上的簡(jiǎn)單性卻帶來(lái)了上述的反動(dòng)作被挪用的問(wèn)題。為了在控制強(qiáng)干擾的同時(shí)，避免引入負(fù)面效應(yīng)，應(yīng)該謹(jǐn)慎選擇動(dòng)作和反動(dòng)作的歸約對(duì)象。在SA中，反動(dòng)作的參數(shù)就是其所在灰箱的名字，在歸約中并沒(méi)有起到任何實(shí)質(zhì)的作用。本文嘗試在利用反動(dòng)作控制強(qiáng)干擾問(wèn)題的同時(shí)，進(jìn)一步利用反動(dòng)作的參數(shù)限制其歸約對(duì)象，以預(yù)防反動(dòng)作被挪用。以下簡(jiǎn)單討論各反動(dòng)作參數(shù)的取舍。在隨后的章節(jié)中，我們將對(duì)新演算系統(tǒng)進(jìn)行形式化引入。i).:假設(shè)灰箱外部有多個(gè)灰箱等待進(jìn)入，這些灰箱進(jìn)入的先后次序必須有一定的手段來(lái)控制。顯然，一個(gè)直觀的方法是：用所帶的參數(shù)來(lái)指定允許使用該反動(dòng)作的灰箱。如：h[n]|n[inh]就可歸約為h[n[]]，而h[n]|m[inh]就不能。ii).:同樣，在多個(gè)灰箱等待跳出同一灰箱時(shí)，的參數(shù)可用來(lái)指定哪個(gè)灰箱有權(quán)使用它。如：h[n|n[outh]]n[]|h[]。iii).:與上述和相反，只有父灰箱會(huì)使用open來(lái)試圖打開(kāi)某一個(gè)子灰箱（同該子灰箱的進(jìn)行歸約），這里不存在多個(gè)open競(jìng)爭(zhēng)同一個(gè)的問(wèn)題，因此，后沒(méi)有必要再增加一個(gè)多余的參數(shù)。另外，對(duì)于三個(gè)傳統(tǒng)的動(dòng)作（in、out、open）中的out來(lái)說(shuō)，它所在的灰箱唯一所要跳出的灰箱就是其父灰箱。故此，在引入反動(dòng)作后，out后所帶的參數(shù)也是沒(méi)有實(shí)際作用的。采用以上描述方法，表達(dá)式(4)、(5)分別可表示為：n[inm..P]|m[n.openn.Q]|h[inm] (6)m[n.inn.P|n[out.m.Q]|h[out]] (7)經(jīng)過(guò)上述修改，反動(dòng)作n和n被指定只能由灰箱n使用，灰箱h無(wú)法挪用。ROAM演算基于以上取舍分析，下面給出這種新演算——ROAM的形式化描述及操作語(yǔ)義。語(yǔ)法(syntax)設(shè)N為名字集，元素用n表示，定義ROAM演算中的進(jìn)程集Proc和能力集Cap如下（其元素分別用P和M表示）：P::=0┃(vn:W)P┃P|Q┃!P┃M[P]┃M.P┃(n1:W1,…,nk:Wk).P┃M1,…,MkM::=┃n┃inM┃M┃out┃M┃openM┃┃M.M’這里的“v”、“|”、“!”、“.”分別為進(jìn)程代數(shù)中通常使用的名字創(chuàng)建、并置、重復(fù)和動(dòng)作記號(hào)；M[P]為灰箱記號(hào)，代表一個(gè)名字為M、內(nèi)部活動(dòng)進(jìn)程為P的灰箱；“()”和“”分別表示消息的輸入和輸出記號(hào)，同時(shí)本文使用了多元輸入輸出操作，即以元組作為輸入輸出的基本單位；三種基本操作進(jìn)入、移出、打開(kāi)分別由in、out和open表示。這些基本結(jié)構(gòu)的具體含義可參見(jiàn)[1]中的詳細(xì)介紹。ROAM中最大的不同是引入了類(lèi)似SA中的反動(dòng)作：、和，同時(shí)進(jìn)一步規(guī)定了反動(dòng)作的歸約對(duì)象，只有特定的灰箱才能參與。動(dòng)作和反動(dòng)作的具體歸約規(guī)則將在2.4節(jié)中給出。為減少括號(hào)的使用，這里規(guī)定“|”的優(yōu)先級(jí)最低。自由變量和約束變量采用習(xí)慣的定義方式：在(vn:W)P和(n1:W,…,nk:W).Q中，n和n1,…,nk分別為約束變量，其它情況下出現(xiàn)的變量稱(chēng)為自由變量。函數(shù)fn(P)表示進(jìn)程P中的所有自由變量的集合。同時(shí)，為避免名字捕獲，我們對(duì)約束變量可以使用-換名規(guī)則。替換操作(substitution)為描述歸約規(guī)則中的消息傳遞機(jī)制，首先引入替換的概念。設(shè)M’為能力、n為名字，定義對(duì)進(jìn)程P和能力M的替換(substitution)操作P{M’/n},M{M’/n}如下：(Sub-Eps) {M’/n}=(Sub-n) n’{M’/n}=n’, n’n n’{M’/n}=M’,n’=n(Sub-in) (inM){M’/n}=in(M{M’/n})(Sub-) (M){M’/n}=(M{M’/n})(Sub-out) out{M’/n}=out(Sub-) (M){M’/n}=(M{M’/n})(Sub-open) (openM){M’/n}=open(M{M’/n})(Sub-) {M’/n}=(Sub-Path) (M1.M2){M’/n}=(M1{M’/n}).(M2{M’/n})(Sub-Inact) 0{M’/n}=0(Sub-Res) ((vn’:W)P){M’/n}=(vn’:W)(P{M’/n}),n’n且n’fn(M’) ((vn’:W)P){M’/n}=(vn’:W)P ,n’=n(Sub-Par) (P|Q){M’/n}=(P{M’/n})|(Q{M’/n})(Sub-Rep) (!P){M’/n}=!(P{M’/n})(Sub-Amb) (M[P]){M’/n}=(M{M’/n})[P{M’/n}](Sub-Act) (M.P){M’/n}=(M{M’/n}).(P{M’/n})(Sub-Abs) ((n1:W1,…,nk:Wk).P){M’/n}=(n1:W1,…,nk:Wk)(P{M’/n}),n’{n1,…,nk}且n’fn(M’) ((n1:W1,…,nk:Wk).P){M’/n}=(n1:W1,…,nk:Wk).P ,n’{n1,…,nk}(Sub-Msg) (M1,…,Mk){M’/n}=M1{M’/n},…,Mk{M’/n}為書(shū)寫(xiě)簡(jiǎn)單起見(jiàn)，下文使用P{M1/n1,…,Mk/nk}來(lái)表示(…(P{M1/n1})…){Mk/nk}；M{M1/n1,…,Mk/nk}表示(…(M{M1/n1})…){Mk/nk}。同構(gòu)關(guān)系(structuralcongruence)在引入ROAM演算的歸約規(guī)則之前，再引入Proc集上的同構(gòu)關(guān)系“”，定義如下：(StructRef) PP(StructSymm) PQQP(StructTrans) PQ,QRPR(StructRes) PQ(vn:W)P(vn:W)Q(StructPar) PQP|RQ|R(StructRep) PQ!P!Q(StructAmb) PQM[P]M[Q](StructAct) PQM.PM.Q(StructAbs) PQ (n1:W1,…,nk:Wk).P(n1:W1,…,nk:Wk).Q(StructParComm) P|QQ|P(StructParAssoc) (P|Q)|RP|(Q|R)(StructRep) !PP|!P(StructResRes) (vn:W)(vm:V)P(vm:V)(vn:W)P ,如果nm(StructResPar) (vn:W)(P|Q)P|(vn:W)Q ,如果nfn(P)(StructResAmb) (vn:W)m[P]m[(vn:W)P] ,如果nm(StructZeroPar) P|0P(StructZeroRes) (vn:W)00(StructZeroRep) !00(StructEps) .PP(StructPath) (M.M’).PM.M’.P歸約規(guī)則(reductionrules)ROAM演算有以下8條歸約規(guī)則：(R-in) n[m.P1|P2]|m[inn.Q1|Q2]n[P1|P2|m[Q1|Q2]](R-out) n[m.P1|P2|m[out.Q1|Q2]] n[P1|P2]|m[Q1|Q2](R-open) openn.P|n[.Q1|Q2]P|Q1|Q2(R-Msg) M1,…,Mk|(n1:W1,…,nk:Wk).PP{M1/n1,…,Mk/nk}(R-Res) (R-Par) (R-Amb) (R-) ROAM較之MA和SA，最明顯的不同在于歸約雙方的參與性和相互控制——?jiǎng)幼鞯膱?zhí)行者和動(dòng)作的授權(quán)者必須同時(shí)參與歸約動(dòng)作，并且動(dòng)作的授權(quán)者必須明確指定動(dòng)作執(zhí)行者的身份。ROAM演算的類(lèi)型系統(tǒng)本文的ROAM演算類(lèi)型系統(tǒng)結(jié)合了文獻(xiàn)[6]中的線(xiàn)程數(shù)概念和文獻(xiàn)[3]中的移動(dòng)性特點(diǎn)，并在此基礎(chǔ)上提出了一套基本的類(lèi)型系統(tǒng)。在ROAM中，進(jìn)程和能力包含兩個(gè)的屬性：移動(dòng)性和線(xiàn)程數(shù)。進(jìn)程的消息交換類(lèi)型概念和能力的Amb和Cap兩種類(lèi)型源自MA的類(lèi)型系統(tǒng)[2]，基本保留了原有概念的涵義。類(lèi)型語(yǔ)法設(shè)移動(dòng)性標(biāo)志集合Alpha為{,}，其元素用表示；線(xiàn)程數(shù)標(biāo)志集Beta為{0,1,1+,n}，其元素用表示。定義ROAM演算的類(lèi)型語(yǔ)法如下：W ::V ，能力的類(lèi)型表達(dá)式V :: 有以下兩種： Amb[S] ，1.灰箱能力，如：n[P]中的n Cap[S] ，2.動(dòng)作能力，如：openn，inn，等。T ::S ，進(jìn)程的類(lèi)型表達(dá)式S :: 消息交換有以下兩種：: W1…Wk ，1.交換類(lèi)型為(W1,…,Wk)的元組 Shh ，2.不進(jìn)行消息交換(上式中k=0) :: 兩類(lèi)移動(dòng)性標(biāo)志： ，1.移動(dòng)(包含in或out動(dòng)作) ，2.固定(否則) :: 四類(lèi)線(xiàn)程數(shù)標(biāo)志： n ，1.多線(xiàn)程 1+ ，2.單線(xiàn)程，但以openn結(jié)束 1 ，3.單線(xiàn)程，不以openn結(jié)束 0 ，4.沒(méi)有活動(dòng)線(xiàn)程此外，Alpha和Beta集上的四種運(yùn)算定義如下：i).二元運(yùn)算ii).二元運(yùn)算12:212:2n1+1011nnnnn1+nnn1+1n1+110n1+10iii).二元運(yùn)算iv).一元運(yùn)算12:2n1+101nnnNnNn1+nnN1+1+1+1nnN111+0n1+1001同時(shí)，為描述集合元素間的關(guān)系，分別引入Alpha和Beta集上的全序關(guān)系“”。i).Alpha上的關(guān)系“<”為{(，)}，“”為“<”的自反、傳遞閉包。容易得到以下關(guān)于“”及運(yùn)算“”的一些性質(zhì)：性質(zhì)3-1(對(duì)稱(chēng)):12=21性質(zhì)3-2(結(jié)合):(12)3=1(23)性質(zhì)3-3:11=1性質(zhì)3-4:12=31323性質(zhì)3-5:121323ii).Beta上的關(guān)系“<”為{(0,1),(1,1+),(1+,n)}，“”為“<”的自反、傳遞閉包。容易得到以下關(guān)于“”及運(yùn)算“”、“”、“”的一些性質(zhì)：性質(zhì)3-6(結(jié)合):(12)3=1(23)性質(zhì)3-7:12=31323性質(zhì)3-8:121323性質(zhì)3-9(對(duì)稱(chēng)):12=21性質(zhì)3-10(結(jié)合):(12)3=1(23)性質(zhì)3-11:11=1(11)性質(zhì)3-12:12=31323性質(zhì)3-13:121323性質(zhì)3-14:1212類(lèi)型規(guī)則ROAM的類(lèi)型推導(dǎo)規(guī)則采用與文獻(xiàn)[2,3]中相同的判定形式。令表示一個(gè)類(lèi)型環(huán)境；├表示為一個(gè)合法的類(lèi)型環(huán)境；├M:W表示能力M在環(huán)境下是一個(gè)合法的能力表達(dá)式，其類(lèi)型為W；├P:T表示進(jìn)程P在環(huán)境下是一個(gè)合法的進(jìn)程表達(dá)式，其類(lèi)型為T(mén)。ROAM演算的類(lèi)型演算規(guī)則如下：(Sany表示任意某個(gè)消息傳遞類(lèi)型)(EnvEmpty) (Envn) (Capn) (CapEps) (Capin) (Cap) (Capout) (Cap) (Capopen) (Cap) (CapPath) (ProcInact) (ProcRes) (ProcPar) (ProcRep) (ProcAmb) (ProcAct) (ProcAbs) (ProcMsg) 上述類(lèi)型系統(tǒng)的正確性由下面的命題3-15所保證：命題3-15:如果├P:S111,PQ,那么├Q:S122并且2121。該命題的完整證明由附錄一給出。結(jié)果“2121”表明對(duì)一個(gè)進(jìn)程表達(dá)式的歸約絕對(duì)不會(huì)增加其移動(dòng)性和線(xiàn)程數(shù)目。一個(gè)非移動(dòng)的進(jìn)程將永遠(yuǎn)是不可移動(dòng)的，一個(gè)單線(xiàn)程的進(jìn)程也絕對(duì)不會(huì)隨著歸約進(jìn)程而變成一個(gè)多線(xiàn)程的進(jìn)程。在該類(lèi)型系統(tǒng)的基礎(chǔ)上可以進(jìn)一步引入子類(lèi)型（subtype）的概念，這樣一個(gè)類(lèi)型約束性高的表達(dá)式（如：不可移動(dòng)、單線(xiàn)程）同時(shí)也可以具有約束性比該類(lèi)型低的類(lèi)型，這種更加完整的子類(lèi)型系統(tǒng)將是我們下一步的主要工作之一。舉例在增強(qiáng)了反動(dòng)作參數(shù)限制以后，ROAM演算仍然具有類(lèi)似MA和SA的很強(qiáng)的表達(dá)能力。我們以灰箱演算中經(jīng)典的防火墻跨越（firewall-crossing）例子以及對(duì)多元異步-演算的描述來(lái)說(shuō)明以上事實(shí)。防火墻跨越在文獻(xiàn)[1]和[5]中多次使用防火墻跨越的例子，來(lái)說(shuō)明灰箱演算在安全性上的描述能力。一個(gè)授權(quán)的代理（agent）可以正確地穿越一個(gè)防火墻（firewall）到達(dá)其內(nèi)部。該防火墻（一個(gè)灰箱）的名字對(duì)外部完全保密，為了讓授權(quán)的代理正確進(jìn)入防火墻，防火墻首先送出一個(gè)向?qū)Щ蚁?，由于授?quán)代理?yè)碛蓄A(yù)先約定好的密鑰k，k’和k’’，因此可以由向?qū)Щ蚁鋷ьI(lǐng)進(jìn)入防火墻內(nèi)部。在ROAM中，防火墻跨越的例子表示為：Agent::=k’[k.openk.(x:W).inx.|k”[|Q]] (8)Firewall::=(vw)w[k[out.ink’..w]|k.k’.openk’.openk”.P] (9)在表達(dá)式(8)、(9)中，進(jìn)程P和Q的可以是任意的。假設(shè)其類(lèi)型分別為：├P:Sppp、├Q:Sqqq，則灰箱w,k,k’,k”可賦予以下類(lèi)型：├w:Amb[Sp]n├k:Amb[(w)]1├k’:Amb[(w)]n├k”:Amb[Sq]qq只要保證密鑰k,k’,k”的保密性，授權(quán)代理利用密鑰可順利進(jìn)入防火墻內(nèi)部，并讓其內(nèi)部的進(jìn)程Q在防火墻內(nèi)部運(yùn)行，我們可以得到以下結(jié)論：(vkk’k”)(Agent|Firewall)((vw)w[P|Q])這里的關(guān)系“”是一種全等關(guān)系（congruence），由于篇幅關(guān)系，在文中并未引入。它可以被看作是一種上下文全等關(guān)系（contextualcongruence）。即，無(wú)論將兩個(gè)全等的進(jìn)程放入什么上下文中，所得到的結(jié)果都表現(xiàn)出完全相同的外部特性。在SA中，防火墻跨越前后的全等性必須通過(guò)禁止上下文中存在某類(lèi)動(dòng)作來(lái)達(dá)到[6]。ROAM的魯棒性表現(xiàn)在對(duì)任何存在惡意干擾的上下文，該全等性都成立。描述多元異步-演算對(duì)多元異步-演算（polyadicasynchronous-calculus）的描述通?？梢泽w現(xiàn)一套演算系統(tǒng)的描述能力。在多元異步-演算中，通道（channel）n的類(lèi)型為Ch[W1,…,Wk]，表示該通道傳遞的元組中第i個(gè)元素的類(lèi)型為Wi。類(lèi)型判定使用├P的形式，其中為類(lèi)型環(huán)境，P為符合正確類(lèi)型規(guī)則的-進(jìn)程。ROAM演算對(duì)多元異步-演算的一種編碼方案如下：[├P]::=[]├[P]:Shhn[,n1:W1…,nk:Wk]::=,n1:[W1]…,nk:[Wk][Ch[W1,…,Wk]]::=Amb[[W1]…[Wk]]n[(vn:Ch[W1,…,Wk])P]::=(vn:[Ch[W1,…,Wk]])

(n[!(n.openn)]|[P])[n(n1:W1,…,nk:Wk).P]::=(vp:Amb[Shh]n)(openp|n[inn..(n1:[W1],…,nk:[Wk])(p[out..[P]]

|p)])[nn1,…,nk]::=n[inn..n1,…,nk][P|Q]::=[P]|[Q][!P]::=![P][0]::=0在這里，一個(gè)-通道n表示為一個(gè)灰箱n。該灰箱中的進(jìn)程!(n.openn)不斷地讓試圖在該通道上進(jìn)行通信的灰箱進(jìn)入，并將它們打開(kāi)。在-通道n上進(jìn)行輸入和輸出操作被描述為若干進(jìn)入灰箱n并被打開(kāi)的灰箱。輸入和輸出灰箱被相繼打開(kāi)以后，消息傳遞便在灰箱n中進(jìn)行。在消息傳遞發(fā)生后，得到輸入的進(jìn)程跳出灰箱n并繼續(xù)執(zhí)行。這樣，在-通道n上進(jìn)行元組通訊被轉(zhuǎn)化為在灰箱n中進(jìn)行多元消息傳遞。以上編碼方案對(duì)于一個(gè)-通道名只使用了一個(gè)灰箱名，該名字既作為表示一個(gè)-通道的灰箱的名字，也用來(lái)表示進(jìn)入該通道進(jìn)行消息交換的輸入輸出灰箱。當(dāng)然，可以分別再使用兩個(gè)不同的灰箱名分別表示輸入和輸出灰箱，這樣，每個(gè)灰箱的類(lèi)型還可以定義得更加具體，如表示通道的灰箱就可規(guī)定為非移動(dòng)灰箱。但是，以上這種方案簡(jiǎn)單明了，同名的灰箱并不會(huì)引起混淆，足以說(shuō)明問(wèn)題。結(jié)論和進(jìn)一步的工作本文基于MA和SA的工作，提出了魯棒灰箱演算系統(tǒng)——ROAM，進(jìn)一步改進(jìn)了SA中對(duì)MA強(qiáng)干擾的控制，克服了SA中存在的安全隱患。通過(guò)對(duì)防火墻跨越和多元異步-演算的描述，表明ROAM同MA和SA類(lèi)似，具有很強(qiáng)的描述能力。同時(shí)，本文提出了一套具有線(xiàn)程數(shù)和移動(dòng)性屬性的類(lèi)型系統(tǒng)，并證明了該類(lèi)型系統(tǒng)對(duì)歸約操作的一致性。本文對(duì)ROAM的研究尚處于起步階段，其中的類(lèi)型規(guī)則，各種全等關(guān)系等還有待進(jìn)一步的研究和探索。對(duì)ROAM演算的進(jìn)一步工作主要有：子類(lèi)型系統(tǒng)的建立和證明、單線(xiàn)程進(jìn)程的性質(zhì)研究等。參考文獻(xiàn)L.Cardelli,A.D.Gordon.MobileAmbients.FoundationsofSoftwareScienceandComputationalStructures,LectureNotesinComputerScience,No.1378,Springer,pp.140-155,1998.L.Cardelli,A.D.Gordon.TypesforMobileAmbients.Proc.26thPOPL,pages79-92.ACMPress.1999.L.Cardelli,G.Ghelli,A.D.Gordon.MobilityTypesforMobileAmbients.InProc.ICALP’99,LectureNotesinComputerScience,No.1644,Springer,pp.230-239,1999.L.Cardelli,G.Ghelli,A.D.Gordon.AmbientGroupsandMobilityTypes,toappear.A.D.Gordon,L.Cardelli.EquationalPropertiesofMobileAmbients.ProceedingsofFOSSACS'99,W.Thomas,Ed.,LectureNotesinComputerScience,No.1578.Springer,pp.212-226,1999.F.Levi,D.Sangiorgi.ControllingInterferenceinAmbients.ToappearinProc.27thAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,Boston,Massachusetts,Jan.19-21,2000.Alsoavailableat:ftp://zenon.inria.fr/meije/theorie-par/davides/SafeAmbients.psR.Milner.Thepolyadic-calculus:atutorial.InLogicandAlgebraofSpecification.SpringerVerlag,1993.附錄一命題3-15的證明引理A-1:如果├M.P:S111,那么├P:S1222121.直接由(Proc-Cap)和“”關(guān)系的定義可得。引理A-2:如果├P1:S111,├P2:S222,├P1|Q:S133,并且├P2|Q:S244,2121,那么43并且43.直接由(Proc-Par),性質(zhì)3-5,3-13可得.推論A-3:如果├M.P|Q:S111,那么├P|Q:S1222121.直接應(yīng)用引理A-1和引理A-2的結(jié)果可得.引理A-4:如果’,n:W,’’├J那么ndom(’,’’).證：將變量引入環(huán)境的唯一方法是通過(guò)規(guī)則(ProcRes)和(ProcInput)。由于可以使用約束變量換名，可以認(rèn)為這些引入的變量都不相同。這樣，在任何環(huán)境中，任意變量n只可能出現(xiàn)一次。引理A-5:如果├n:W并且├n:W’,那么W=W’.證：得到├n:W的唯一辦法是通過(guò)(Capn)，由于相同的變量n在同一個(gè)環(huán)境中只可能出現(xiàn)一次，因此，如果還有├n:W’，則W=W’。引理A-6(ImpliedJudgement):如果’,’’├J那么’├.證：對(duì)’的構(gòu)造過(guò)程進(jìn)行歸納。i).如果’=，那么由(EnvEmpty)知’├。ii).如果’=”’,n:W，那么有”’,n:W,”├J。由歸納假設(shè)知”’├。由引理A-4知ndom(”’)，所以通過(guò)(Envn)可得”’,n:W├，即：’├。引理A-7(Exchange):如果’,n:W’,m:W’’,’’├J那么’,m:W’’,n:W’,’’├J.證：從環(huán)境中獲取變量類(lèi)型的唯一途徑是(Capn)。由(Capn)知，引入變量的類(lèi)型與該變量在環(huán)境中的位置無(wú)關(guān)，即’,n:W’,m:W’’,’’和’,m:W’’,n:W’,’’從外部觀察是等價(jià)的。（即：對(duì)同樣的變量名，返回的類(lèi)型是完全一樣的)。因此，通過(guò)對(duì)’,n:W’,m:W’’,’’├J的推導(dǎo)過(guò)程進(jìn)行歸納，很容易可以同樣得到’,m:W’’,n:W’,’’├J。引理A-8(Weakening):如果’,’’├J并且ndom(’,’’)那么’,n:W,’’├J.證明過(guò)程類(lèi)似引理A-7。引理A-9(Strengthening):如果’,n:W,’’├J并且nfn(J)那么’,’’├J.證：通過(guò)將J中的所有約束變量n換名，使得J中的變量名不包括n。這樣，在’,n:W,’’├J的推導(dǎo)過(guò)程中，條件n:W不會(huì)被使用，因此’,’’├J可通過(guò)同樣的步驟推導(dǎo)得到。引理A-10(Substituition):如果’├M’:W并且’,n:W,’’├J,那么’,’’├J{M’/n}.通過(guò)對(duì)’,n:W,’’├J的推導(dǎo)過(guò)程歸約可以證明（此處略）。引理A-11(SubjectCongruence):(1)P:S111并且PQ,那么├Q:S111。(2)如果├P:S111并且QP,那么├Q:S111。證：對(duì)PQ和QP的推導(dǎo)進(jìn)行雙向歸納。(1)如果├P:S111并且PQ,那么├Q:S111。(StructRef)易知。(StructSymm)那么QP,由歸納假設(shè)知(2)，可知：├Q:S111。(StructTrans)那么由某個(gè)R使得：PR，RQ。由歸納假設(shè)(1)，├R:S111。再由歸納假設(shè)(1)，├Q:S111。(StructRes)那么P=(vn:W)P’，Q=(vn:W)Q’，且P’Q’。設(shè)├(vn:W)P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRes)得到，且有,n:W├P’:S111。由歸納假設(shè)(1)知，,n:W├Q’:S111。再由(ProcRes)知：├(vn:W)Q’:S111。(StructPar)那么P=P’|R，Q=Q’|R且P’Q’。設(shè)├P’|R:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcPar)得到，且有├P’:S122,，├R:S133且1=231=23。由歸納假設(shè)(1)知，├Q’:S122。再由(ProcPar)知：├Q’|R:S111。(StructRep)那么P=!P’，Q=!Q’且P’Q’。設(shè)├!P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRep)得到，且├P’:S112并且1=22。由歸納假設(shè)(1)知：├Q’:S112.By(ProcRep),├!Q’:S111.(StructAmb)那么P=M[P’]并且Q=M[Q’],withP’Q’，設(shè)├M[P’]:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcAmb)得到，且├M:Amb[S2]22，├P’:S233，3232且1=1=0。由歸納假設(shè)(1)知，├Q’:S233.By(ProcAmb),├M[Q’]:S111.(StructAct)那么P=M.P’并且Q=M.Q’,withP’Q’，設(shè)├M.P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcAct)得到，且├M:Cap[S1]22,├P’:S133并且1=231=23。由歸納假設(shè)(1)知：├Q’:S133。再由(ProcAct)可的：├M.Q’:S111。(StructAbs)那么P=(n1:W1,…,nk:Wk).P’，Q=(n1:W1,…,nk:Wk).Q’且P’Q’，設(shè)├(n1:W1,…,nk:Wk).P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcAbs)得到，且,n1:W1,…,nk:Wk├P’:W1…Wk11并且S1=W1…Wk。由歸納假設(shè)(1)知：,n1:W1,…,nk:Wk├Q’:W1…Wk11.By(ProcAbs),├(n1:W1,…,nk:Wk).Q’:S111.(StructParComm)那么P=P’|P’’并且Q=P’’|P’，設(shè)├P’|P’’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcPar)得到，且├P’:S122，├P’’:S133且1=231=23。由和的對(duì)稱(chēng)性可知：1=321=32。再由(ProcPar)可得：├P’’|P’:S111。(StructParAssoc)那么P=(P’|P’’)|P’”并且Q=P’|(P’’|P’”)，設(shè)├(P’|P’’)|P’”:S111，這只能通過(guò)使用兩次類(lèi)型規(guī)則(ProcPar)得到，且有├P’:S122，├P’’:S133，├P’”:S144且1=(23)41=(23)4。由和的結(jié)合性可知，1=2(34)1=2(34)，再由兩次(ProcPar)可得├P’|(P’’|P’”):S111。(StructRepPar)那么P=!P’并且Q=P’|!P’，設(shè)├!P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRep)得到，且├P’:S112并且1=22。由性質(zhì)3-11知，1=2(22)=21。再由(ProcPar)可得：├P’|!P’:S111。(StructResRes)那么P=(vn:W1)(vm:W2)P’并且Q=(vm:W2)(vn:W1)P’，設(shè)├(vn:W1)(vm:W2)P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRes)兩次得到，且,n:W1,m:W2├P’:S111。由引理A-7可得，,m:W2,n:W1├P’:S111。再由(ProcRes)兩次可得：├(vm:W2)(vn:W1)P’:S111。(StructResPar)那么P=(vn:W)(P’|P’’)，Q=P’|(vn:W)P’’且nfn(P’)。設(shè)├(vn:W)(P’|P’’):S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRes)得到，且,n:W├P’|P’’:S111，再由(ProcPar)得到，且,n:W├P’:S122，,n:W├P’’:S133且1=231=23。由nfn(P’)利用引理A-8可知：,n:W├P’:S122，再由(ProcPar)可知,n:W├P’|P’’:S111，最后由(ProcRes)可得：├(vn:W)(P’|P’’):S111。(StructResAmb)那么P=(vn:W)m[P’]，Q=m[(vn:W)P’]且nm，設(shè)├(vn:W)m[P’]:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRes)得到，且,n:W├m(xù)[P’]:S111，以及(ProcAmb)且,n:W├m(xù):Amb[S2]22，,n:W├P’:S233，3232且1=1=0。由nm利用引理A-9可得：├m(xù):Amb[S2]22，再由(ProcRes)可得├(vn:W)P’:S233。最后由(ProcAmb)可知：├m(xù)[(vn:W)P’]:S111。(StructZeroPar)那么P=P’|0并且Q=P’，設(shè)├P’|0:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcPar)得到，且├P’:S122，├0:S10且1=21=20.。由和的定義可知1=21=2，即：├P’:S111。(StructZeroRes)那么P=(vn:W)0并且Q=0，設(shè)├(vn:W)0:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRes)得到，且,n:W├0:S111。由引理A-9可得：├0:S111。(StructZeroRep)那么P=!0并且Q=0，由于├0:Sany0，設(shè)├!0:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcRep)得到，且├0:S112，1=22。再由(ProcInact)且1=2=0。因此1=00=0=2。(StructEps)那么P=.P’并且Q=P’，設(shè)├.P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcAct)得到，且├:Cap[S1]22，├P’:S133并且1=231=23。前者只能由(CapEps)得到，且2=2=0。由和的定義可知：1=31=3，即：├P’:S111。(StructPath)那么P=(M.M’).P’并且Q=M.(M’.P’)，設(shè)├(M.M’).P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcAct)得到，且├M.M’:Cap[S1]22，├P’:S133且1=231=23。前者只能由(CapPath)得到，且├M:Cap[S1]44，├M’:Cap[S1]55且2=452=45。由性質(zhì)3-2及3-6，可知：1=(45)3=4(53)1=(45)3=4(53)。再由兩次(ProcAct)可得：├M.(M’.P’):S111。(2)如果├P:S111并且QP，那么├Q:S111。(StructRef)易證。(StructSymm)那么PQ，由歸納假設(shè)(1)知：├Q:S111。(StructTrans)那么存在某個(gè)R使得：QR，RP。由歸納假設(shè)(1)知：├R:S111，再由歸納假設(shè)(1)知：├Q:S111。(StructRes)(StructPar)(StructRep)(StructAmb)(StructAct)(StructAbs)同(1)中的證明完全對(duì)稱(chēng)，略。(StructParComm)那么Q=P’|P’’并且P=P’’|P’，設(shè)├P’’|P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcPar)得到，且├P’’:S122，├P’:S133且1=231=23。由和的對(duì)稱(chēng)性可得：1=321=32，再由(ProcPar)可知：├P’|P’’:S111。(StructParAssoc)那么Q=(P’|P’’)|P’”并且P=P’|(P’’|P’”)，設(shè)├P’|(P’’|P’”):S111，這只能通過(guò)使用兩次類(lèi)型規(guī)則(ProcPar)得到，且有├P’:S122，├P’’:S133，├P’”:S144且1=2(34)1=2(34)。由和的結(jié)合性質(zhì)可知：1=(23)41=(23)4，再應(yīng)用兩次(ProcPar)可得：├(P’|P’’)|P’”:S111。(StructRepPar)那么Q=!P’并且P=P’|!P’，設(shè)├P’|!P’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcPar)得到，且├P’:S122，├!P’:S133且1=231=23。后者只能通過(guò)使用(ProcRep)得到，且2=33=22。由性質(zhì)3-3可知：1=33=3。再由性質(zhì)3-11可得1=2(22)=22=3，即：├!P’:S111。(StructResRes)同(1)中的證明完全對(duì)稱(chēng)，略。(StructResPar)那么Q=(vn:W)(P’|P’’)，P=P’|(vn:W)P’’且nfn(P’)，設(shè)├P’|(vn:W)P’’:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcPar)得到，且├P’:S122，├(vn:W)P’’:S133并且1=231=23.。后者只能通過(guò)使用(ProcRes)得到，且,n:W├P’’:S133。由nfn(P’)根據(jù)引理A-9可得：├P’:S122，再由(ProcRes)知：├(vn:W)P’’:S133，最后由(ProcPar)，可得：├P’|(vn:W)P’’:S111。(StructResAmb)那么Q=(vn:W)m[P’]，P=m[(vn:W)P’]且nm，設(shè)├m(xù)[(vn:W)P’]:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcAmb)得到，且├m(xù):Amb[S2]22，├(vn:W)P’:S233，3232且1=1=0。后者只能通過(guò)使用(ProcRes)得到，且,n:W├P’:S233。由nm利用引理A-8可知：,n:W├m(xù):Amb[S2]22，再由(ProcAmb)可得：,n:W├m(xù)[P’]:S111，最后由(ProcRes)可得：├(vn:W)m[P’]:S111。(StructZeroPar)那么Q=P’|0并且P=P’，設(shè)├P’:S111。由引理A-6可知├，再由(ProcInact)知：├0:S10。由(ProcPar)得：├P’|0:S1(1)(10)，再由和的定義可知：├P’|0:S111。(StructZeroRes)那么Q=(vn:W)0并且P=0，設(shè)├0:S111，由引理A-8知：,n:W├0:S111，再由(ProcRes)可得：├(vn:W)0:S111。(StructZeroRep)那么Q=!0并且P=0，設(shè)├0:S111，這只能通過(guò)使用類(lèi)型規(guī)則(ProcInact)得到，且1=1=0，由(ProcRep)可知：├!0:S112且2=11=00=0=1，即：├!0:S111。(StructEps)那么Q=.P’并且P=P’，設(shè)├P’:S111，由引理A-6知├，再由(ProcEps)知：├:Cap[S1]0，再利用(ProcAct)可得：├.P’:S1(1)(10)。由得定義可得：├.P’:S111。(StructPath)那么Q=(M.M’).P’并且P=M.(M’.P’)，設(shè)├M.(M’.P’):S111，這只能通過(guò)使用兩次類(lèi)型規(guī)則(ProcAct)得到，且├M:Cap[S1]22，├M’:Cap[S1]33，├P’:S144且1=2(34)1=2(34)，由性質(zhì)3-2和3-6可知1=(23)41=(23)4。再由(ProcAct)及(ProcPath)可得：├(M.M’).P’:S111。命題3-15:如果├P:S111,PQ,那么├Q:S122并且2121.證：對(duì)PQ的推導(dǎo)過(guò)程進(jìn)行歸納。(R-in):(1)├n[m.P1|P2]|m[inn.Q1|Q2]:S111 已知條件(2)├n[m.P1|P2]:S122 (1)，僅能使用(ProcPar)(3)├m(xù)[inn.Q1|Q2]:S133 同(2)(4)1=23,1=23 同(2)(5)2=2=0 (2)，僅能使用(ProcAmb)(6)├n:Amb[Sn]nn 同(5)(7)├m(xù).P1|P2:Sn44 同(5)(8)4n4n 同(5)(9)3=3=0 (3)，僅能使用(ProcAmb)(10)├m(xù):Amb[Sm]mm 同(9)(11)├inn.Q1|Q2:Sm55 同(9)(12)5m5m 同(9)(13)├P1|P2:Sn66 (7)+推論A-3(14)6464 同(13)(15)├Q1|Q2:Sm77 (11)+推論A-3(16)7575 同(15)(17)6n6n (8)(14)+的傳遞性(18)7m7m (12)(16)+的傳遞性(19)├m(xù)[Q1|Q2]:S0 (10)(15)(18)+(ProcAmb)(20)├P1|P2|m[Q1|Q2]:Sn66 (13)(19)+(ProcPar)(21)├n[P1|P2|m[Q1|Q2]]:S10 (6)(17)(20)+(ProcAmb)(22)1=1=0 (4)(5)(9)+,的定義由(21),(22)知，命題在(R-in)情況下成立。(R-out):(1)├n[m.P1|P2|m[out.Q1|Q2]]:S111 已知條件(2)├n:Amb[Sn]nn (1)，僅能使用(ProcAmb)(3)├m(xù).P1|P2|m[out.Q1|Q2]:Sn22 同(2)(4)1=，1=0 同(2)(5)2n2n 同(2)(6)├m(xù).P1|P2:Sn33 (3)，僅能使用(ProcPar)(7)3232 同(6)+性質(zhì)3-4,3-12(8)├m(xù)[out.Q1|Q2]:Sn44 同(6)(9)4242 同(6)+性質(zhì)3-4,3-12(10)├P1|P2:Sn55 (6)+推論A-3(11)5353 同(10)(12)5n5n (5)(7)(11)+的傳遞性(13)├n[P1|P2]:Sany0 (2)(10)(12)+(ProcAmb)(14)├m(xù):Amb[Sm]mm (8)，僅能使用(ProcAmb)(15)├out.Q1|Q2:Sm66 同(14)(16)6m6m 同(14)(17)4=，4=0 同(14)(18)├Q1|Q2:Sm77 (15)+推論A-3(19)7676 同(18)(20)7m7m (16)(19)+的傳遞性(21)├m(xù)[Q1|Q2]:Sany0 (14)(18)(20)+(ProcAmb)(22)├n[P1|P2]|m[Q1|Q2]:Sany0 (13)(21)+(ProcPar)由(4),(22)知，命題在(R-out)情況下成立。(R-open):(1)├openn.P|n[.Q1|Q2]:S111 已知條件(2)├openn.P:S122 (1)+(ProcPar)僅能使用(3)2121 同(2)+性質(zhì)3-4,3-12(4)├n[.Q1|Q2]:S133 同(2)(5)3131 同(2)+性質(zhì)3-4,3-12(6)├n:Amb[Sn]nn (4)+(ProcAmb)僅能使用(7)├.Q1|Q2:Sn44 同(6)(8)4n4n 同(6)(9)├Q1|Q2:Sn55 (7)+推論A-3(10)5454 同(9)(11)├openn:Cap[Sn]nn (6)+(Capopen)(12)├openn:Cap[S1]66 (2)，僅能使用(ProcCap)(13)├P:S177 同(12)(14)67=267=2 同(12)(15)Sn=S1n=6n=6 (11)(12)(16)n7=2n7=2 (14)(15)(17)├P|Q1|Q2:S188 (13)(9)(15)+(ProcPar)(18)75=875=8 同(17)(19)5n (10)(8)+的傳遞性(20)57n7 (19)+性質(zhì)3-5(21)82 (18)+性質(zhì)3-1,(16)+的傳遞性(22)81 (2