全局类型和网络服务的移动进程保护方法

网址：http://www.elsevier.nl/locate/entcs/volume54.html14页全局类型和网络服务G. 法拉利文凭 意大利比萨大学InformaticaE. 莫吉意大利热那亚大学DISIR. Pugliese文凭 di Sistemi e Informatica，意大利摘要移动性似乎是全球计算的一个基本方面，但它引起了许多相关的安全问题。我们解决的问题，保护- ING主机免受攻击或不当行为的移动进程。我们建议移动过程抽象，即。相对于具有局部含义的操作参数化的进程，而不是准备运行的进程或活动进程（代理）。此外，我们利用全局值和类型来确保具有本地含义的操作仅在本地使用我们的方法是通用的，可以应用于每一种语言/系统的编程和协调网络服务，允许远程通信与代码片段的传输我们通过使用Klaim语言来说明我们的方法，其中网络服务通过网络服务存储库内的元组进行编码，例如，在SUN JavaSpace和IBM TSpace中。1引言在全球计算中，进程移动性似乎是一个基本方面，然而它引起了许多相关的安全问题。例如，移动进程威胁主机盗窃或滥用系统资源（例如信息，金钱，CPU时间，磁盘空间，带宽）。这可能会降低主机的性能或损害其安全性和声誉。反过来，主机威胁移动进程窃取资源（例如信息）和声誉（例如，主机可以将其自己的任务植入到？ 工作得到欧盟工作组APPSEM和MURST项目SALADIN和TOSCA的支持。c2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2在其他主机上执行的进程），并有可能杀死这些进程。在本文中，我们解决的问题，保护主机免受攻击或不当行为的移动进程。为了克服这个问题，在文献中已经提出了不同的解决方案，例如，[2019 - 04 - 19][2019 - 04 - 19][2019 - 04][2019 - 04 - 19][2019 - 04][2019- 04 - 19][2019 - 04 - 19]为了对移动进程的行为进行新粒度的控制，并直接编程和管理安全策略，我们建议移动进程抽象，即从本地操作中抽象的进程代码，而不是准备运行的进程或活动进程。要完成迁移，必须首先在源主机和目标主机之间进行通信。然后，目标主机可以通过定义所有潜在危险的操作来实例化接收到的流程抽象，并且可以将所得到的流程包装在负责流程执行的定制环境中。换句话说，取决于所接收的代码的可信度，代码在其上被抽象的本地操作可以用正确安全级别的本地操作的实现来实例化，从而避免对本地资源的不期望的访问。我们的方法是通用的，可以适用于每一种语言/系统的编程和协调网络服务，允许远程通信与代码片段的传输。然而，把它在一个具体的形式，在本文中，我们将我们的方法应用到一个特定的语言。我们将考虑语言Klaim1（用于代理交互和移动性的内核语言），这是一种实验性内核语言，受Linda协调模型[11，5]的启发，专门设计用于建模和编程利用代码移动性的分布式并发应用程序。因此，遵循Klaim方法，我们假设网络服务通过网络服务存储库内的元组（即多个分布式元组空间）进行编码。我们注意到Jini [1]基础设施提供了类似的机制（JavaSpace [21]）来匹配客户端请求和服务。Klaim编程范式将进程识别为计算的主要单元，并将网络（即节点的集合）识别为进程活动的协调者。每个节点都有一个地址，称为局部性，并由一个进程组件和一个元组空间组件组成进程分布在节点上，并通过元组空间异步通信。Klaim过程可以执行三种不同的基本操作：访问（可能是远程的）元组空间，发送（可能是远程的）执行过程和创建新节点。特别地，可以以两种不同的方式执行移动性。（异步）迁移原语eval允许进程自主地移动到另一个节点，该节点对传入的移动进程没有控制权。此外，可以通过使用out和in/read原语在通信中交换进程。这是一个同步的移动--1 [7]中介绍了该语言的需求和设计理念;[2]中描述了Klaim3因为接收进程对传入进程的执行有一定的控制权。在本文中，我们介绍了HotKlaim（高阶类型的Klaim），一个变种的Klaim，不提供eval原语，但提供了一种数据，可以体现一个过程，即过程抽象。流程抽象对于局部操作的参数化非常有用为了在HotKlaim中表达流程抽象，需要系统F [10]的全部功能，而2-t是，类似于2[6]，用于对可以在网络上自由移动的全局值进行分类。我们提出了一个简化的HotKlaim版本，其中模式匹配被替换为抽象，只有一个操作从元组空间读取值，这说明了本文的核心思想。然而，在非正式的例子中，我们使用了模式匹配和其他典型的函数式语言结构。本文的其余部分组织如下：第2节介绍了HotKlaim的语法，第3节给出了类型系统，第4节定义了操作语义，第5节给出了类型安全结果（证明被省略），第6节说明了一个简单的例子，移动代码应用程序在HotKlaim。与相关工作的一些比较见第7节。2HotKlaim在本文中，我们将使用以下符号和约定。m; n的范围在自然数的集合N上，并且m2N与它的前代的集合fi2Nji m表示项的序列，je j表示其元素的数量如果1和2是声明的序列，那么1;2表示它们的连接（对于术语的序列也是类似的）;（A）是元素在A中的多重集的集合，且]是多重集并;e 2[x：= e 1]表示e 1替换e 2中的x（模α转换）。HotKlaim是一种基于系统F [10]的内核函数式语言，扩展了2[6]的模态类型和Klaim的原语，用于并发、通信和动态创建新站点。 该语法使用一些辅助语法类别：一个类型变量的集合XT，其范围为X; Y;：;术语变量的集合X，范围为x; y;：;地点的集合L，范围为l; l 1;：;一个集合O =fnil;spa wn;new;input;outputg的l o个运算，范围为O。本地业务需要 类型操作数和项操作数e4类型t 2T：：= X jL j P j t 1！t2j（tij i2m）j2tj 8X： k：t其中 k= g; l全全局类型 g2G：：=Lj（ gij i2 m）j2t条件e2E： ： =xj lj x：t：k：ej e1e2j xx：t：k：ej（eiji2m）j i（e）jX：k：e j e [t] j nil j o [t]（e）其中，jtj=#to且jej=#o>0签名L型鳍上下文;2 Ctx：：= ; j; X：k j; x： t： kFig. 1. 类型和术语的注释。process：nil，spawn（e）新地点：新（e）通信：输入[t]（e 1; e 2），输出[t]（e 1; e 2）#t0和#o将指示o的类型和术语。 本地操作的输入和输出在元组空间上操作，new创建一个新的站点，spawn（本地）激活一个新的执行线程，nil代表终止的进程。HotKlaim的语法如图1所示。自由变量集FV（）的定义是预期的，例如。 FV（x：t：k：e）=FV（t）[（FV（e）f x g）。在HotKlaim中有两种类型（和术语），全局和局部类型（术语），分别由g和l分类。上下文声明了类型变量和术语变量的种类。L是局部的全局型，P是局部的过程型。全局类型不包含P，也不包含声明为局部的自由类型变量。此外，全局项不包含局部操作o，也不包含声明为局部的自由项变量。3类型系统类型系统派生下列形式;`，即是一个格式良好的上下文;`t，即t是格式良好的类型e：t，即： e是t类型的格式良好的项。我们将使用;`J来表示上述任何判断。此外，我们将使用g来指示局部声明的上下文，即。形式X：1和x：t：1的那些已经被去除。最后，我们还将使用导出的判断t;g`gJ来代表;g`J，附加要求是P和局部运算o不在J中使用。511图2中给出了类型规则（在某些规则中，当从上下文中清楚时，前提;`被删除）。大多数规则都是标准的。通过将o视为高阶多态常量，局部操作onil：tnil[P]=Pspa wn：tspa wn[P]=（（）！ P）！（）下一页new：tnew[P]=（L！ P）！L输入：t输入t[P]=8X：g：（L;2X！ P）！P输出：t输出t[P]=8X：g：（L;2X）！（）下一页例如，多态类型8 X：g：（L; 2X！ P）！ P抽象了全局值的类型X（可以从元组空间中读取），并声明输入将局部性（类型L）和延续函数（类型2X！ P）给出一个全局值，得到一个连续过程。因此，输入操作返回延续过程。现在我们可以对图2中的类型规则进行注释。x：t：k：e和xx：t：k：e中 的 绑 定 变 量 可 以 声明为 局部变量或全局变量，取决于k是l还是g。当k=l时，分型规则是标准规则。2t的形成规则要求t是全局类型。2t的引入和排除规则说2t是t的子集（即它分类了由t分类的术语的子集），并且当t2G时2t等于t（即2t和t分类了相同的术语集）。2t的一个关键属性是它的值恰好是类型t的全局值。只有类型2t的值可以与输入和输出操作交换。特别是，不能交换进程。 然而，人们可以ex changeglobal values ofty peCode8X：l：（to[X] j o2O）！ X. 我相信，代码是在本地类型P和O中的本地操作上抽象的过程代码的类型。它的定义类似于[17，18]中给出的一元码的定义。当一个Code类型的全局值被读取时，它可以通过将其应用于本地类型P和本地操作的元组（ojo 2O）来转换为一个进程。引理3.1（代换）下列规则是可容许的（参见[6]）：;g`t;1; X： g;2`J;g`e：t;1; x： t： g;2`J;1;2[X： =t]`J[X： =t];1`t;1;X：l;2`J;1;2[X： =t]`J[X： =t]1.2`J [x：= e];1`e：t;1; x： t： l;2`J1.2`J[ x：= e]GG6Gg1 2g1 2GGG1G;`X新鲜; `tx新鲜;g`tx新鲜;;X： k`;; x： t：l`;; x： t： g`;`t1; `t2;“不！ t 2;ti i2 m; `（tij i2m）;g`t; `2吨;;X： k`t; `8X： k：t;`; `L;`; `P;`l：LL2;`;`x：tx： t： k2;`;`e：（）！ Pe：L！P; `nil： P; `spawn（ e）：（）;`new（ e）： L;g`t;`e：L; e：2t！ P;`input[ t]（ e1; e2）： P;;x： t1： l` e：t2;`（x：t1：l：e）：t1！t2;g`t;e：L; e：2吨; `output[ t]（ e1; e2）：（）;;x： t1： g` e：t2;`（x：t1：g：e）：2t1！t2; e 1：t 1！ t 2^e2：t 1; `e1 e2： t2;; x： t： l`e：t;`xx： t： l：e：t;g; x： t： g`e：t; `xx： t： g：e：2t;'e i：t i i 2 m; `（eij i2 m）：（ tiji2 m）; `e：（ tij i2m）i（e）：tii2 m;g`e：t;`e：2吨; `e： g;`e：2g;`e：2吨;`e：t;; X：k`e：t;`（X： k：e）：8 X：k：t;`e：8 X：l：t 2;第一个;`e[t1]：t2[X： =t1]; `e：8 X： g：t2 ;g`t;`e[t1]：t2[X： =t1]7图二. 类型系统。4操作语义一个HotKlaim网N 2 Net=（L E）是一个多对集（l：e），局部性L（节点名称）和项E（在该节点的权限下运行的进程或该节点的元组空间中的值）。网的动力学由一个转移关系给出=）Net（Net+fer rg），记作N=）N0 或N=）er r，根据过渡关系定义>（SigEAE）+（SigEfer rg），写作;ea>e0 或8值v2V： ： =lj x：t：k：ej（viji2m）j X：k：eRedexes r 2 R：：= x j v 1 v 2jx x：t：k：e ji（v）j v[ t]jo[t]（v） 其中jtj=#to且jvj=#o>0Eval. 上下文E 2 EC：：=[ ] jE e j v E j（v; E; e）ji（E）j E[ t]jo[t]（v;E;e） 其中jtj=#too且jv;ej+ 1=#o图三. 值、兑换和评估上下文。;e> err，描述一个术语与其余术语的潜在相互作用。网。 潜在相互作用的集合A是a 2 A：：=j i（v）@ l j o（v）@ l j s（e）j l：e例如，i（v）@l是从位置l处的元组空间输入值v的能力，而l：e是创建运行进程e的新位置l的（非阻塞）动作。22.我曾与你同行，>在赎回和评估环境（见表3），减少>（签名）R一E）+（ SigR（f err g）对于图4中约简利用签名来检查是否存在节点在网中的名字为l。input[t]（l; v2）的约简对应于早期语义（根据微积分[16]使用的术语遵循Klaim类型系统[8，9]，input执行运行时类型检查，并要求输入值必须是全局的。我们现在可以将转移关系定义为满足以下规则的最小关系：一;r> e一;E[ r]> E[ e];r> err;E[ r]> err最后，在图5中给出了净转换关系=（）。 与Linda-like语言一样，输入删除了一个非确定性选择的匹配值（因为]是可交换的），并且这样的值可以在执行输入操作的进程的相同位置（对于输出也是如此）。引理4.1（基本性质）一个值v2V不可能是E[r]的形式.对于任何e2E，最多有一个E2EC和一个r2R s. t。e E[r]，也就是FV（r）FV（e）。请注意，nil不是一个值，而是不活动的。引理4.2（求值上下文的91 2 121 12x>错误（x：t：k：e）v2>e[x： =v2]否则v1v2>errxx： t： k：e> e[ x：=xx： t： k：e]i（vij i2 m） > viwhen i2 motherwisei（ v）> err（X：k：e）[t]>e[X： =t]否则v[t]>errspawn（ v）s（ v（））>（）;new（ v）l：（ v l）> l提供 l62;input[ t]（ l;v2）i（ v）@ l>v2vwhenl2and;;`gv：t;input[ t]（ v1; v2） > errwhen v162;output[ t]（ l;v）o（ v）@ l>（）当 l2;output[ t]（ v1; v） > errwhen v162见图4。 还原关系。在不相关的时候是（N）[flg;e >e0（N）[flg;e>errN]（l：e）=） N]（l：e0）s（ e1）N]（l：e）=）errl2：e2（N）[flg;e>e2（N）[fl1g;e> e1N]（l：e）=） N]（l：e1）]（l：e2）N]（l1：e）=） N]（l1：e1）]（l2：e2）i（ v）@ l212> eN]（1：e）]（1：v）=）N]（1：e0）]（1：ni1）o（ v）@ l21> eN]（l：e）=）N]（l：e0）]（l：v）10图五、 网络转换关系。 （N）是签名flj9e：（l：e）2Ng。如果;`E[e]：t具有E2EC，则存在t1，使得;`e：t 10;`e0：t1表示0;`E[e0]：t表示任何0E011G5式安全当一个网是格式良好的时候，我们定义类型安全属性。定义5.1网N是良构的，当且仅当，对于每个（l：e）2N，要么（N）;;`e：P，要么e2V，要么（N）;;`e：g，对于某个g2G（即：N中的每一个e是局部过程或全局值），其中（N）是签名f1：e：（1：e）2Ng。下面的引理捕获了2-ty pes的关键性质。引理5.2如果; `v：g，则; g`v：g。证据 通过归纳法对的推导;`v：g2下面的引理表达了>和>的类型安全性。引理5.3（>的安全性）如果; ; `r：t，则;r6>错误0 0; r; r; r> e暗示;; `e：ts（ e2）> e1表示;;`e2： P和;;`e1：tl： e2> e1表示 l62，;l;;`e2： P和;l;;`e1： ti（ v）@ l0 0; r> e隐含l 2，; ; `v：g对于一些g 2 G和; ; `e：to（ v）@ l0 0; r> e隐含l 2，; ; `v：g对于一些g 2 G和; ; `e：t证据 通过案例分析可能的减少2引理5.4（>的安全性）如果;;`e：t，则; e6>错误0 0; e; e; e> e暗示; ; `e：ts（ e2）> e1表示;;`e2： P和;;`e1：tl： e2> e1表示 l62，;l;;`e2： P和;l;;`e1： ti（ v）@ l0 0; e> e蕴涵l 2，; ; `v：g，对于某些g 2 G和; ; `e：to（ v）@ l0 0; e> e蕴涵l 2，; ; `v：g，对于某些g 2 G和; ; `e：t证据如果e是主动的，那么它必须是E[r]的形式根据引理4.2，存在一个t1s. t。 ;;`r：t 1，则可以利用安全性获取>2定理5.5（类型安全）设N是良型网，则12N =6）错误13N=）N0这意味着N0 是we ll-形式的ed和（N）（N0）。证据如果N是活动的，则存在对（l：e）2Ns. t。E是活跃的。 由于N是良构的，则（N）;;`e：P，并且可以利用安全性来>26一个简单的例子：动态新闻收集者在本节中，通过一个简单的例子借用[7] ，我们展示了如何使用HotKlaim编程移动代码应用程序。让我们考虑以下情况。用户U需要关于由项表示的数据片段的附加信息（例如，item可以是一本书的标题，而U想知道它的价格）。U的部分行为取决于此信息。然而，也有一些活动是独立于它的。U可以寻找所需的信息，在数据库中分布在网络上，通过使用一个移动的过程抽象，动态地在节点之间旅行，寻找一个元组，包含信息的项目。我们假设数据库的每个节点都包含一个形式为（item，d）的元组，其中包含所需的信息，或者一个形式为（item，ln）的元组，其中包含关于必须重复搜索的下一个节点的信息。在本节的其余部分，我们将使用Klaim语法来处理模式p：：=x！t：kje j（piji 2m）以及类似ML的函数和局部声明符号此外，出于排版的原因，我们写fg而不是2。给定局部操作的类型（nil的类型为P）：I[P]=VX：g。（L，{X}->P）->P;（* 输入类型 *）O[P]= VX：g.（L，{X}）->（）;（* 输出类型 *）N[P]=（）->P;（*type of delayed nil*）我们将使用以下额外的全局类型：Bool =;Data=...;（*项目和相关信息 *）Key=...;（*授权密钥 *）L=.;（* 位置 *）EnvK[X] =（L，Key->I[X]，Key->O[X]，N[X]）MC = VX：1。 EnvK[X]-> X;（*带键的移动代码*）该示例使用了三个辅助函数：start： {（L，L，Data，Key）} ->P;gatherer： {（L，Data，Key）} -> {MC};execute：（L，Key->Bool，（Key，L）->Bool）-> P;开始是用户U的行为的一部分，其取决于与项目相关联的信息。它14是关于其位置自身、搜索必须开始的位置li（其可以根据搜索关键字项来选择）、搜索关键字项和授权关键字k（以远程执行本地操作）而参数化的过程。start添加一个包含15类型MC的过程抽象收集器（self，item，k）到l i处的元组空间，然后等待本地元组空间处的搜索结果。start（self，l_i：L：g，item：Data：g，k：Key：g）=output [MC]（l_i，gatherer（self，item，k））; input（self，{x！数据}=>. ）的方式gatherer是用于搜索的移动代码它的参数是：必须放置搜索结果的位置res，搜索关键字item和用于检查执行本地操作的权限的授权关键字k由于Gatherer是MC类型的移动代码，因此它是相对于通信操作的定制版本（将密钥作为参数）进行抽象的。gatherer查找两个可选元组中的一个。第一个包含与项目相关联的所需信息（例如价格）;如果找到了，则将搜索结果添加到res处的元组空间，并且过程终止。第二个元组包含必须重复搜索的节点的地址l;如果找到它，则将包含过程抽象收集器（res，item，k）的元组添加到l处的元组空间以在那里搜索。gatherer（res：L：g，item：Data：g，k：Key：g）=fixng：MC：g。Fn X：l fn（self，in'，out'， nil'）：EnvK[X]：g=> in'k（self，（d！Data，item）=> out' k（res，d）;nil'（）|（l！L，项目）=>out' k（l，ng）;nil'（））execute是充当节点监护人的进程它相对于其位置自身被参数化，授权功能安全，其基于授权密钥检查代码是否可以被认为是可靠的（并且因此可以不受约束），并且授权功能允许基于授权密钥和位置检查代码是否可以被允许在该位置处执行通信操作。execute负责处理进程抽象（即，一个只有一个MC类型字段的元组），专门化和实例化抽象，然后执行结果进程。“in”和“out”是移动代码专用的通信操作的定制版本;它们使用安全和允许的两个授权功能。execute （ self ： L ： l ， safe ： Key->Bool ： l ， allow ：（Key，L）->Bool：l）=fixexec：P：l.letfun in'（k：Key）=如果安全k则输入elseFn [X：g] fn（l：L， f：{X}->P）=>ifallow（k，l）then input[X]（l，f）else nil ; funout '（k：Key）=如果安全k则输出elseFn [X：g] fn（l：L， x：{X}）=>ifallow （k ，l ）then output[X] （l ，x）else（）; fun nil'（）=nil16在input（self，mc！{MC}=> spawn（mc[P]（self，in'，out'，nil'））; exec）最后，用于此应用程序的HotKlaim网络可以是（l_U：start（l_U，l_i，item，k））（l_U：execute（l_U，safe_U，allow_U））（l_i：（item，l_1））（l_i：execute（l_i，safe_i，allow_i））（l_1：（item，l_2））（l_1：执行（l_1，safe_1，allow_1））（l_2：（item，data））（l_2：执行（l_2，safe_2，allow_2））期望的信息被假定在L2处，并且每个位置具有其自己的监护者，该监护者是通过用适当的参数实例化EXECUTE而获得的。7相关工作与我们更接近的编程范式是[23，24，15]中的那些。在[23，24]中，一种名为D的过程语言被认为是由按值调用演算和-演算的集成以及用于过程分布和远程过程创建的原语产生的。与HotKlaim不同的是，通信是基于通道的，过程不能明确地引用位置（实际上，这些是匿名的）。D允许传输相对于资源（即通道）名称参数化的进程抽象。更具体地说，在[23]中，D的类型系统被定义为确保在任何一个时间，所有打算在给定信道上执行输入的进程都位于同一位置。为此目的，只要一个值的输出不违反通道的局部性，它就被认为是可发送的。虽然类型系统有不同的从HotKlaim的观点来看，可发送的值和类型扮演着与我们的全局值和类型类似的角色。在[24]中，定义了一个用于D的新粒度类型系统，该系统允许控制本地资源上传输的过程抽象的效果（即，渠道）。与HotKlaim不同的是，进程被分配了新粒度的类型，这些类型与接口一样，记录了进程访问的资源以及相应的能力，而进程抽象被分配了依赖的功能类型，这些功能类型从通道名称和类型中抽象出来。虽然流程抽象没有像HotKlaim那样的多态类型，但通道名可能会出现，并在术语和类型中绑定，因此在某种意义上，扮演类型变量的角色。在[15]中，提出了一种名为Conned-的高阶函数语言，它通过允许不同局部的表达式通过通道进行通信来支持分布式计算。在Conned-中，代码的作者可以将区域（即子系统）分配给值，以限制值可以自由移动的系统部分。然后，定义一个类型系统，保证每个值只能在相应的区域内漫游。与HotKlaim不同的是，通信是基于信道的，可传输的进程抽象可以根据信道名称进行参数化，17可传输值允许限制值可以自由移动的子系统。致谢我们感谢匿名推荐人提供的有用意见。引用[1] K.阿诺德湾奥苏利什Schei er，J. Waldo，A.沃尔拉斯湾奥沙利文Jinispeci cation。艾迪森·韦斯利1999年[2] L.贝蒂尼河De Nicola，G.费拉里河，巴西-地普利亚人XKlaim中的交互式移 动 代 理 。 在 Proc.of7thInternationalWorkshoponEnablingTechnologies：Infrastructure for Collaborative Enterprises（WET-ICE）'98，pp.110-115，IEEE Computer Society Press，1998。[3] C. Bodei，P.Degano，F.H.R.尼尔森尼尔森对进程进行静态分析，不进行读和写。在FOSSACS'99，LNCS1578，第120 -134页，Springer，1999的Proc.中。[4] L. Cardelli，A.戈登移动环境的类型。在Proc. of the ACM Symposium onPrinciples of Programming Languages，pp.79-92，ACM Press，1999。[5] N. Carriero，D.格勒恩特琳达在上下文。Communications of the ACM，32（4）：444-458，ACM Press，1989.[6] R.戴维斯F.芬宁分阶段计算的模态分析。在第23届年度ACM程序设计语言原理研讨会（POPL'96）上，佛罗里达州圣彼得堡海滩，1996年1月[7] R. De Nicola，G. L.费拉里河，巴西-地普利亚人KLAIM：A Kernel LanguageforAgentsInteractionandMobility ， IEEETransactionsonSoftwareEngineering，24（5）：315-330，IEEE Computer Society，1998.[8] R. De Nicola，G. L.费拉里河，巴西-地普利亚人类型作为访问策略的规范。在安全的互联网编程：分布式和移动对象（J。维泰克角Jensen编 ） ， LNCS State-Of-The-Art-Survey ， LNCS1603 ， Springer ， pp.117-146，1999年。[9] R. De Nicola，G. L.费拉里河，巴西-地普列塞湾文内里访问控制的类型。Theoretical Computers Science ， 240 （ 1 ） ： 215-254 ， Special issue onCoordination，Elsevier Science，July 2000.[10] J-Y吉拉德解释功能和消除超常规算术运算的方法。PhD.巴黎第七大学论文，1972年。[11] D. 格 勒 恩 特 琳 达 的 生 成 通 信 。 ACM Transactions on ProgrammingLanguages and Systems，7（1）：80-112，ACM Press，1985.18[12] N. Heintze，J.G.里克SLAM演算：编程的保密性和完整性。在Proc. of theACM Conf. on Principles of Programming Languages （ POPL ） ， pp.365-377，ACM Press，1998。[13] M. Hennessy，J. Riely.匿名网络中移动代理的类型安全执行。在安全互联网编程：分布式和移动对象的安全问题（J. Vitek，C。Jensen编），LNCS State-Of-The-Art-Survey，LNCS1603，Springer，pp.95-115，1999年。[14] M. Hennessy，J.莱利信息流与异步π演算中的资源访问自动机、语言和程序设计国际学术讨论会论文集，LNCS，Springer，pp.415-427，2000。[15] D.基尔利连接移动功能。第14届IEEE计算机安全基础研讨会论文集，IEEE计算机协会，2001年。[16] R. Milner，J. Parrow，D.沃克移动过程的演算（第一部分和第二部分）。信息与计算，100：1-77，1992。[17] E. Moggi，F.帕伦博Monadic encapsulation of ects：A revised approach.理论计算机科学电子笔记，26，119{136。1999年第三届语义学高阶运算技术国际研讨会[18] E. Moggi，A.萨布里Monadic encapsulation of ects：A revised approach（extended version）. Journal of Functional Programming，即将出版。[19] G. Necula 携 带 验 证 码 ACM Symposium on Principles of ProgrammingLanguages，1997年。[20] J. 里里，M。轩尼诗移动代理开放系统中的信任与部分类型程序设计语言原理的ACM研讨会论文集，第93 - 104页，ACM出版社，1999年。[21] 太阳微系统公司JavaSpace规范。可查阅http://java.sun.com/products/javaspaces，1997年。[22] A.K. 赖特，M。费莱森类型可靠性的句法方法信息与计算，115（1），1994。[23] N.吉田，M。轩尼诗分布式高阶过程中的子类型和局部性。在Proc. ofthe Int. Conf. on Concurrency Theory（CONCUR），LNCS1664，Springer，pp.557-572，1999年。[24] N.吉田，M。轩尼诗将类型转换为进程。CS技术报告02/99，苏塞克斯大学，1999年。可在以下网址获得：http://www.mcs.le.ac.ukwww.example.com/n~yoshida，