（计算机软件与理论专业论文）安全移动资源的语义、类型系统及其代数性质的研究.pdf

安全移动资源演算的语义、类型及其代数性质的研究 摘要 移动资源演算( m r ) 是一种用于描述携带资源的移动系统及其交互的形式化方 法，它隶属于灰箱演算的一支灰箱演算由c a r d e l l i 提出，最初被称为移动灰箱演算 ( m a ) ，本文将绝大部分由灰箱演算发展而形成的进程代数系统称为类灰箱演算。本 文以移动资源演算的一个变体一一安全移动资源演算( s r ) 作为研究对象，从操作语 义、类型系统、进程等价性和表达能力等方面对其进行了研究 首先，本文在分析现有移动资源演算及相关的类灰箱演算( 诸如移动灰箱m a ， 安全灰箱演算s a ，盒灰箱b a 等) 不足的基础上，提出通过增加协动作并限制协动作 的实施对象来提高安全性的思想，并以此为指导给出s r 的语法和归约语义 其次，本文研究了s r 的类型问题，提出一套可以解决移动资源演算中存在的进程 干扰问题的位置类型系统( l s ) 由于在移动资源演算中引入了灰箱路径作为能力操 作对象的语义，因而进程的干扰问题变得更错综复杂，而且原先类灰箱演算干扰问题 相关研究成果以及解决方法无法妥善地解决基于灰箱路径的操作语义所带来的相关问 题，进程在不同层次的灰箱结构中对同一灰箱路径的访i 可无法通过已有的系统得到控 制本文利用对携有灰箱路径的能力设定相应的位置类型，进而为携有相关路径的进 程记录其访问目的的类型值，配合特殊的位置类型构造，表示位于不同的灰箱层次内 进程的访问地点的特性，解决了移动资源演算的巢式干扰问题l s 系统可以有效地 追踪进程的访问地点，并支持子类型关系，该系统还可以和传统的类型属性，如移动 性和线程数，构成复合类型系统 再次，本文参照l e v i 研究s a ，以及g o d s k e s e n 研究m r 等价性使用的方法，对s r 进行了类似的研究首先引入s r 进程的标号动作和固化结果，用于将进程中可能参 与归约的部分与剩余的部分分开在标号动作和固化结果的基础上，按照进程的归约 特性给出s r 基于提交关系的标号转移语义，并逐一分析这些规则与归约规则的对应 关系，并证明标号转移语义和归约语义的等价性在标号转移语义的基础上，研究了 判定进程观察互模拟等价的一般方法，得出s r 进程的观察互模拟等价关系与标号互 模拟等价关系是同一关系的结论，并给出s r 进程与上下文( 含路径上下文) 发生交互 的各种可能，作为判定进程等价的一般性结论 此后，本文综合类型系统和等价性判定的结论，给出用于判定进程等价的一些代 数定律，同时使用这些定律证明移动资源的线性特征和数字签名卡例子在给定条件下 的正确性这些例子不仅示意了等价性定律的具体使用方法，同时也体现了s r 较之 m r 在安全性方面的优越性 最后，本文利用上述等价性定律给出并证明了s r 演算翻译”演算的一个方案，弥 补了移动资源演算作为灰箱演算的一个分支，到目前为止尚缺乏对表达能力的研究， 有力地说明s r 在提高安全性的同时，没有失去灰箱演算应有的表达能力 本文的主要创新性体现在以下几个方面 ( 一) 对利用新增的可供三方同步的协动作，以及相关的能力参数加强移动资源演 算安全性这一命题进行了研究，提出了移动资源演算的变体s r 通过利用协动作参 数加强交互双方的彼此控制，s r 在安全控制方面比起m r 来有一定优势同时，对协 动作参数进行控制后，s r 并没有丧失m r 所具有的表达能力 ( 二) 针对移动资源演算中存在的进程干扰问题给出了支持访问位置类型特性的类 型系统o s 该系统通过区分不同灰箱层次( 即不同灰箱路径) 下进程的位置类型， 可以精确地避免不同的进程对同一访问地点产生非朴素干扰的现象，并支持子类型关 系考虑到l s 系统的独立性，l - s 在设计时还考虑到和传统类型属性整合的可能性， 并给出了复合类型系统的框架 ( 三) 有别于g o r d o n 和c a r d e l l i 基于硬化关系的上下文等价方法，本文借鉴l e v i 和 s a n g i o r g i 基于固化结果和提交关系所引入的标号互模拟等价性，给出了s r 中判定进程 等价性的一般性方法；同时结合位置类型系统，证明了在给出的类型环境r 下s r 进 程的等价性定律 ( 四) 本文借助自行推导的s r 进程的等价性定律完成对”演算翻译的代数方法证 明，较之z i m m e r 的证明方法来得更为简明另外，本文将前人对移动资源演算以及相 关的类灰箱演算的语义、等价性、表达能力等方面的研究成果结合本文s r 演算在这 些方面的研究和探索进行了贯穿和融合 关键词计算理论，进程代数，类型系统，灰箱演算，移动资源演算 t y p es y s t e ma n da l g e b r a i ct h e o r y o fs a f em o b i l er e s o u r c e s a b s t r a c t t h ea m b i e n tc a l c u l u si saf o r m a lm e t h o dm o d e l l i n gr e s o u r c e s c a r r y i n gm o b i l es y s t e m sa n dt h e i r i n t e r a c t i o n s t h i st h e s i sm a i n l yf o c u s e so nt h ec a l c u l u so fs a f em o b i l er e s o u r c e sr o b u s t ( s r ) 一a v a r i a t i o no ft h ec a l c u l u so fm o b i l er e s o u r c e s f u n d a m e n t a lr e s e a r c ho nt h eo p e r a t i o n a ls e m a n t i c s ， t y p et h e o r y ，b e h a v i o re q u i v a l e n c ea n de x p r e s s i v e n e s so fs ra r ec a r r i e do u ti ni t f i r s t l y , b ya n a l y z i n gt h ei n a d e q u a c i e sf o u n di nt h ee x i s t i n gc a l c u l u so fm o b i l er e s o u r c e s ( m r ) a n dr e l a t e da m b i e n t l i k ec a l c u l u s ( m o b i l ea m b i e n t s ，m o b i l es a f ea m b i e n t s ，b o x e da m b i e n t s ，e t c ) ， a 1 1a p p r o a c hi sp r o p o s e dt h a tc a ni m p r o v et h o s ei n a d e q u a c i e sb ya d d i n gc o - a c t i o n sa n du t i l i z i n g t h ep a r a m e t e r so fc c - a c t i o n st ol i m i tt h ep r o c e s s e s v i s i t i n gt a r g e t s b a s e do nt h i s ，t h es y n t a xa n d r e d u c t i o ns e m a n t i c so fs ra r eg i v e n s e c o n d l y , t h et y p es y s t e mo fs ri ss t u d i e d at y p es y s t e mn a m e dl - si sp r o p o s e dt os o l v et h e p r o c e s si n t e r f e r e n c e sp r o b l e me x i s t i n gi nt h ec a l c u l u so fm o b i l er e s o u r c e s b e c a u s eo ft h ei n t r o d u c t i o n o fa m b i e n tp a t ha st h ep a r a m e t e ro ft h ec a p a b i l i t i e si nm o b i l er e s o u r c e s ，t h ep r o c e s si n t e r f e r i n g p r o b l e m sb e c o m em u c hm o r ec o m p l i c a t e da n du n p r e d i c t a b l e ，a n dc u r r e n ta p p r o a c h e sf r o mf o r m e r r e l a t e ds t u d i e si na m b i e n t - l i k ec a l c u l u sc a n n o tc o m p l e t e l ys o l v et h ea m b i e n tp a t hb a s e dp r o b l e m si n s r i nt h i st h e s i s ，b ys e t t i n gl o c a t i o nv a l u e st ot h o s ee a p a b i l i t i e sw i t ha m b i e n tp a t h ，r e c o r d i n gt h e p r o c e s sw i t hi t sv i s i t i n gt a r g e t s v a l u e ，a n da p p l y i n gt h es p e c i a lc o n s t r u c t i o no fl o c a t i o nv a l u e s ，w e s o l v et h en e s t e di n t e r f e r e n c e sp r o b l e mi ns r t h el - sc a ne f f e c t i v e l yt r a c kt h ev i s i t i n gt a r g e t so ft h e p r o c e s s e s ，i ta l s os u p p o r ts u b t y p er e l a t i o n s b e s i d e s ，t h i ss y s t e mc a nb ec o m p o s e dw i t ht r a d i t i o n a l t y p ep r o p e r t i e s ，s u c ha st h r e a d n e s sa n dm o b i l i t y ，t ob eac o m p o s i t et y p es y s t e m t h i r d l y ，f o l l o w i n gl e v i sw a yi ns aa n dg o d s k e s e n sw a yi nm re q u i v a l e n c er e s e a r c h ，s o m e p r o c e s se q u i v a i e n c ep r o p e r t i e so fs ra r es t u d i e d b yi n t r o d u c i n gl a b e la c t i o n sa n dc o n c r e t i o n st h a t s e p a r a t e dt h ea c t i v ep a r to f ap r o c e s sf r o mt h er e s i d u e ，ac o m m i t m e n tr e l a t i o nb a s e dl a b e l l e dt r a n s i t i o n s e m a n t i c si s 百y e na n dp r o v e ds o u n dw i t hr e g a r dt ot h er e d u c t i o ns e m a n t i c sd i s c u s s e db e f o r e t h e n l b a s e do nt h i sl a b e l l e dt r a n s i t i o ns y s t e m ，t w or e s u l t sf o rp r o v i n gt h ee q u i v a l e n c er e l a t i o n so fp r o c e s s e s a r eg i v e n ，at h e o r e mt h a te q u a t e st h eb a r b e db i s i m u l a t i o ne q u i v a l e n c er e l a t i o nw i t ht h el a b e l l e d b i s i m u l a t i o ne q u i v a l e n c er e l a t i o n ，a n ds o m el e m m a st h a te n u m e r a t e st h ew a y sap r o c e s sm a yi n t e r a c t w i t ha n yc o n t e x t si n c l u d i n gp a t hc o n t e x t s f o u r t h l y , b a s e do np r e v i o u sr e s u l t so l lt y p es y s t e ma n dp r o c e s se q u i v a l e n c e s ，s o m ea l g e b r a i cl a w s f o rp r o c e s se q u i v a l e n c ea r eg i v e n t od e m o n s t r a t et h e i ru s a g e s ，t h er e s o u r c el i n e a r i t ye x a i n p i ea n dt h e d i g i t a ls i g n a t u r ec a r de x a m p l ea r ep r o v e nt h r o u g ht h e m ，u n d e rc e r t a i nc o n s t r a i n t s ，t h e s ee x a m p l e s i l l u s t r a t et h ea d v a n c e ds e c u r i t yf e a t u r e sp r o v i d e db ys r f i n a l l y , t h ee n c o d i n go ft h e c a l c u l u si n t os r i sg i v e na n dt h eo p e r a t i o n a lc o r r e s p o n d e n c ep r o v e d u s i n gt h ea l g e b r a i cl a w s a sab r a n c ho ft h ea m b i e n tc a l c u l u s ，t h i sr e m e d i e st h el a c ko ft h es t u d yi n e x p r e s s i v ep o w e r i ts h o w st h a tb yl i m i t i n gt h ep a r a m e t e r so fc o - a c t i o n si nr e d u c t i o n ，s rs t i l lh o l d s t h es t r o n ge x p r e s s i v ep o w e ro fi t sa n c e s t o r s t h em a l nc o n t r i b u t i o n so ft h et h e s i sa r es u m m a r i z e db e l o w t h er e s e a r c ho ns rh e r es h o w st h a t ，b yf u r t h e rr e s t r i c t i n gt h en e w l y - a d d e dc o - a c t i o n sf o rt h r e e - p a r t ys y n c h r o n i z a t i o n ，s rh a sb e t t e rs e c u r i t yc o n t r o lo v e rs a ，a si s d e m o n s t r a t e db yt h ed i g i t a l s i g n a t u r ec a r de x a m p l e m o r e o v e r ，u p t o - n o w ，t h e r ei sn oe v i d e n c et h a ts ri sl e s se x p r e s s i v et h a n m r t od e a lw i t ht h ep r o c e s si n t e r f e r e n c ep r o b l e m si nt h ec a l c u l u so ft h em o b i l er e s o u r c e s ，w ep r o p o s e al o c a t i o ns y s t e m ( l s ) t os u p p o r tv i s i t i n gl o c a t i o nt y p e sf o rp r o c e s s e s b yd i f f e r e n t i a t et h ep r o c e s s e s l o c a t e di nd i f f e r e n tn e s t e da m b i e n tp a t h ，l - sc a l lc o n c i s e l ya v o i dt h en o n - p l a i ni n t e r f e r e n c e si n c u r r e d b yd i f f e r e n tp r o c e s s e sa c c e s s i n gt h es a m et a r g e tl c o a t i o n ，a n dt h i ss y s t e ma l s os u p p o r ts u b t y p er e l a t i o n w i t hr e s p e c to ft h ei n d e p e n d e n c yo fl - s w ec o n s i d e rt h ep o s s i b i l i t yt h a tl sc a r lb ei n t e g r a t e dw i t h t h et r a d i t i o n a lt y p ea t t r i b u t e sa n dp r o p o s et h ef r a m e w o r ko ft h ec o m p o s i t et y p es y s t e m t h i st h e s i sa l s op r o v i d e sn e wp r o o fm e t h o df o re q u a t i o n a ll a w s ，t h r o u g hg o d s k e s e n sm o b i l e r e s o u r c e s m o r e o v e r ，t h eo p e r a t i o n a lc o r r e s p o n d e n c ep r o o fo ft h e 口e 。ce n c o d i n gi sa l g e b r a i c ，w h i l et h e o r i 舀n a lp r o o fb yz i m m e r i ss o m e w h a t m o r ec o m p l e x k e yw o r d st h e o r yo fc o m p u t a t i o n ，p r o c e s sa l g e b r a ，t y p es y s t e m ，a m b i e n tc a l c u l u s ，m o b i l e r e s o u r c e s 文中用到的符号及含义 中文含义 s r 进程 灰箱名 资源名 能力 标号动作 结构同余关系 归约关系 位置单型 简单位置类型 复合位置类型 类型环境 固化结果 结形 标号转移关系 上下文 路径上下文 观察结论 工化观察结论 观察模拟 观察互模拟 观察互模拟等价 标号模拟 标号互模拟等价 英文含义 p r o c e s s a m b i e n tn a m e r e s o u r c en a m e c a p a b i l i t y a c t i o n s t r u c t u r a lc o n g r u e n c er e l a t i o n r e d u c t i o nt e l a t i o n s i n g l et y p e s i m p l et y p e l o c a t i o nt y p e t y p ee n v i r o n m e n t c o n c r e t i o n o u t c o m e l a b e l l e dt r a n s i t i o nr e l a t i o n c o n t e x t p a t hc o n t e x t o b s e r v a t i o n ，o rb a r b o b s e r v a t i o nr e s p e c tt ol b a r b e ds i m u l a t i o n b a r b e db i s i m u l a t i o n b a r b e db i s i m n l a t i o ne q u i v a l e n c e l a b e l l e ds i m u l a t i o n l a b e l l e db i s i m u l a t i o ne q u i v a l e n c e 定义页码 1 9 1 9 1 9 1 9 4 9 2 3 2 4 2 9 2 9 2 9 3 0 5 0 5 0 5 0 2 3 2 3 6 5 8 4 6 6 6 6 6 6 6 8 6 8 号吼m 乱 妒 十 ， 0 衔川ma n兰一sr r七。气“h增矿“5 上海交通大学学位论文答辩决议书 申请者i l傅城0 所在学科( 专业) 0 i 十算机软件与理论 安全移动资源演算的语义、类型及其代数硅度的研究 答辩日期1 12 0 0 5 - 1 卜0 5 犷答辩地点0 上海交通大学 答辩委员会成员 签名 委员l | 虞慧群i l 教授l 华东理工大学 委员l l 孙永强i | 薯女授0 上海交通大学 委员f j 徐良贤 | 教授f 性海交通大学 匝亟亘蟹二二 固亟亘塑二二 委员| | 黄林鹏| 教授 委员 评语和决议： 傅城同学的博士学位论文安全移动资源演算的语义、类型及其代数性质的研究， 对安全移动资源( s r ) 演算的语法、类型系统、操作语义、等价性判定与定律、以及表 达能力等方面进行了研究。其工作具有重要的理论意义和实用价值，论文的主要工作及 创新性在丁| ： 1 提出了使用协动作参数加强交互双方的彼此控制， s r 演算在安全控制方面比 移动资源( m r ) 演算更严格。同时，增加协动作控制后，s r 演算并没有矗失 m r 演算所具有的表达能力。 2 3 发现了原先m r 演算中存在巢式干扰的问题，并提出了解决该问题的一个有效 方法二位置类型系统l - s 。该系统在设计过程中考虑到了与携有移动属性的类 型系统的正交性，而且可以无缝的与灰箱演算研究中形成的娄型系统进行融合a 建立了s r 演算巾基于固化结果和提交关系所引入的标号互模拟等价性，班及判 定进程等价性的方法；同时结合位置类型系统，证明了在给出的类型环境下s r 进程的等价性定律。 4 征自行推导的s r 进程等价性定律基础上，完成了对p i 演算翻译的代数方法证 明，较之z i m m e r 的证明方法来得更为简明。将前人对移动资源演算以及类灰箱 演算的相关研究和探索进行了贯穿和融合。 论文条理清晰，行文流畅，论证严谨，反映作者掌握了坚实宽广的基础理论和系统 深入的# 业知识，独立科研工作能力和创新研究能力强。 表决结果 答辩过程中讲述清楚，回答问题正确。经答辩委员会无记名投票，一j 致通过傅城同学的博士学位论文答辩，建议授予工学蛙兰焦：一，一 答辩委员会主席i 殇以加( 签名) 心一强画 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究工作所取得的成果。除文中已经注明引用的内容外， 本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。 对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式 标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：锄孽“ 日期：年月 目 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位 论文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印或扫描等复制手段保存和汇编本学位论文。 保密口，在年解密后适用本授权书。 本学位论文属于， 不保疆争口： ( 请在以上方框内打“4 ”) 学位论文作者签名：瓢 日期：沙薛i 月、日 乏 日 旃夥 名 年 雠 眸 师 蛳 埘 影 期 指 日 第一章概述 在日常生活中，一些移动计算资源( m o b i l ec o m p u t i n gr e s o u r c e s ) 经常从其他一些计算资源 中进进出出常见的有在s i m 卡和下一代信用卡技术领域应用的智能芯片卡“，它可用于读卡 器、移动电话和自动应答机器( a t m ) 等设备当并发系统内存在移动计算资源时，是否具有能 够演绎系统行为正确性的能力，以及对系统设计和实现工具的迫切需求，越来越成为人们关注的 热点而本文所作的研究移动资源演算( ac a l c u l u so fs a f em o b i l er e s o u r c e s ) 旨在为 位于有名( n a m e dl o c a t i o n ) 且容量有限的场所内、含有嵌套关系的( 具有树状结构的，n e s t e d ) 移动资源进行形式化设计和建模 移动计算资源属于分布计算中移动计算领域的一个分支以移动计算的研究领域而沦，该方 向涵盖了操作系统( o p e r a t i n gs y s t e m ) 、通讯网络( 有线和无线) 、计算机网络、程序设计语言 ( p r o g r a m m i n gl a n g u a g e ) 、集群系统、阿格计算、分布式系统、嵌入式系统等研究领域同时， 由于研究的侧重点不同，对移动计算中移动性一词的理解也存在两种完全不同的涵义：一方面， 对于熟知无线通讯网络和通讯协议的研究人员来说，移动一词的含义为其生活中的本义，表示物 现实世界中计算设备的移动；另一方面，在分布式计算和并行计算的研究领域，移动一词通常意 眯着软件意义上的移动，其代表为研究代码在不同的计算蓑体上迁移的技术1 1 。o 在英文中 通常将前者称为m o b i l ec o m p u t i n g 将后者称为m o b i l ec o m p u t a t i o n 5 】；为了在汉语中区分这两 种术语，暂且将前者译为硬移动，将后者译为软移动本文的工作属于软移动的范畴 近几年来，随着移动计算的不断发展，对该研究领域形式化方面的研究成果主要体现在： 口 演算方面，由于其可以很好的描述进程间基于通道的通讯，甚至进程在通道中的移动口) ，但作为 描述移动计算方面的形式化模型，尤其是描述移动计算中普遍存在的进程和资源的位置分布、进 程在不同位置闯的移动以及由此带来的安全性问题，一般意义上的- 演算并不适合矧，因而有 以”演算”1 为基础，其上增加表示进程和资源分布构造的些变体f 5 ”5 5 ；a 演算方面，作 为顺序执行程序领域经典的形式化模型代表，在 演算”】基础上增加代码移动原语的a d i s t 演算 4 2 】；其他方面，在j o i n 演算“”基础上增加树状位置分布和位置失效( f a i l u r e ) 概念的分布式j o i n 演算，以及专门用于描述移动计算模型及其安全性的灰箱1( a m b i e n t ) 演算”1 ”和s e a l 演算 ”本文的研究工作主要围绕灰箱演算的一个变体系统一移动资源演算一展开讨论 g o d s k e s e n 等人最初受到移动灰箱演算限删( m a ) 的启发提出了移动资源演算i s 2 ( m r ) ， 目的在于通过个形式化框架来表达和证明关于安全方面的移动资源的性质。这些资源是基于不 可复制和不可修改的特点而设立的m r 演算从形式上看将盒灰箱演算1 ( b a ) 、s e a l 演算 】，连同几种分布式进程代数”，1 ”联系到一起，但是由于设计目标上的不同，m r 和这些代 数系统之间也着重要差异为了阐述本文所作研究的动因，下面将先对m a 和m r 演算作简要的 1 关于a m b i e n t 的译名，本文沿用文献1 5 1 中的翻译，即用4 灰箱。一词t 箱字取自其整体移动性，灰宇取自其 内部结构部分可见、部分不可见之意一一发生归约的部分可见，其余不可见采用直译译名一环境- 一词不能很好 的表进a m b i e n t 作为名词代表移动的软硬件对象这屡含义 2第一章概述 介绍，然后分析这些系统的不足之处，最后给出本文的立论依据本文将所有以m a 演算为基础 发展的各种演算框架统称为类灰箱演算 1 1 1 移动灰箱演算 移动灰箱演算( m o b i l ea m b i e n t ，以下简称m a ) 是1 9 9 8 年由c a r d e l l i 等人提出，该演算是 移动计算领域中比较热门领域，它被提出的动因在于现有的演算无法在同一个框架内同时描述软 移动和硬移动该演算受到w w w 中移动计算的潜力所启发：因特网的地理分布自然导致软计算 作为一种灵活控制延迟和带宽的机制而存在然而，在w w w 上实现软计算的难点并不在于移动 本身，而在于域p 1 出于安全的考虑系统管理员实施一系列的安全策略将域与因特网通过防火 墙进行隔离该演算旨在在单一的幄架中同时描述软汁算和硬计算，并且能够描述进程在域间的 移动基于广域网络中资源和进程的树状嵌套结构，灰箱演算中的核心概念一一灰箱( a m b i e n t ) 体现为一个有界的、树状嵌套的计算场所 在m a 这单一的计算框架之下，灰箱既可以用于表示计算代码也可以表示计算代码的载体一 设备移动原语身并不区分灰箱所代表的实体类型因此，抽象的移动实体一灰箱成为研究的主 要目标，从而软移动与硬移动便能在同一个框架之下进行建模灰箱演算中，计算的移动性主要 体现为灰箱的移动下面介绍一下灰箱演算的一些基本行为- n i nm 尸】im q 】m 如f p 】i 翻这里每对“i 】”表示一个灰箱，每个灰箱前有一个名字， 用于标识这个灰箱符号“i ”在并发模型中表示进程的并发运行，在灰箱演算中，还表示 灰箱的并置，大写字母p 、0 、r 等代表任意进程表达式其中归约步骤( 符号。_ ”) 表示进程的归约关系，可理解为计算的进行这个例子表示进程i nm p 运行在灰箱n 内，进 程口运行在灰箱m 内其中i nm 代表进入灰箱m 的原语，该原语能够实掩当且仅当灰箱 m 与直接包含该原语的灰籀处于平行结丰每( 即并量) 在该愿语实簏后。灰箱n ( 连同其内进 程p ) 便可进入灰箱m 。 m n o u t m p lq 】n p l m q 这里进程o u t m p 运行在灰箱n 内，而灰箱n 和进程0 同时运行在灰箱m 内其中，o u tm 表示离开灰箱m 的原语该原语能够实施当且仅当直 接包含该原语的灰箱在灰箱m 内在该原语实施后，灰箱1 2 连同其内的进程p 便可移出灰 箱m o p e n n p n q 】- - - ) p l q 这里进程o p e n n p 和灰箱n 处于平行结构其中。原语o p e n n 表 示打开灰箱n ，当灰箱n 打开后即被删除，其内的进程会被释放，从而取代原先n 留下的位 置该原语能够实施当且仅当灰箱n 与它并置 从以上三个例子我们看到，灰箱具有主动移动的特点，不需要载体而且打开灰箱的语义可 以造成多个线程从灰箱内部释放，这样就可以获得封装在灰箱内的消息( 线程) ，因此对基于消息 传递的演算进行编码模拟也就变得可越( 当然，灰箱演算也引入了搂息传递机制，不过对纯灰籍 演算的研究似乎更容易一些) 灰箱的树状嵌套模型和三个动作原语i n 、o u t 和o p e n 体现了灰箱演算的核心内容无论 是物理计算设备的移动还是软件代码的移动，都被抽象为灰箱的移动由于该模型直观、精简， 并且拥有惊人的表达能力( 仅这三个基本动作就可以翻译同步f 演算“) ，这使得灰箱演算的研 i 1 动因 3 究成为移动计算形式化方向一个非常活跃的领域c a r d e u i 等人利用穿越防火墙的例子来说明该 演算的表达能力，这也是设计该语言的初衷： f i r e w a i l 兰( ) w k o n t i n 砂i nw 】io p e nn o p e n 砂尸 a g e n t 兰 o p e nk p i 】 f i r e w a l la g e n t ； ( p ) ( 肚 o u tw i 7 i nw 】io p e n o p e nk ”p i o p e nk k ” 0 】 ) _ + ( ) 舢【。p 8 n g t o p e n p l lk 仕【妞1 1 3 i o p e n 【q m + ( v w ) ( w o p e nn o p e n 砂p 】【i nt ，l 女” 0 】) ( p ) ( w o p e n o p e n 砂pl 女似”旧1 ) 一( p m ) ( ”【尸l 刎) 我们看到，a g e n t 要将口送入进入f i r e w a l l ，首先要知晓三个名字一，然后f i r e w a l l 就 可以将0 从a g e n t 中取出，并让它进入f i r e w a l l 实际上，这里有一个假设，即把k ，k ，k ”看作 是对称密钥，只有a g e n t 和f i r e w a l l 之间知道这样，任何一个q 既可以畅通无阻通过防火墙 了这里有一点值得注意，就是任何进程都无法感知( 体现为约束名) 防火墙的存在，因此也 就不存在针对性地攻击，所以它可以被视为完美的防火墙 最初由c a r d e l l i 和g o r d o n 提出的灰箱演算称为移动灰箱( m o b i l ea m b i e n t ) 演算( 以下简称 m a ) ”】随着研究的不断深入，m a 也暴露出一些设计上的不足l e v i 和s a n g i o r g i 在文献【14 】 中首次指出m a 在语法上存在冢干扰( g r a v ei n t e r f e r e n c e 】问题一一由于灰箱原语动作的单方参 与性，归约顺序的不同将会导致完全不同的结果例如以下的m a 进程表达式： h 【】i n f i n h f m o u tn p 】 ( 1 - 1 ) 可归约为( 首先灰箱n 经i n 动作进入h ，之后灰箱m 经。u tn 动作移出n ，即：先i n 后o u t ) + h n f m o 们 p 】+ m 】i m p 】 也可归约为( 先o u t 后i n ) l _ h n 【i n h i l m 【p _ h l n 【 1 m 【p 】 ( 1 2 ) ( 1 3 ) 虽然并发和分布模型中进程的归约不再具有顺序程序执行时的礴定性，但是在以上两种归约 结果中，不确定性却超出了可以解决的范围：进程m p 】由于无法知道自己的确切位置，从而影响 后续的归约( 必然有一种情况使m f p 】无法顺利进行后续的计算) 更严重者，可能发生这种冢干扰 的进程很难使用类型系统( t y p es y s t e m ) 来识别上述冢干扰问题使得m a 的代数理论( a l g e b r a i c t h e o r y ) 比较薄弱、进程的等价性不易判定，导致程序的正确性很难验证 1 1 2 移动资源演算 移动资源演算( m o b i l er e s o u r c e s ，以下简称m r ) 由g o d s k e s e n 等人提出，该演算属于移动 演算的一种，是基于语义的移动m r 虽然是m a 的变体，但是语法和语义却有很大的变化，甚 至还融入了三方进程的同步语义在m r 中灰箱又被称为有名槽( n a m e ds l o t ) ，形式上同m a 相同，如砒d 】表示进程( 或资漂) p 位于灰箱n 内除此。灰箱可以有多个别名( a l i a s ) ，如在 4第一章概述 表达式q l m ，n m 中，m 和n 都标识了同一个灰箱我们可以用元表示一个名集，用于表示一 个有多个名字的灰箱，如乔嘲在m r 中，灰箱不能被打开，但是可以被删除，我们在名集中使 用帅表示该灰箱可以被删除，如 m ，4 n ) 嘲可以通过名字n 被删除，只要有进程知晓名n 即可 m r 进程的移动行为由一个监控( 或旁观) 进程来实旌的，我们使用n i n 2 睁丽表示把位于灰箱路 径( 即灰箱嵌套的树状路径) n ，n 2 内的资源( 即内部进程) 搬到路径m 下下面介绍一下m r 演 算其中三种基本的计算行为： n l n 2p m p 1 i n l b l n 2 慨m 甄】+ p l i n l p 2 l n 2 - 】l m b i p 4 】这是一个三方进程同步的行 为，当n l n 2 m 实施后，位于平行结构的灰箱路径n - n 2 内的进程p 3 被挪到了另一个位于 平行结构的灰箱m 中，被移入的进程船和在m 内已有的进程肌处于平行结构 i n p f m ，唧) 酣p 如前所述。灰箱m 因为有别名唧，所以它允许其他进程将其删除 这里，进程5 n p 必须与被删灰箱处于平行结构，当动作4 n 实施后，灰箱m 连同其内的进程 q 均被删除 n m a p l n m k q 】| r 】+ p i n f m 嘲这里的n 在m r 演算中表示资源，资源的消费在归约形 式中体现为单纯的同步此间，并无任何消息传递和进程移动的结果产生 m r 演算最重要的特点为进程的移动是在三方构成的合约中完成的这比较复合资源访闻和使用的 特点，即“使用资源的地点由资源的使用者决定”从上述第一个例子可以看到进程n - n z m p - 为资源的使用者，灰箱 2 为资源的提供场所，灰箱m 为资源的使用场所该演算最著名的应用 为数字签名卡t e n c k 竺! ( r e g ) ( i n 而1 r e g 睁石蕊m g 【小1 ) 旧“小】 d e c k 兰t ( r e o ) ( i n 而g r e 9 ；爵ir e 口【】) i i n o 】lo u t * 】 其中r e 9 表示寄存器，i n ，o u t 分别表示输入输出缓冲加密进程为e n e ，其参数k 表示密钥， 该进程负责不断的对输入缓冲( i n ) 内的资源进行加密，然后将其返回至输出缓冲内( o u t ) 相应的解密进程为d e c k ，其参数k 即为密钥。该进程不断对进入输入缓冲( i n ) 的资源进行解 密，然后将结果返回到输出缓冲o u t 内 如果密钥为全局可知，则任何人都可以用它来加密或解密而另一方面，如果仅在通信 的双方共享，例如a l i c e 的加密进程作为一个私有资源，b o b 的解密进