SecSpaces数据驱动模型扩展及其可扩展性证明" On SecSpaces数据驱动模型扩展及可扩展性

理论计算机科学电子札记99（2004）31-47www.elsevier.com/locate/entcs在SecSpacesMario Bravetti、Roberto Gorrieri、Roberto Lucchi和Gianluigi ZavattaroDipartimmntoodiScienzedel电子邮件：{bravetti，gorrieri，lucchi，zavattar}@ cs.unibo.it摘要SecSpaces是一个数据驱动的协调模型，它支持基于元组的协调空间，并扩展了用于控制和验证对条目的访问的机制这是利用空间内部的（对称和非对称）抽象分区的概念来实现的。在本文中，我们考虑SecSpaces的局限性之一：它不适合支持原子访问一次多个分区。为了解决这个限制，我们扩展了SecSpaces模型，引入了一个操作符来组合分区;输出操作可以使用新的操作符来使一个条目在多个分区中可见，数据检索操作可以使用它来原子地访问多个分区。我们正式定义，在一个过程演算，这个概念，我们证明了这个新机制的可扩展性通过例子。1介绍协调语言和模型旨在提供用于开发分布式应用的机制和语言，其中活动组件的内部行为的描述和它们的相互依赖性的描述是不同的和分离的为了支持这种分离，已经开发了通用交互模型;主要方法之一包括将计算与交互信息分离，并将前者定位在活动组件内，将后者定位在所谓的协调基础设施内。当交互信息存储在共享数据空间内时，这种方法称为数据驱动Linda [3]及其方言[8，10，7，6]是这一协调语言家族中最突出的代表。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.00232M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-Linda协调模型基于一个公共存储库，其中交互组件引入和检索协调信息：存储库中的数据是元组（有序的数据序列），并且使用模式匹配机制检索愿意收集元组的进程如果存储库中的元组具有所请求的字段数，并且至少在指定的字段中包含所请求的数据，则该元组满足模板。本机协调模型不包括对控制数据访问的任何支持。例如，任何能够访问存储库的进程也能够引入、检索和使用存储库本身内部的任何元组。最近的分布式应用，如Web服务，移动Ad Hoc网络（MANN）的应用程序，对等应用程序（P2P），本质上是开放的进程，代理，组件，在设计时是未知的。当Linda协调模型被开发来编程这类应用程序内部的协调时（例如，参见用于Web服务的WSSecSpaces [5]，用于P2P应用程序的MANDIX和PeerSpaces [11]的上下文中的Lime [6]），方便的是用用于控制访问、用于认证数据的生产者/消费者、用于确保信息的保密性等的机制来扩展本地协调模型。在文献中已经提出了一些扩展。Klaim模型[7]（用于代理交互和移动性的内核语言）利用类访问控制策略来管理进程对元组空间的访问。访问权限描述了每个进程可以在每个可用元组空间上执行的操作。在开放系统中，特别是在那些具有高水平的动态性，这些信息的管理可能是一个关键的任务，主要是因为系统应该支持一个快速的，有时不受控制的进化的代理社区。更确切地说，新的代理可以频繁地进入系统，以及旧的代理可以以不受控制的方式快速退出。此外，在某些应用中，具有更细粒度的控制可能是有用的，例如，在元组的层次上，而不是在空间的层次上。例如，我们可能希望确保代理不能读取具有私有内容的元组，但它可以读取所有其他元组。SecOS [9]遵循一种非常不同的方法。访问权限不与代理相关联，但所有控制信息都存储在数据中更准确地说，SecOS支持两种形式的锁，称为对称锁和不对称。前者利用相同的密钥来保护和访问信息，而后者使用一对密钥，一个用于保护，另一个用于保护。M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-33一个访问。这两种锁定技术可以应用于保护元组中的一个字段或整个元组。在第一种情况下，使用的锁被称为字段锁，而在第二种情况下，它们被称为对象锁。最近的一个提案，称为SecSpaces[2]，通过完善其访问控制策略，继续了SecOS发起的方法。更准确地说，SecSpaces细化了对象锁的概念，而字段锁没有建模。然而，这不是一种限制性的方法，因为字段锁可以很容易地在我们的模型中编码。例如，在SecOS中，不可能区分元组的非破坏性读取器和破坏性消费者，也不可能避免元组的读取器精确地重新生成该元组。另一方面，在SecSpaces中，可以将两个不同的访问控制信息与元组相关联，一个用于非破坏性读取，另一个用于破坏性输入操作。此外，当在SecSpaces中访问元组时，读取过程仅接收元组内部的协调信息，而不是访问控制信息;因此，它无法精确地再现该元组。SecSpaces本质上允许将两对信息关联到元组，现在我们称之为条目。每个对（p，k）包含对称访问信息p（称为对称划分）和非对称访问信息k（称为非对称划分）。对于这两种访问信息，都定义了一个默认值，因此进程也可以显式地只设置其中一个或为了让读者访问信息，它必须证明p以及k的知识，访问信息对应于非对称分区k。使用其中两个对（p，k）;第一个被认为是在读者愿意执行非破坏性读取操作的情况下，第二个被认为是破坏性输入操作。在本文中，我们调查，在SecSpaces的上下文中，在生命周期的应用程序的访问控制策略的修改的问题。这在参与者可能变得能够访问新资源的应用中特别有用，因为例如，它们为此付费，或者在应用程序中，进程可以根据相关的信任级别访问共享资源，并且该级别可以根据它们的运行时行为而增加或减少。本机SecSpaces模型并不特别适合支持具有此动态方面的应用程序。例如，如果两个单独的用户组在运行时决定加入一个唯一的组，则需要显式地修改存储在这两个用户组当前使用的条目内的访问控制信息。 另一种解决方案是允许用户利用更有表现力的访问权限，表示原子地访问两个组的数据的意图。另一方面，假设34M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-有必要在运行时将用户从组中排除，因为其信任级别已降低。在这种情况下，排除一个用户意味着它不应该再访问该组用户之间交换的新条目。同样在这种情况下，原生SecSpaces模型需要显式修改存储在组条目中的访问控制信息我们提出的解决方案包括扩展SecSpaces，以便：i）在运行时创建新的对称分区，ii）合并分区。我们可以使用合并操作符合并分区，用“：“表示• 当进程通过使用分区p和pJ的合并（即p：pJ）来执行数据检索操作时，它隐式地访问分区p和pJ;• 当进程通过组合分区P和PJ（即P：PJ）将条目插入到空间中时，该条目将对能够访问P和PJ分区中的一个分区在本文中，我们证明了SecSpaces协调模型的这种简单扩展具有足够的表达能力，可以增加显著的动态水平。例如，为了从使用分区p交换条目的组中排除用户，产生新的分区pJ，仅将pJ的知识分发给保留在组内的用户，并且开始使用：i）新分区pJ来交换新条目，以及ii）组合p：pJ来访问由组产生的所有条目（所有新条目和在组限制之前产生的所有那些条目）是足够的值得注意的是，这些扩展只涉及对称分割而不涉及非对称分割。这是因为这两种分区旨在表示不同类型的信息。对称分区用于限制对条目的访问，而非对称分区用于认证条目的生产者/消费者。为此，非对称分区旨在使用离线机制（诸如标准公钥基础设施PKI）而不是SecSpaces协调模型所提供的机制来产生和分发本文的其余部分结构如下：在第2节中，我们回顾了SecSpaces协调模型，该模型是根据进程计算定义的，在第3节中，我们扩展了进程计算，引入了创建新分区以及合并分区的可能性，在第4节和第5节中，我们描述了一些应用程序，这些应用程序证明了新扩展的可扩展性，以便对几种访问控制策略进行建模，在第6节中，我们报告了一些结论性的评论。M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-35e=dJ2SecSpaces协调模型SecSpaces[2]是一个协 调模型，支持开放 环境中的安全数 据驱动协调。SecSpaces通过引入对存储在协调空间中的条目的访问的某种形式的控制来扩展Linda [3]，例如允许认证/识别条目的生产者或其读取器/消费者。SecSpaces的协调原语是Linda的经典协调原语：out（e），in（t）和rd（t）。输出操作符out（e）在空格中插入一个条目e。Primitivein（t）是阻塞输入操作符：当在空间中找到与模板t匹配的条目e时，将其删除并返回其内容。 读原语rd（t）类似于in（t），但在这种情况下，条目e没有从空间中移除。为了表达对条目的访问权限，SecSpaces通过使用特殊的控制字段（即分区和非对称分区字段）装饰Linda元组来扩展它们。前一个逻辑分区的空间，而后者提供了一种方法来区分写和读/删除每个条目的访问权限。设Mess，由m，n，. . ，是一组无限的消息，分区，由c，ct，. . 是分区和AP分区的集合，范围为k，k，J，k，t，. . 是不对称分区的集合。我们还假设分区（resp. AP部分）包含一个特殊的默认值，比如#（分别为？），用于允许任何代理访问该空间。 假设你说呢？如果k=kj，则KJ=k。条目的访问权限由控制字段表示;为了区分rd和in访问权限，条目有两个控制字段，一个与in操作关联，另一个与rd操作关联。与条目不同，模板只有一个与特定操作不关联的控制字段：它们动态地与代理愿意执行的操作相关联（即，rd或in）。条目的集合Entry，范围为e，eJ，.。. ，定义如下：→[c]rd[cJ]in[k]rd[k]in其中，rec，CJ∈P artin，k，KJ∈APart in，并且数据d→的元组是以下文法的集合d→：：= d|d;d→，d：：= m|C|K.数据字段d可以是消息、分区或非对称分区。36M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-[k]我们定义一个函数，给定一个条目e，返回其元组：→[c]rd[cJ]in→数据，即， 如果e=d[r]rd[rJ]in，则e=d。模板的集合T模板，由t，tJ，. . 定义为如下所示：t=d→t[ct]不当rect∈P art，kt∈Aprt，且d→t是该矩阵的一个矩阵时，d→t：：=dt|d t;d→t，dt：：= d|null.对于条目，模板使用的数据字段也可以设置为一个额外的值（null），表示字段：字段用于匹配所有字段值。定义2.1匹配规则和返回值 设e=d1; d2;. ;d[c]rd[cJ]in是一个条目，t=ddt; dt;. ;dt[ct]是一个模板和op∈n[k]rd[kJ]in1 2m[kt]{rd，in}是一个操作。 设ce和ke为e的控制场，op，我们说e匹配opt，如果以下条件成立：(i) M=n(ii) dti=di或dti=null，1≤i≤n(iii) ce=ct(iv) ke=kt.如果在匹配条目e上执行具有模板t的rd或in操作，则仅返回数据字段（而不返回控制字段），即，返回值为e。条件（i）和（ii）改写了经典的Linda匹配规则，即测试e和t是否具有相同的arity，以及e的每个数据场是否等于t的相应场，或者后者是否被设置为n。条件（iii）测试与操作op相关联的条目的划分域条件（iv）检查模板的非对称分区字段对应于与操作op相关联的条目的非对称分区字段的共同密钥。最后，关于数据检索操作的返回值：它不包括匹配条目的控制字段，而只包括存储在数据字段元组中的数据。以这种方式，可以仅通过执行包含数据元组内的分区或非对称分区值的条目的读取/输入操作来获取新的访问许可分区字段可以被视为一种特殊类型的数据字段，在匹配计算中不接受重复分区字段逻辑上对空间进行分区（每个分区包含具有特定分区的条目M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-37值作为标识分区的分区字段），并且对分区的访问仅限于那些知道分区标识符的进程。事实上，为了在分区上执行操作，进程必须知道标识该特定分区的分区字段。然而，为了允许任何进程通过SecSpaces原语相互交互，定义了每个人都可以使用的分区字段的特殊默认值#。类似地，任何进程已知的默认值也被定义为非对称分区字段（用“？”表示与分区不同的非对称分区字段使得可以简单地通过利用产生或读取/移除条目所需的不同知识来区分条目的写入和读取/移除权限。例如，为了读取具有设置为k的非对称分区场的条目，该过程必须使用k作为模板的非对称分区场，这对于该条目的生产者来说可以是未知值（因为只需要k因此，遵循分区的相同思想，适当地分配这些值，我们可以为进程分配权限，以便在该条目上执行可能操作的子集。3具有组合分区的SecSpaces在本节中，我们提出了一个支持分区动态组合的SecSpaces扩展。更确切地说，我们在分区上引入了一个新的合并运算符（用“：“表示我们将要介绍的语言通过引入分区上的合并操作符和用于生成分区新名称的操作符来扩展[1]。在3.1节中，我们介绍了扩展语言和匹配规则的新定义，而3.2节介绍了相应的语义。3.1语言本节介绍扩展语言。更确切地说，我们首先描述如何使用新的合并运算符扩展分区，然后我们正式化系统配置，该配置由以下组成：利用SecSpaces协调原语的进程和共享元组空间的状态。设CP分段，由p，pJ，. . ，是由以下语法定义的分区的可能组合的集合：p：：= c|p：p。分区的组合可以是分区值或分区的合并：38M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-[k] [kJ][k]我们还将ps：CP artition−→P（Partition）定义为这样一个函数：给定一个分区组合，它返回它所包含的分区集合，其定义如下：1ps（c）={c}，ps（p1：p2）= ps（p1）ps（p2）.对称分区字段中的条目和模板结构发生了变化，现在包含分区组合，而不是分区c∈Partitionp∈CPartitionn. Anentrye=d→[p]rd[pJ]in日在 意味着它是可用的（即它出现）在包含在ps（p）和ps（pJ）中的分区中，用于rd和Inprimitives，reespectively. 在rh和nh上，atempllatet=blogd→blog[pt]means不匹配条目必须在ps（pt）中的至少一个分区中可用。下面是条目和模板之间匹配规则的定义定义3.1具有组合划分的d; d;. ; d.[p]rd[pJ]in是一个条目，t=ddt; dt;. ;dt[pt]是模板1 2 n[k]rd[kJ]in1 2m[kt]而op∈ {rd，in}是一个运算。 设pe是e与op相关联，如果定义2.1的条件（i），（ii）和（iv）以及以下条件成立，则我们说e匹配opt(iii)’条件（iii）当从删除操作访问匹配条目时，它会被出现它的任何分区删除。 这个想法是，一个进程可以利用合并机制，通过执行一个out操作来产生一个必须出现在多个分区中的条目;如果一个进程需要产生一个以上的条目，它必须为它需要的每个条目执行一个out值得注意的是，通过在SecSpaces模型中引入与rd和in对应的非阻塞rdp和inp原语以及事务机制，可以实现相同的机制。在匹配条目可用的情况下，非阻塞数据检索原语具有与相应阻塞原语相同的行为，而在相反的情况下，它们立即返回失败值，指示不存在匹配条目。当进程需要执行访问多个分区的数据检索原语时，比如c和cJ（对泛型数的扩展是直接的），它们可以通过以下方式利用非阻塞原语：1我们假设合并运算符的结合性质成立，即（c：c′）：c′=c：（c′：c′′）。M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-39另一方面，为了产生应该出现在多于一个分区中的条目，可以在条目应该可用的每个分区中引入条目的出现。事务是必要的，因为为了消费那个条目，in操作应该原子地执行从它出现的每个分区中删除匹配条目的存储在TS中的条目被表示为作为进程的并行组成的成员设V为，以x，y，. .是数据变量的集合。 在下面的翼中，我们使用e→x，→y，。 . . ，以定义序列sx1;x2;. . ;xn的数据变量。系统配置，按A、B、. . ，和过程，由P，Q，. . ，定义如下：A，B，. * =系统e条目P过程一|平行作文（v c）限制P，Q，. * =进程0空进程输出e.P.输出rdt（→x）. P读int（→x）. P输入P|P平行合成！P复制（v c）P限制一个系统可以是一个入口、一个进程或入口和进程的并行组合。（v c）A表示分区名c在系统中被绑定A. 一个进程可以是一个终止程序0，一个前缀形式μ.P，一个并行两个程序的组合，一个程序的复制，或者它可以包含一个分区名，其范围仅限于进程。前缀μ可以是以下经典Linda操作之一：i）out e，将条目e写入TS;ii）rdt（→x），给出一个模板t，读取TS中的一个匹配查询e，并将返回值存储在→x中;iii）int（→x），给出一个模板t，在TS中消耗一个匹配查询e，并将返回值存储在→x中。 A过程P|Q是两个进程P的并行组合，Q表现为两个并行运行的进程。递归过程是用复制运算符表示的P，它的意义是无限的40M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-复制P。最后，进程可以有边界名（划分）：（ν c）P表示划分名c在进程P中是边界的，因此它只被P知道。在下文中，我们使用P [d/x]来表示表现为P i的过程，其中x的所有发生都与d相关。我们可以用P[d→f→x]来表示通过在P中替换所有出现的变量而获得的过程，其中，当p[d1;d2;. . ;dn/x1;x2;. . . ;xn]=P[d1/x1][d2/x2]. . . [dn/xn]。→[c]rd[cJ]in如果在（→x）操作中每个ch rd/in都有一个t[k]rd[kJ]，则我们将形成这个系统变量→x和数据元组d→t具有相同的性质。设fn（A）和fv（A）是给定系统A的函数，它们分别返回语法上出现在A中的名称集合和A我们说一个系统是封闭的，如果它没有自由变量。在下文中，我们只考虑闭的和良型的系统;我们用System表示这样的系统的集合3.2语义在本节中，我们通过定义系统上的结构同余并将其映射到描述系统在一步计算后如何约简的约简关系上来表1描述了一种关系（结构一致性），表明系统之间的句法差异，这些系统不影响进程的行为。更确切地说，恒等式（i），自反（ii）和传递（iii）关系成立，系统的并行组合的顺序是不相关的（iv），结合关系成立（v），系统的部分可以用结构等价的其他部分替换（vi），空过程对系统的行为没有影响P对应于P的无限平行合成（viii），（ix），（x）和（Xi）表示作用域定律，最后，（xii）描述了alpha转换（即，选择绑定名称是无关紧要的）。系统上的结构同余被定义为满足规则（i）的最小同余。. ，（xii）.表2包含系统缩减规则。规则（1）、（2）和（3）分别描述了三个前缀运算符in、rd和out更确切地说：（1）表明在（→x）中存在过程。如果在TS中存在匹配模板t的当前可用的n个输入，则P可以执行输入，并且在这种情况下，e从TS中被移除，并且过程s是P[e_t/→x];（2）过程s是如何处理的。如果在TS中存在匹配模板t的当前可用的n个尝试，则P可以执行读取操作，并且在这种情况下，过程是P[e_x/→x]，以及（3）P如何在一个M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-41(i)A A（二）BAA组B组（三）ABCA/CN.9/2004/L.16(iv)一|BB|一(v)（A）|B）、|CA|（B）|C）、(vi)AAJA|BAJ|B(vii)一|0mA（viii）！PP|！P(ix)（ν c）（ν cJ）A（ν cJ）（ν c）A（x）（νc）0 <$0(xi)（v c）（A|B）（ν c）A|B，如果c/∈fn（B）(xii)如果A可以通过α转换变为B，则A→B表1系统的结构等价将条目e的新出现步进到TS中，然后该过程表现为P。规则（4）、（5）和（6）分别描述了并行运行的进程的行为，我们可以在任何时候用另一个结构一致的系统替换一个系统，值得注意的是，表1的规则（Xi）和（xii）以及规则（1）和（2）允许我们实现如最初在π演算[？].4组通信示例本节的目的是描述我们提出的SecSpaces扩展可以用来管理重要任务的场景在文献[1，2]中，我们已经证明了进程间交互的某些安全性质是可以被忽略的。特别是，我们已经表明，它是可能的，以保证数据的保密性，生产者和接收者的身份验证，42M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-（一）e匹配 te|int（→x）. P−→P[e/→x]（二）(3)输出e.P−→e|P（四）AB −→BJ（五）A−→BJe匹配rdte|rdt（→x）. P−→e|P[e/→x]A−→AJ一|B −→AJ|BA −→AJ（六）（ν c）A−→（ν c）AJ表2过渡制度条目的确认和数据可用性。在这里，我们现在回顾一下我们已经在这些论文中介绍过的实现安全组通信的想法，其中只有组的实体可以访问组通信中使用的条目。在这项工作中，我们考虑了一个简单的解决方案，其中组中的实体共享一个秘密分区，比如c（可以被认为是会话分区），用于限制对交换条目的访问：任何通信都是通过使用c作为分区字段的条目和模板来完成的。以这种方式，没有其他进程可以读取、移除或产生用于实现组通信的条目，因为c不是公共值，从而保证了交换数据的隐私。下面是一个安全组通信的例子（为了简单起见，不对称分区字段，假设它们被设置为默认值，省略）：（v c）rd<$null<$[c]（x）.out（<$x<$[c]rd[c]in） | out（d[c]rd[c]in）.一如何以安全的方式分布分区值c的建议（假设非对称分区场被适当地分配（如引言中所解释的）到组的每个进程，在4.1节中描述。虽然管理新实体在组中的插入很容易，因为它可以简单地通过（以安全的方式）将组的秘密分区传输给愿意进入的实体（技术上这是通过范围挤压获得的，参见第3.2节）来完成，但管理从组通信中删除某些实体则更复杂，这是组密钥管理系统的常见功能，因为应该创建新分区并将其分发给组中除了要删除的进程之外的进程。一个更普遍的问题是将对某些条目的访问限制到组中的实体子组。第4.1节解释如何管理M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-431i−1i sn通过利用合并运算符来消除组限制。最后，第4.2节描述了如何组合分区，以便在运行时管理两个（或多个）独立进程组之间的协调。更确切地说，我们打算为那些需要发布某些数据并使其可供多个用户组使用的应用程序提供支持，或者控制不同组之间交换数据的流量4.1群限制令G ={P1，. ..，Ps} ∈G是G中过程的子集.我们在本节中考虑的问题是：i) 为组G和Gp提供安全组通信，以及ii) 允许Gp中的进程（应该被认为是G的特权进程）执行数据检索操作，这些操作可以原子地访问整个组或特权进程可用的条目我们提出的解决方案是定义，除了c，一个新的分区cJ，它是特权进程的共享和私有值，利用它来限制组Gp级别的通信。更正式地说，我们要定义的系统配置如下：（v c）（P| ... | P|......这是什么？|... |......这是什么？|... | P ).语句i）和ii）成立，因为：1）G中的每个进程可以通过使用c作为条目/模板的分区字段来在组中彼此通信，此外，特权进程还可以将通信限制为J J通过插入具有被设置为cJ的分区的条目，例如，out（intd[c]rd[c]in;2)特权进程在一个步骤中可以简单地通过利用合并运算符来访问这两个分区，该合并运算符在模板的分区字段中指示c：cJ，例如rd_null_n[c：cJ]（x）。这个问题的一个特殊例子是从组中删除一些用户：在这种情况下，将分区c与新分区cJ组合允许我们原子地访问新条目以及删除这些用户之前产生的条目下面的例子描述了一种可能的方法来实现cJ到Gp中的进程的安全分发。例4.1给定一个生成新划分cJ的进程P I，我们考虑一组s − i个非对称划分kij，其中j满足j：i +1 ≤ j ≤ s。我们假设对每一个i +1 ≤ j ≤ s，kij仅由过程Pi已知而kij仅由Pj已知。组限制可以通过利用以下分发协议来实现：44M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-[k][k]我[k][k]我1i−1i snJ（vc）（P| ... |P|PJ|......这是什么？|......这是什么？|... | P )哪里PJ=（ν cJ）out（cJ[c]rd[c]in）.out（cJ[c]rd[c]in）...我.out（cJ[c]rd[c]in是rd处于PJ=innull[c][ki（i+1）]rd[ki（i+1）]in）.P1，以及（x）.Pj，其中i+1≤j≤s.[ki（i+2）]rd[ki（i+2）]inj[kij]PJ创建一个新的分区cJ，然后将其分发给Gp中的进程，达到构型（ν c）（P1| ... | Pi−1 | (ν cJ)(Pi | ... |......这是什么？|... | Pn).应当清楚，伊季路伊日因 只能由PJ产生，对于任意i +1≤j≤ s，只有Pj可以访问该条目。4.2小组协调在本节中，我们将讨论如何利用合并操作符来支持不同组之间的协调，例如将数据分发给多个组。我们遵循的想法是，一个进程（一个新的进程或从组中选出的进程）扮演协调者的角色;它知道与每个组相关联的分区，并且通过合并所有（或部分）组分区，可以插入所有（或部分）组都可以访问的条目，以及读取和删除所有组生成的所有条目。我们考虑的情况下，两个群体必须协调，扩展到任意数量的群体是直截了当的。令G ={P1，. ，Pn}和GJ={PJ，. ，PJ}是利用共享的进程的两组进程（以及1kJ组专用）分区c和c组，分别。来互相交流我们在细节中描述了协调器向组提供插入数据的方式的情况，该数据应该在两个组（即分区c和cJ）中都是可访问的。为了避免直接访问其他群的划分，我们假设每个群都有一个标识符，并且知道其他群的群标识符;我们分别对群G和GJ使用g和gJ当组的进程（例如，G）愿意产生在其他组中应该可用的条目，则它在其空间中产生条目，该条目在数据字段的元组中包含条目应该可用的组的标识符和它愿意发布的数据d（例如，out（gJg，d[c]rd[c]rd））。协调器删除这些条目，记录请求M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-45然后发布条目。 协调器流程定义如下：！（in_null;null_n[c：cJ]（x;x）.LogReq（x，x）.out（_nx_n[P（x1）]rd[P（x1）]in）），1 2 1 2 2其中LogReq注册请求，P（grp）返回合并grp中标识的分区的表达式（例如，P（gJg）=c：cJ）。协调器的角色还可以通过管理访问权限来扩展，即，检查一个组是否可以写入指定的组。值得注意的是，如果我们必须管理两个分区的组合而不是c和cJ，则可以使用相同的方法，在这种情况下，我们分发已经在多个分区中可用的信息。5具有多级安全性在本节中，通过实现一个多级系统来证明所提出的扩展的可扩展性和可表达性，在该多级系统中，可以访问某个级别l的进程也可以访问比l更高的每个级别。为了尽可能地通用，我们考虑一个层次树描述系统的安全级别，用节点表示，以及它们的（部分）排序关系，即：每个节点（级别）高于每个孩子。我们打算在SecSpaces中编码的模型允许，给定一个级别l，i）在指定的级别l上生成一个新的数据，ii）执行一个数据检索操作，可以访问级别l或高于l的级别上的数据。换句话说，在该系统中，由访问级别l的进程产生的数据在l中以及在l高于lJ的所有级别lJ中可用。以这种方式，分层树的每个叶可以访问路径leaf-root中的每个级别，并且可以被认为是具有最大特权的级别在路上的人，为了对系统进行编码，我们分两步进行：i）我们引入一种新的算子，用于对将被用来编码系统的分区进行子分区，以及ii）我们通过利用所提出的合并算子来编码所引入的算子。为了引入子划分算子，我们扩展了划分的语法：p：：= c|p：p|p→ p。给定一个划分p1，子划分算子允许我们引入新的划分（p1→p，对于任何p），这些新的划分通过定义是p1的子划分。一般来说，一个分区是另一个分区的子分区，如果后者的名称p1→p2→p3是p1→p2以及p1的子划分）。我们遵循的想法是，分区表示46M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-层次树和子分区运算符允许我们表达节点和祖先之间的关系：每个分区，比如说P1，是P1的每个子分区的祖先，例如P1→P表示P1是P1→P的祖先（例如，p→c有父p），则p1有比p1→p高的能级。函数ps的定义被扩展为以下情况：ps（p1→ c）={p1→ c}·ps（p1）.通过使用合并和子分区操作符来组合分区，匹配规则（参见定义3.1）允许匹配出现在模板指定的分区中或每个分区中具有更高级别的条目。为了对系统进行编码，我们假设安全级别标识符（即，也通过→运算符表示层次级别关系的分区）的知识已经被正确地分配给过程;该阶段可以通过利用非对称分区字段来完成（更多细节请参见[2]）。多级系统提供以下原语，其编码为：• out（d→，p）=out（d→n[p]rd[p]in），在s中，数据集d→in第i个evelp，• rd（d→t，p）=rdd→t[p]（→x），其通过使用访问级别p来读取在具有d→t的ching处的数据m，以及• in（d→t，p）=in_d→t_p[p]（→x），其通过使用访问级别p来消耗具有d→t的数据集。应该清楚的是，如此定义的系统对上述多级系统进行编码。例如，可以访问级别p1→p的进程可以读取/消耗在ps（p1→p）中的级别处可用的任何数据。最后，在这里，我们展示了如何通过只使用合并运算符来编码子分区运算符。唯一的变化是关于SecSpaces原语使用的分区字段值，即：i）在out原语中，我们保持相同的分区p;在它包含子分区操作符的情况下，它将被视为分区名称的一部分，以及ii）在rd/in原语中，p被编码为合并操作符对每个分区的应用，该分区由ps（p）的扩展定义确定。就在这一段。 例如，ou t（d→，（c1：c 2）→ c 3）是一个具有hd→h d[（c1：c2）→c3]rd[（c1：c 2）→ c 3 ] n的编码，它在一个部分中产生一个尝试，该部分是通过使用dd（d→t，（c1：c 2）→ c 3）→ c 4），具有rd d → hd [（（c1：c 2）→c 3）→c4）：（（c1：c2）→c3）：（c1：c2）]（→x）的编码而产生的。值得注意的是，编码所需的knwl边缘的ps），因此我们不需要修改过程的知识。M. Bravetti et al. / Electronic Notes in Theoretical Computer Science 99（2004）31-476结论和今后的工作本文介绍了SecSpaces的一个扩展，以便为诸如组通信管理或具有不同访问权限级别的进程之间的交互等问题提供解决方案。所提出的解决方案的可扩展性已被证明，通过描述几个例子，其中它是必要的运行时管理的条目的范围的支持。最后，作为未来的工作，我们打算将SecSpaces的扩展版本与一些多级系统进行比较，例如[4]，这是一个支持单向流的多级系统，与第5节中描述的模型有一些相似之处。引用[1] 马里奥·布拉韦蒂，罗伯托·戈列里，罗伯托·卢基。安全空间中安全性检验的形式化方法。在Riccardo Focardi和Gianluigi Zavattaro，编辑，理论计算机科学电子笔记，第85卷。Elsevier，2003年。[2] Nadia Busi，Roberto Gorrieri，Roberto Lucchi，and Gianluigi Zavattaro. Secspaces：一个数据驱动的协调模型，用于对不可信代理开放的环境。在Antonio Brogi和Jean-Marie Jacquet的编辑中，理论计算机科学电子笔记，第68卷。Elsevier，2003年。[3] D. 格 勒 恩 特 琳 达 的 生 成 通 信 。 ACM Transactions on Programming Languages andSystems，7（1）：80[4] 明海Kang，Andrew P. Moore，and Ira S.莫斯科维茨 NRL泵的设计和保证策略。IEEEHigh-Assuruance Systems Engineering Workshop（HASE97）.[5] 罗伯托·卢基和吉安路易吉·扎瓦塔罗。WSSecSpaces：一个用于Web服务应用程序的安全数据驱动协调服务。ACM Symposium on Applied Computing（SACACM Press，2004.[6] A. 墨菲湾，澳-地皮科和G.-C. 罗曼用于物理和逻辑移动性的中间件在第21届分布式计算系统国际会议，第524-533页[7] R. De Nicola，G. Ferrari和R.普利亚人KLAIM：一种用于Agent交互和移动的核心语言。IEEE软件工程学报，24（5）：315-330，1998年5月。专刊：移动性和网络感知计算。[8] 孙微系统，Inc.JavaSpacesTM服务规范，2002年。http://www.sun.com/jini/specs/的网站。[9] JanVitek，Ciar'anBryce，andManuelOriol. 与Sec ureSpaces共同制定预防措施。计算机程序设计科学，46：163[10] P. Wycko，S.W. McLaughry和D.A. Ford。TSpaces。IBM System Journal，1998年8月。[11] 吉安路易吉·扎瓦塔罗PeerSpaces：Data-driven Coordination in Peer-t