面向状态的CCS：非干涉类型系统及安全性属性的研究

理论计算机科学电子笔记194（2007）39-60www.elsevier.com/locate/entcs面向状态的CCSIlaria Castellani Ilaria Castellani1，2INRIA索菲亚安提波利斯2004路des Lucioles，BP 93，06902 Sophia Antipolis Cedex，法国摘要我们解决的问题，打字不干涉（NI）在演算CCS，在这样一种方式，米尔纳的翻译成CCS的标准并行命令式语言既保留了现有的NI属性和相关的类型系统。最近，Focardi，Rossi和Sabelfeld已经表明，米尔纳的翻译的一个变体，仅限于语言的顺序片段，映射一个时间敏感的NI属性的持久Bisimulation-based非演绎成分（PBNDC）的CCS。然而，由于CCS没有配备类型系统，因此无法解决翻译是否保留类型的问题 我们扩展Focardi，罗西和Sabelfeld的结果表明，一个稍微简单的米尔纳的翻译的变体保留了时间不敏感的NI属性的完整的并行语言，通过将其再次映射到PBNDC。作为一个副产品，我们正式的民间传说的结果，即米尔纳的翻译保留了行为上 我们提出了一个简单的类型系统，确保CCS上的PBNDC，现有的类型系统的π演算的启发。不幸的是，这种类型系统的限制太多，无法获得预期的类型保留结果。我们提出了一个解决方案来克服这个问题。关键词：非干扰，类型系统，并行命令式语言，进程演算，互模拟。1介绍近年来，随着移动设备和游牧计算的普及，安全信息流问题引起了人们极大的兴趣。这个问题已经在编程语言（参见[26]的评论）和进程演算[24，8，13，21，11，14，12，5，17，10]中进行了深入的研究。当提到编程语言时，我们将谈到“基于语言的安全性”，“基于语言的方法关注的是秘密数据不会被程序泄露，也就是说，机密的安全属性。这个属性通常通过不干涉（NI）的概念来形式化，说明程序的秘密输入不应该影响它们的公共输出，因为这可以允许-至少在原则上-公共用户重建秘密信息。1 工作部分由ANR SETI-06-010赠款支持。2电子邮件：Ilaria. sophia.inria.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.09.01240I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39另一方面，基于过程的方法关注的是过程的秘密行动，而不是公开观察的。虽然与基于语言的方法有明显的相似之处--在这两种情况下，安全级别都被分配给信息载体，分别是变量和渠道--但基于过程的方法并不依赖于完全相同的简单直觉。实际上，观察者可以通过与进程通信来收集什么信息，这方面有几种选择。这一点得到了认可。在为进程演算提出的各种NI属性中，主要基于迹等价、测试或互模拟（参见[8]的评论）。一般来说，这些属性不能清楚地区分数据流和控制流，它们在进程演算中紧密交织在一起。让我们考虑一些例子。在具有值传递的微积分CCS [18]中，输入过程a（x）.P在通道a上接收值v，然后变成P{v/x}。对称地，一个输出进程a在通道a上发出表达式e的值，然后变成P。 典型的不安全数据流如下所示，其中下标表示通道的安全级别（h表示“高”或“秘密”，l表示“低”或“公共”）：得到h（x）。 把lx这里，在高信道上接收的值在低信道上被重传。由于x的值可以从一些高外部来源获得，因此该过程被认为是不安全的。然而，也有其他情况下，低输出操作不携带数据，或携带并非源自高源的数据，如：geth（x）. alch. 把lvgeth（x）. putlv当实际情况是，与传统的纸张和磁盘一起使用的网络具有一致的价值时。尽管这些过程不直接将数据从高级别传输到低级别，但它们可以用于实现间接的不安全流，如以下过程中所示（其中x是布尔值，并且通道ch和dh上的动作受到限制，因此不可观察）：P=（（得到h（x）。if x then chelse dh）|（ch. 把l0+ dh。putl <$1<$））\{ch，dh}上述例子提出了一个对CCS实施不干扰的简单标准，即高动作之后不应有低动作。诚然，这要求非常强烈。然而，它可以作为，并且确实已经被用作定义进程演算的安全类型系统在基于语言的方法中，理论结果常常导致用于验证安全属性的工具的设计和安全实现的开发。到目前为止，大多数语言都配备了类型系统或其他工具来强制执行所需的安全属性[19，20，23，22]。相比之下，基于过程的方法仍然停留在理论层面。Hennessy等人在[11，12]和Honda等人在[13，14]中提出了πPottier在[21]中给出了π演算的一个纯安全型系统。最近，Crafa和Rossi [10]和Kobayashi [17]研究了π演算的不同安全类型系统（最后一项工作也提供了类型推断算法）。在[5]中，已经提出了CCS变体的其他静态验证方法我们解决了统一基于语言和基于过程的ap的问题，I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3941方法，通过将它们的安全概念和相关的类型系统联系起来。 在这个方向上的第一步是由Honda，Vasconcelos和Yoshida在[13]中采取的，其中并行命令语言嵌入到类型化π演算中。Honda和Yoshida在[14]中进行了这项工作，其中考虑了更强大的语言，包括命令式和函数式在[9]中，Focardi，Rossi和Sabelfeld表明，Milner将顺序命令式语言翻译成CCS的变体基于持久性双模拟的非演绎组合物（PBNDC），介绍[7]由Focardi和Rossi引入。但是，由于中央结算系统没有配备证券类型系统，因此无法解决类型保存问题以[9]为出发点，我们通过证明Milner翻译的一个更简单的变体在并行命令式语言上保留了时间不敏感的NI属性，将其再次映射到PBNDC来扩展其结果作为一个副产品，我们表明，翻译保留了程序的行为等价。我们还提出了一个确保PBNDC的类型系统，灵感来自[21，11，12]的π演算类型系统。不幸的是，这种类型系统的限制太多，因为它代表了源语言的任何已知类型系统。 然而，它可以作为基础来派生一个合适的类型系统，这是简要概述在这里。论文的其余部分组织如下。在第2节中，我们回顾了CCS的BNDC 和PBNDC在第3节中，我们介绍了并行命令式语言和它的时间不敏感的NI属性，然后我们提出了一个适应米尔纳的翻译这种语言到CCS，并表明它保留了我们的NI属性。最后，我们讨论了类型保持。在《易经》中，有许多典籍记载，其中有《易经》的记载。2一种简单的CCS在本节中，我们将为CCS提供一个安全类型系统，其灵感来自Pottier [21]和Hennessy和Riely [11，12]为π我们证明了这类系统保证了Focardi和Rossi在[7]中提出的基于持久双模拟的非演绎合成（PBNDC）2.1过程演算CCS我们选择的进程演算是具有值传递和保护和的CCS。我们先回顾一下主要的定义。我们假设一个可数的通道或名称N的集合，由a，b，c组成，输入和输出采用通常的符号约定。类似地，设V ar是与N不相交的变量的可数集合，并且其范围为x，y，z，并且V al是数据值的集合，其范围为v，vJ。我们定义Exp，范围为e，eJ，是使用标准的全运算从值和变量构建的布尔和算术表达式的集合。最后，我们让val：Exp→Val是表达式的求值函数，满足val（v）=vforanyvalu e v。 我们将使用这个非整数→x（resp）。→vorr→e）todentence1，.，xn nn（resp.一个序列是1，...，vnore1，.，en）。42I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39ΣΣ进程前缀的语法，范围为π，πJ，由下式给出π：：= a（x） | 一个人 | 一|一a和a形式的简单前缀将在示例中使用，但从我们的技术处理中省略，因为它们是a（x）和a（x）的简单情况。为了定义递归过程，我们假设一个可数集I={A，B，. . }的参数过程标识符，其中每一个都应该有一个固定的arity。然后，我们定义参数项的集合，范围为T，TJ，如下所示：T：：=A|（recA（→x）.其中P是CCS过程，定义如下。Aterm（recA（→x）. P）是满足以下条件的最佳选择：（1）所有（2）f→x的取值等于A的取值;（3）P的取值都等于0→x;（4）A的取值不等于P的取值;(5)递归是受保护的：所有出现在P中的A都出现在前缀之下。 由P，Q，R覆盖的进程集合Pr由以下语法给出：P，Q：：=i∈Iπi.Pi|（P|Q）|（νa）P|T（→e）其中I是索引集。 我们用0作为空和Pi. 因此，我们可以得到一个统一的sum i∈{1}πi.Pitoπ1.P1andabinry总和i∈{1，2}πi.Pito（π1.P1+π2.P2）. 在一 个 实例中，sA（→e）或r（recA（→x）。 P）（→e），→e的长度等于A的长度。 在所有的y中，f→a=1， . . ，一个，当i/=j时，m（νa1）·· ·（νan）P是一个倒推函数d到o（ν→a）P。IfK={a1， . . ，an}，我们将（ν→α）P简单地定义为（νK）P，或者使用原始CCS符号P\K，特别是在示例中。自由变量的集合（分别为自由进程标识符）将由fv（P）（分别）表示。fid （P ））。 我们用P {v/x}来替换变量x ， 用 P 中 的 v 来替换。 同 样 ，f→x=1， . . ，xn=1， . . 因此，P{→v/→x}不能确定P中的每个变量的子节点。 F在所有y中，P{T/A}表示用参数项T代替P中的标识符A。P−α→PJ的简单变换给出了预处理的电磁场。转换被标记为动作α，β，γ，它们是集合的元素：Actd=ef {av：a∈N，v∈Val} <${a<$v：a∈N，v∈Val}<${τ}前缀的主语定义为subj（a（x））= subj（ae）=a，动作的主语定义为y subj（a v）=subj（av）=aanddsubj（τ）=τ。该组件可以通过写入av= a <$v和da<$v=av来执行输入和输出操作。CCS工艺的操作规则见图1。一个不确定的总数i∈Iπi.Pi执行一个被加数πi.Pi，同时丢弃他人 a（x）的值。Pi在通道a上接收一个值v，然后替换它对于Pi中的x。一个被加数一个加数。Pi在通道a上发出表达式e的值，然后变成Pi。平行组合P|Q交错执行P和Q，可能使它们在互补动作上同步，以产生τ-动作。限制（νb）P的行为类似于P，其中通道b上的动作被禁止。I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39431i∈iiI−→⇒=P2−→P=Pααατ（SUM-OP）π。P−a→vPi{v/x}，若πi=a（x）且v∈V al（SUM-OP）πi.PiavPi，如果πi=ae且val（e）=v（PAR-OP1）P−α→PJP|Q−α→PJ|Q（执行部分第2段）Q−α→QJP|Q−α→P|QJ（执行部分第3段）−→PJ−→QJ（RES-OP）−→PJb/=subj（α）P|Q−τ→PJ|QJ（νb）P−α→（νb）PJ（REC-OP）P{→v/→x}{（recA（→x）. P）/ A}−α→PJ →v=val（→e）（recA（→x）. P）（→e）α PJ图1.一、CCS过程的操作语义2.2CCS的安全属性我们回顾了CCS的两个安全属性：由Focardi和Gorrieri [8]引入并由Focardi和Rossi在[7]中重新制定的基于双模拟的非演绎组合（BNDC），以及[7]中提出的基于持久双模拟的非演绎组合（PBNDC），作为BNDC的加强，更适合处理动态上下文。我们首先回顾弱互模拟的定义。我们采用通常的符号约定：• 对任意α∈Act，设P=α• 对于ayα∈Act，令tP=αtPJdefPJdefτ∗ατ−→−→−→⎨⎧αJτPJ=P−→ 如果α=τ，定义2.1[弱互模拟]对称关系S（Pr× Pr）是弱互模拟互模拟，如果PSQ意味着，对于任何α∈Act：若P−α→PJ则存在QJαˆ这样，Q=QJ和PJSQJ。P和Q是弱双相似的，P<$Q，如果对某个弱互模拟S，PSQ。为了建立BNDC的场景，我们需要更多的定义。定义2.2[高和低信道]信道的集合N被划分为高（秘密）信道H的子集和低（公开）信道L的子集。输入和输出动作根据其支持通道的水平被定义为高或低。没有给τ-action提供安全级别。PPQ⇒i∈I如果α44I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39synsyn−→ˆ−→α定义2.3[语法上的高进程w.r.t. H]相对于H的语法上高的进程的集合，记为PrH，是在H中只包含通道的进程。[8]的基于双模拟的非演绎合成（BNDC）的性质，在Focardi和Rossi [7]给出的重新表述中，现在定义如下：定义2.4[BNDCH]设P∈Pr，H ∈ N为高通道的集合。则P关于H是安全的，P∈BNDCH，如果对每个过程P∈PrH，（νH）（P|P.当没有歧义时，我们简单地写BNDC而不是BNDCH。让我们指出两个典型的不安全来源：(i) 当P中的高位名后面跟着低位名时，可能会出现不安全性，因为在这种情况下，（νH）P的执行可能会阻塞高位名，使低位名不可达，而在（ν H）（P）中总是可以找到一个高位进程，使低位名可达|）。例如，设P=ah。贝湖 Choosin g n=ah，onobtains（νH）（P|P.(ii) 当高名称与低名称冲突时，也可能出现不安全性，asinP=ah+bl。 He eagain，takin gn=ahone gets（νH）（P|n）/n（νH）P，因为第一个过程可以做一个无声的移动τ， 导致一个状态等价物，0，第二个进程无法匹配。另一方面，注意Q=ah。 bl+bl是一个可解的问题，因为在这种情况下，在（νH）（Q）中，|可以用（ν H）Q中的无动来模拟。在[7]中，Focardi和Rossi提出了一个比BNDC更鲁棒的属性，他们称之为基于持久双模拟的非演绎组合（PBNDC）。为了定义PBNDC，需要一个更宽松的互模拟概念，∼α在一个新的转移关系= αH上，对于任何α∈Act，定义为：∼αP=100000Pdef=P=PJαˆ或PτPJ如果subj（α）∈ HP=定义2.5[弱互模拟高达高]对称关系S 如果P S Q，则P（Pr×Pr）是弱互模拟直到高对于任何α∈Act，意味着：若P−α→PJ则存在QJ∼α使得Q=HQJ和PJS QJ。两个过程P，Q是弱互相似的，记为P<$HQ，如果PSQ是弱互相似的，直到高S。定义2.6[PBNDCH]设P∈Pr. 然后，P被认为是持续安全的对于H，P∈PBNDCH，如果P<$H（νH）P.∼αJ⎨⎧I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3945在PBNDC的定义中使用了过渡关系=H，46I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39ΣP的移动被（νH）P的τ-移动序列（可能是空的）匹配。在[7]中表明PBNDC比BNDC更强，并且对于P需要PBNDC等于对于P的所有可达状态需要BNDC。BNDC和PBNDC以同样的方式处理上述所有例子。安全但不持久安全的过程的示例可以在[7，6]中找到。2.3PBNDC的安全类型系统在本节中，我们将介绍CCS的安全类型系统，并证明它确保PBNDC属性。这种类型系统的灵感来自于Pottier [21]和Hennessy等人先前提出的π-演算。[11、12]。安全级别由δ、θ、σ组成，通常定义为一个格（T，≤），其中顺序关系≤代表“比... 在这里，我们假设格是简单的{l，h}，其中l≤h，以匹配通道集合划分为L和H。类型环境Γ是从通道到安全级别的映射，以及从进程标识符到安全级别的部分映射。这个映射通过让Γ（π）= Γ（subj（π））扩展到前缀和可见动作，并且对于任何ατ，Γ（α）= Γ（subj（α））。过程的类型判断有形式为Γ <$σP。直观地说，Γ <$σP意味着在类型环境Γ中，σ是在P.打字规则如下：（SUM）πi∈I：Γ（πi）=σΓ<$σPiΓ <$σ <$i ∈Iπi.（PAR）σPσQΓ π σP|Q（RES）Γ，b：θ<$σPΓσ（νb）P（SUB）ΓσP σJ≤σΓσJP（RE c1）（RE c2）Γ（A）=σΓσA（→e）Γ，A：σ<$σPr∈σ（recA（→x）.P）（→e）让我们简单地讨论一下规则（SUM），这是一个不太标准的规则。这条规则对进程i∈Iπi.Pi施加了一个强约束，即所有前缀πi都有相同的安全级别σ，并且Pi有自己的类型σ。事实上，由于每个判断都可以通过使用subtypig来得到，因此对于每个σi，都必须对所有的判断都进行rg化，使得σ≤σi。 不，不。 blanddah+bla re notypablee. 然而，它应该是最好的，因为它有一个安全的保护区。 bl+bl也不是可打印的。因此，规则（SUM）比我们希望的要严格 为了让我们的关系更好。bl+bltypable，我们通过以下方式计算出一个通用的应I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3947用程序规则（SUM）48I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39规则（SUM-LAX），它允许一个prefixπi的级别高于l，只要它的连续过程Pi与原始的和过程不可区分：<$i∈I：Γ<$σPi< $（Γ（πi）=σ<$（Γ（πi）>σ<$Pi <$H<$i∈Iπi.Pi））（SUM-LAX）Γ <$σ <$i ∈Iπi.然而，请注意，规则（SUM-LAX）使用语义等价性H，并且因此不是完全静态的。为了避免在我们的类型系统中引入这样的语义检查，我们将暂时坚持更经典的规则（SUM）。我们现在着手为PBNDC建立这种类型系统的可靠性。我们在这里陈述最相关的结果，请读者参考[6]以获得更多细节。定理2.7（主体归约）对于nyP∈Pr，若Γ <$σP且P−α→Pj，则nΓ <$σPJ.引理2.8（确认）Let P∈Prand rrdrσP. IfP−α→PJandατ则Γ（α）≥ σ。可靠性证明的关键是可类型程序的以下属性：引理2.9（在L∈ P∈Pr，Γ∈σP和H={a∈N：Γ（a）=h}. 如果P−α→PJ且Γ（α）=h，则P.J.推论2.10（可类型化程序的可组合设P，Q，R∈Pr，Γ是一个型环境，使得Γ<$σP， Γ<$σQ，则若P <$HQ，则P |R·H·Q |R.请注意，在任意程序上，并行组合并不保留Pini，正如这个例子所示，其中PiPiniQi（i=1，2，但P1|P2/P2/P1|第二个问题：P1=ahQ1=0P2=Q2=bl+ah这是一个简单的方法，|P2/P2/P1|Q2，sic e P1|P2可为τ-作用量，|Q2不能匹配。请注意，P2是不可类型化的.事实上，P2是不安全的。如图所示，PBNDC本身的性质是组成性的。使用上面的结果，我们可以证明可类型性意味着PBNDC：定理2.11（合理性）若P ∈Pr且Γ <$σP，则P <$H（νH）P，其中H ={a ∈ N：Γ（a）= h}.目前，我们关于CCS的安全性和类型的讨论到此结束3并行命令式程序到CCS的我们在这里关注Smith和Volpano在[30]中研究的并行命令语言，我们称之为I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3949PARIMP。已经为这种语言提出了几个NI属性和相关的类型系统[27，1，29，4]，受到开创性的启发，50I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39Volpano，Smith等人的工作[32，30，31]。有一个众所周知的PARIMP到CCS的翻译，由Milner在[18]中提出。在[9]中，Focardi，Rossi和Sabelfeld表明，这种翻译的变体通过将其映射到PBNDC来保留PARIMP序列片段的我们将在这里关注完整的语言PARIMP，以及这种语言的时间不敏感的NI属性。我们将证明，这NI财产是由米尔纳的翻译一个合适的变种保存。作为一个副产品，我们将表明，我们的翻译也保留了程序的行为等价。3.1命令式语言PARIMP在本节中，我们回顾了PARIMP语言的语法和语义，并受[4]的启发，为它定义了一个时间不敏感的NI属性我们假设一个可数的变量集合，其范围为X，Y，Z，一个值集合，其范围为V，VJ，以及一个表达式集合，其范围为E，EJ。形式上，表达式是使用全函数F，G，. ，我们假设其与函数f，g，. 用于构建CCS表达式：E：：= F（X1，.，Xn）程序或命令的集合C，由C，D组成，定义为：C、D：：=零| X：=E| C; D| （如果E，则C，否则D）|（whileEdoC）| （C）该语言的操作语义是根据配置之间的转换给出的，其中C，CJ是程序，s，sJ是状态或存储器，即从变量的有限子集到值的映射。这些映射以一种显而易见的方式扩展到表达式，表达式的计算被假定为终止的和原子的。我们用符号s[V /X]表示内存更新，用<$→表示→的自反闭包，用→表示它的自反和传递闭包。配置的操作规则如图2所示。 规则（第2条）和（PAR R-OP 2）被引入，如在[3]中，以允许每个终止配置形式为nil，s。如果fv（C）是无约束的，则配置<$C，s<$是良构的。通过检查规则，很容易看出，<$C，s<$$> → <$CJ，sJ<$$>意味着fv（CJ）<$fv（C）和dom（sJ）= dom（s）。因此，格式良好是通过执行来保存的。对于CCS，我们假设变量被划分为一组低变量L和一组高变量H。在示例中，我们将分别使用下标L和H表示属于集合L和H的变量。我们现在可以引入低相等和低互模拟的概念。定义3.1[L-相等]两个存储器s和t是L-相等的，记为s=Lt，如果dom（s）=dom（t）和（X∈dom（s）<$L<$s（X）=t（X））.定义3.2[L-互模拟]一个对称关系S ∈（C × C）是一个L-互模拟，如果CSD意味着，对于任何对，I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3951的状态s和t，使得s=Lt和<$C，s<$和<$D，t<$是良构的：如果<$C，s<$→ <$CJ，sJ<$，则存在DJ，tJ，使得D，t两个程序C，D是L-互相似的，CLD，如果CSD对某个L-互模拟S.请注意，模拟程序需要通过一次或零次移动来模拟第一个程序的每次移动。 这种低互模拟的概念受到[4]的启发。我们可以选择一个较弱的概念，其中用→→代替→→， 如[27]中所述。然而，我们的选择允许更精确的安全概念，它尊重定义3.3[L-安全性]一个程序C是L-安全的，如果CLC。当L是明确的，我们将简单地谈论低平等，低互模拟和安全性。示例3.4下面是一个程序框图，其中循环Dd=ef（当tt做D时）：C=（ifXH= 0then loop（YL：= 0;YL：= 1）elseloop（YL：= 1;YL：=0））不是L安全的，因为条件的分支不能在一步或零步中模拟彼此的移动。然而，根据在定义3.2中用→替换<$→得到的较弱的L-互模拟概念，它将是安全的。3.2Milner现在我们回顾一下Milner这种翻译使用了CCS的两个新结构，重命名和条件，我们假设其语义是已知的（参见[18]或全文[6]）。首先，引入寄存器来对存储进行建模。对于每个程序变量X，由其包含的值参数化的关联寄存器RegX由下式定义：defRegX（v）=putX（x）.RegX（x）+getX<$v<$.RegX（v）状态s的转换[s]则是寄存器池，由下式给出：[[s]]=RegX1（s（X1））| ··· |RegXn（s（Xn））， 如果dom（s）={X1，.，Xn}表达式E = F（X1，... .. ，RegXn转化为变量x1，. .，xn），其中f是对应于PARIMP函数F的CCS函数：[[F（X1，.，Xn）]]=得到X1（x1）。···得到Xn（xn）。res=0（x1，.，xn）n。0通道res由辅助运算符Into使用，定义为：PInto（x）Qd=ef（P| res（x）. Q）\res为了模拟顺序组合，引入了一个特殊的通道，在该通道上进程发出终止信号。通道done由辅助操作员52I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39（A SIGN-OP）X：=E，s（SE q-OP 1）C，sC;D，s（SE q-OP 2）nil;D，s（第二部分-第1页）s（E）=tt如果E，则C，否则D，s→C，s（第二部分-第2页）s（E）/=tt如果E，则C，否则D，s→D，s（WHILE-OP1）s（E）=tt当E做C的时候，s →C;当E做C的时候，s（WHILE-OP2）s（E）tt当EdoC，s →nil，s时（PAR L-OP 1）C，sC（PAR L-OP 2）nil（第1段）D，sC（第2段）C图二. PARIMP的操作语义Done，Before和Par，定义如下，假设d，d1，d2是新名称：I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3953Doned=ef完了 0CBeforeDd=efC1Par C2d=ef（C [d/done] |D. D）\d（C1 [d1/done] |C2 [d2/done]|（d1. d2. 完成+d2. D1. 完成））\{d1，d2}54I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39def^^^命令的翻译是：[[nil]] =Done[[X：= E]]=[[E]] Into（x）（putXx. 完成）[[C;D]]=[[C]]之前[[D]][[（ifEthenC1elseC2）]]=[E]]Into（x）（ifxthen[[C1]]else[[C2]]）[[（whileEdoC）]]=W，其中Wd=ef[[(C1<$C2）]]=[C1]]Par[[C2]][E]]进入（x）（ifxthen[[C]]BeforeWelseDone）最后，一个格式良好的配置的翻译定义为：[[C，s]]=（[[C]]|[[s]]）\访问s已完成{done}其中Accs={getX，putX|X∈dom（s）}是状态s的访问排序。正如Milner在[18]中所指出的，上述翻译并没有保持赋值语句的原子性考虑程序C=（X：=X+1<$X：=X+ 1）。C的翻译是：[[C]]=（（getX（x）. resx +1 |res（y）. 把X放进去。d1）\res| (getX(x). resx +1 |res（y）. 把X放进去。d2）\res| (d1. d2. 完成+d2. D1. 完成））\{d1，d2}这里，第二个getX动作可以在第一个putX动作之前执行。 这意味着在两次赋值中可以为X读取相同的值v0，因此可以将相同的值v1=v0+1赋值给X两次。因此，虽然C只产生X的最终值v2=v0+ 2，[[C]也可以产生最终值v1=v0+1。 然后容易 到 看到 翻译 并不能保证安全。让CL=（XL：=XL+1<$XL：=XL+ 1）和DL=（XL：=XL+1;XL：=XL+1）。现在设C=（如果zH= 0，则CL，否则DL）。 C是安全的，但[C]不是。可以用类似的例子（见[6]）表明，为了使翻译保持安全性，它还应该禁止不同变量的赋值重叠，以及表达式求值的赋值重叠为了防止这种错误，我们为整个商店引入了一个全局信号量：Semd=ef 锁. 解锁. Sem相应地，必须在赋值、条件和循环命令的转换中引入锁定和解锁赋值命令的翻译为：[[X：= E]]=锁定。[[E]] Into（x）（putX<$x<$. 解锁. 完成）为了在条件句和循环的翻译中引入锁，我们研究了两种不同的解决方案。I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3955解决方案1. 条件句和循环的第一次修正翻译如下：[[（ifEthenC1elseC2）]]=loc k. [[E]]Into（x） （ifxthenunlock k. [[C1]]否则解锁。[[C2]]）[[（whileEdoC）]]=W，其中Wd=ef锁. [[E]] Into（x）（如果x，则解锁。[[C]]在W之前，否则解锁。 完成）基于解决方案1，我们首次将PARIMP转换为CCS，如图3所示。 这基本上是Focardi，Rossi和Sabelfeld在[9]中提出的翻译的简单版本，其中另外在每个语句的编码（在上述编码中，就在解锁操作之前以便恢复在[xec，s]中的执行步骤和它们在[xec，s]中的模拟之间的直接对应。这是获得完整抽象结果所必需的。解决方案2. 第二次修改的条件句和循环的翻译是基于本地化锁的使用的想法，通过使用锁定和解锁动作作为表达式计算翻译的分隔符。L egets eqX（x）是针对getX1（x1）的一个bbr i a ti ·· ·getXn（xn），andndf（xn）standdforf（x1，.，xn），像往常一样。表示为[E]的表达式E的原子平移定义如下：[[F（X1， . . ，Xn）]]at=loc k.gets eqX（x）。 re sf（x）. 解锁. 0条件句和循环的翻译然后通过在[[（ifEthenC1elseC2）]]=[E]]atInto（x）（ifxthen[[C1]]else[[C2]]）处将[ E ]]替换为[[ E]]来适应。[[（whileEdoC）]]=W，其中Wd=ef[E]]在Into（x）（ifxthen[[C]]BeforeWelseDone）图4给出了基于解决方案2的PARIMP到CCS的第二种转换，其中为了清楚起见，我们用符号[ ]代替[ ]来表示转换。在本文的其余部分，我们将集中讨论第一种翻译，但我们所有的结果也适用于第二种翻译。3.3翻译维护安全在本节中，我们将展示刚刚描述的转换保留了安全性。这个结果将像往常一样，基于源语言中的程序（或更确切地说，配置）与目标语言中的图像之间的操作对应关系。 为了将配置的行为与其图像的行为联系起来，[C]]=（[[C]]|[[s]]|Sem）\Accs{done，lock，unlock}，我们必须提供一种方法来观察CCS 3中[C]]对[[s]执行的更改。到[3]请注意，按照目前的情况，转换将任何配置映射到不可观察的CCS过程。56I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）39Env=信号量：各国翻译defSem =锁定。解锁. Sem[[s]] =RegX1（s（X1））| · · · |RegXn（s（Xn）），如果dom（s）={X1，. .， X n}表达的翻译[[F（X1，. ，Xn）]]=得到X1（x1）。··· 得到Xn（xn）。res_n（x1，. ......、 xn） 0命令翻译[[nil]]=完成[[X：= E]]=锁定。[[E]] Into（x）（putX<$x<$. 解锁. 完成）[[C;D]]=[[C]]之前[[D]][[(ifE then C1else C2）]]= lock. [[E]] Into（x）（如果x，则解锁）。[[C1]]否则解锁。[[C2]]）[[(whileEdoC）]] =W，其中Wdef=锁定。[[E]] Into（x）（如果x，则解锁。[[C]]在W之前，否则解锁。已完成）格式良好的配置文件的翻译：访问状态的排序：[[C，s]]=（[[C]]|[[s]] |Sem）\Accs {done，lock，unlock}defAccs={getX，putX|X∈ dom（s）}图三. 将PARIMP翻译成CCS在[25]和[9]中，我们引入了专用于进程和环境之间数据交换的特殊通道，我们称之为in和out：环境使用X中的通道将新值馈送到寄存器RegX中，而通道outX以检索RegX的当前值。然后，对寄存器的定义进行调整，以说明新的动作。每个注册X 在我们的翻译中被可观察寄存器ORegX所取代 定义如下：defORegX（v）X（x）= 0。ORegX（x）+getXv。ORegX（v）+锁. （在X（x）中）。 解锁. ORegX（x）+解锁。 ORegX（v））+锁. （outXv. 解锁. ORegX（v）+解锁。ORegX（v））在这里，在inX（x）和outX_x_v请注意，在提交通过锁操作与环境通信之后，可观察寄存器总是可以通过执行以下操作来撤回其提交：一个解锁动作，并返回到其初始状态。这确保了当与信号量并行运行时，可观察寄存器总是与某些状态S的图像弱双相似。记法：设Env是集合{inX，outX|X∈Var}。 我曾发誓，环境保护行动{α ∈ Act |subj（α）∈ Env}.I. Castellani/Electronic Notes in Theoretical Computer Science 194（2007）3957def信号量：Semd=ef锁. 解锁. Sem各国翻译[s]| ··· |RegXn（s（Xn）），如果dom（s）={X1，.，Xn}表达的翻译[F（X1，. ，Xn）] n = getX1（x1）. ··· 得到Xn（xn）。 res= 0（x1，. ，xn）n。 0`getse<$q<$X→（x→）x`f<$（→x<$）x表达式的原子翻译[F（X1， . . . ，Xn）]nat= loc k. gets eqX→（→x）. res=f（→x）昂洛克湾0命令翻译[nil][X：= E] [E] 解锁. 完成）[C;D][（ifEthenC1elseC2）][（whileEdoC）] =W，其中Wdef= [E]Haven't（x）（ifxthen[C]BeforeWelseDone）[（C1<$C2）]格式良好的配置的翻译：[|[s] |Sem）\Accs {done，lock，unlock}访问状态的排序：访问s={getX，putX|X∈dom（s）}见图4。 PARIMP到CCS58I. Castellani/Electronic Notes in Theoretical Computer Scienc