资源描述：
《移动灰箱演算中强干扰问题的进一步控制A.doc》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、移动灰箱演算中强干扰问题的进一步控制管旭东杨怡玲尤晋元上海交通大学计算机科学与工程系(200030){guan-xd,yang-yl,you-jy}@cs.sjtu.edu.cn摘要：为了消除灰箱演算(MA)中的强干扰问题，Levi等人在灰箱演算的基础上引入了反动作的概念，并提出了一套安全灰箱演算系统(SA)。然而，SA所引入的反动作却带来了安全上的隐患。本文提出的鲁棒灰箱演算系统(ROAM)在依靠反动作解决强干扰问题的同时，根据反动作的参数明确了该反动作的使用对象，以消除SA中引入的不安全因素。
2、通过对防火墙跨越和多元异步p-演算的描述显示ROAM依然保留了MA和SA较强的表达能力。同时本文就ROAM的类型问题作了初步的探讨，给出并证明了一套ROAM演算的类型系统。该类型系统可以表达进程和能力的移动性和线程数两个属性。关键词:进程代数，移动灰箱演算，安全移动灰箱演算，鲁棒灰箱演算，类型FurtherControlontheGraveInterferenceinMobileAmbientsXudongGuan,YilingYang,YinyuanYouDept.ofCompuerSci.&E
3、ng.,ShanghaiJiaotongUniv.,China,200030{guan-xd,yang-yl,you-jy}@cs.sjtu.edu.cnAbstract.MobileSafeAmbients(SA)wasproposedinordertoremovethegraveinterferenceintheMobileAmbientcalculus.ButthecoactionsintroducedinSAalsobringsomesecuritybreaches.Inthispaper
4、,asimilarcalculuscalledRobustAmbients(ROAM)wasproposedasamorerationalsubstituteforSA.Throughsepcifiyingtheparametersofthecoactions,theambientsinROAMaremorerobustagainstmalicioustampering.Theencodingofpolyadicasynchronousp-calculusinROAMshowsthatROAMdo
5、esnotlossthestrongexpressivenessofitsancestors.AfundamentaltypesystemforROAMwithboththreadcountandmobilityattributeswasalsoproposedandprovedinthepaper.Keywords.processalgebra,MobileAmbient,MobileSafeAmbient,RobustAmbient,typeCardelli和Gordon在文献[1]中首先提出
6、了可以统一描述移动计算中的计算平台移动性和计算代码移动性的移动灰箱（MobileAmbient-MA）演算（箱字取自其整体移动性，灰字取自其内部结构部分可见、部分不可见之意——发生归约的部分可见，其余不可见）。灰箱（ambient）是一个可以整体移动的计算场所。灰箱之间表现为树状嵌套关系，可以直观地描述互联网上的自治域及防火墙、自治域中的子域及计算设备、移动代理运行环境及其内部的移动代理程序等。无论是一个企业Intranet网络、一台便携式计算机，还是一个移动代理，在MA中都统一地被形式化为一个灰
7、箱。同时，灰箱的边界具有保护作用，只有穿越边界进入某灰箱的内部，才能与之发生信息交换。MA对移动计算中的计算性和移动性描述有很好的形式化支持。随着研究的不断深入[2,3,4,5]，MA也暴露出一些设计上的不足。文献[2,3,4]试图从类型的角度进行弥补，但是引入了太多的条件限制，且效果不理想。Levi等人在文献[6]中首次指出MA在语法上存在强干扰（graveinterference）问题——由于灰箱移动的单方参与性，归约顺序的不同将会导致完全不同的结果。例如以下的MA表达式：h[]
8、n[inh
9、
10、m[outn.P]](1)可归约为（首先灰箱n经inn动作进入h，之后灰箱m经outn动作移出n，即：先in后out）®h[n[m[outn.P]]]®h[n[]
11、m[P]](2)也可归约为（先out后in）®h[]
12、n[inh]
13、m[P]®h[n[]]
14、m[P](3)由于存在(2)(3)两种不同归约结果，P无法判断m的具体位置，从而影响后续的归约。文献[6]在指出强干扰问题的同时，也提出了一种解决方法，通过引入移动的双方参与性来约束归约的顺序，即为每个动作（action）配置相应
