安全概率约束的声明式编程研究 - 概率版本的约束性质分析及其正确性验证

理论计算机科学电子笔记48（2001）网址： http://www.elsevier.nl/locate/entcs/volume48.htmlpp. 1- 23声明式框架中的概率约束Alessandra Di Pierro比萨大学信息学院意大利比萨克里斯·汉金2赫伯特·维基基3帝国理工学院计算机英国伦敦摘要我们将展示如何制定和分析一些安全概念的声明式编程的上下文中。 我们集中讨论一类特殊的安全性质，即所谓的约束性质。我们的参考语言是并发约束程序设计.我们使用这种语言的概率版本（PCCP）通过简单的程序示例来强调概率和非确定性确认之间的差异。变量在命令式和约束式编程中扮演的不同角色阻碍了将约束的概念直接转换为声明式设置。因此，我们引入了更适合于约束语言的身份限制的概念。最后，我们提出了一个近似的概率语义，它可以作为基础的confinement属性的分析，并显示其正确性方面的PCCP的操作语义1ncn这项工作的目的是调查的安全问题，从概率的角度来看，通过形式化的一个方面，这个问题的多形式的性质，我们考虑的方面是保密的，即保护一些敏感数据免受未经授权的攻击1电子邮件地址：dipierro@di.unipi.it2电子邮件地址：clh@doc.ic.ac.uk3电子邮件地址：herbert@doc.ic.ac.uk2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。DIPIERRO，H ANKIN和WIKLICKY2管理公开这方面可以用非干扰概念[8]来形式化，该概念规定了保证整个计算机系统中安全信息流的条件。我们提出了一个基于语义的非干扰属性的正式规范，该属性确保给定的程序不会泄漏一些允许访问的私有信息这个性质通常被称为confinement，以Lampson在70年代首次提出这个问题之后我们的规范是基于概率并发约束编程语言（PCCP），以前在[3，4]中作为并发约束编程的概率扩展引入[10]。PCCP提供的概率选择结构使我们能够考虑攻击者也能够利用一些统计信息。以前的方法，特别是Volpano和Smith [19，17]以及Sands和Sabelfeld[14，13]的工作，考虑了命令式编程语言。我们选择的声明性语言，特别是PCCP语言，基本上是出于可用性的一个简单的和数学上健全的语义，这种语言形成了一个基础上，可以开发一事实上，本研究的最终目的是开发一种类似于经典程序分析方法的（概率）程序的概率安全分析方法[12]。作为这个方向的第一步，我们在本文中提出了一个PCCP程序的控制流分析，它能够根据声明性确认的适当概念来检测程序是否被确认。分析是指一个抽象版本的衍生树的PCCP代理，其中所有可能的商店之间的转换记录在一起，其概率，其正确性显示相对于具体的操作语义。1.1确认如果信息处理系统保护一些重要的（所谓的高级）信息不被未经授权的访问，则该系统具有保密- 所谓低级别访问。这意味着信息，例如高级变量的状态或值，不会“泄漏”出去，即不会泄漏低级信息。在标准安全模型[1]的更复杂的实现中，可能有几个级别（例如，计算机操作系统可能试图保护某些用户信息，例如密码等（高级信息），使其不被某些应用程序访问，例如电子表格、浏览器等（低级应用程序），尽管它很可能允许这些应用程序（低级）访问其他数据，例如系统时间等。用户的密码，我们可以说，DIPIERRO，H ANKIN和WIKLICKY3它是保密的。根据高级和低级信息之间的信息流的性质，可以区分几种类型的确认，即确定性，非确定性和概率确认[19]。重要的是要注意，非确定性确认在某种程度上弱于概率性确认，因为它无法捕获实现的概率性质可能允许检测确认信息的情况，例如。通过运行程序足够的次数[9]。在命令式编程语言的上下文中，最近在[17，20，18]中讨论了关于高级别和低级别变量值的确认属性，其中开发了基于类型系统的安全分析对这个问题的另一个最近的贡献是[13，14]中的工作，其中提出了使用概率功率域，这允许基于类型的安全分析的非干扰属性的组成规范。1.2例子：战争与和平我们提出了一个简单的例子来说明我们在本文中要考虑的安全问题想象一个世界危机的场景：一场新的战争可能开始。五角大楼正在为战争做准备，但没有人知道它是已经在攻击还是仍在谈判。显然，这一情报是他们只允许有限数量的人访问关于五角大楼是处于“战争”还是“和平”状态的一位信息因此，这些信息是严格保密的：五角大楼然而，外部人员仍然可以访问低级信息，例如。通过新闻办公室。然而，这种低层次信息的处理为了避免系统过载），而在后者中，GHQ对必须处理低级别信息的方式没有限制那么问题是：如果一个人可以观察五角大楼的行为，而不直接访问敏感信息，例如。通过正常的通信手段，是否仍然可以获得（间接）关于它是处于“战争”还是“和平”状态的信息1.3的方法上面的问题可以通过首先给出一个正式的规范来回答，根据编程语言语义，哪个信息流被认为是安全的我们攻击上述问题的方法的基础上正式的编程语言的语义。为此，我们使用概率并发约束编程（PCCP）语言，这是介绍DIPIERRO，H ANKIN和WIKLICKY表44||ǁCCPCCP代理商名单A：：=p成功终止|e(c)adding a constraintni=1K （ci）→pi：Ai概率选择ni=1 qi：Ai优先并行|∃ xAhiding, local variables|p (x)procedure call, recursion在[3，4]中作为并发约束编程（CCP）范式的概率版本这种语言的基本特征及其语义在第2节中回顾。在第3节中，我们使用这种设置来正式说明我们认为什么是安全的信息流。在将问题形式化为一个确认属性之后，我们现在可以应用静态分析方法来保证给定的程序具有安全的信息流。我们将采用控制流程分析法.在第4节中，这种分析的抽象规范是通过只考虑在程序执行中发生的转换的那些元素来定义的，这些元素包含检测违反confinement属性所必需的然后证明分析在语言的语义方面是安全的（参见。第5节）。2PcCncenC nnnPnPCCP的语法和基本执行模型与CCP非常相似。这两种语言都基于通用约束系统的概念，定义为圆柱代数完全偏序（更多细节见[16，2]），它编码信息排序。在PCCP中，通过概率选择和概率并行的形式引入概率，前者取代了CCP的非确定性选择，后者通过引入优先级取代了CCP交织语义中的纯非确定性在下文中，我们回顾PCCP代理的语法和基本操作模型PCCP程序P是一组形式为p（x）的过程声明：-A，其中A是代理人。PCCP代理的语法在表1中给出，其中c和ci是中的有限约束，并且pi和qi是表示概率的实数。DIPIERRO，H ANKIN和WIKLICKY5i=1i i ipjjjH−→我我XX表2PCCP过渡系统1e（c），d− →1p ，cHd2000 年（c）→p：A，d<$−→ <$A，d<$ j∈[1，n]且d<$c3<$Aj，c<$−→p<$AjJ，cJ<$nnj∈[1，n]⟨ǁi=1 pi：Ai，c−→p·pj ⟨ǁj=/i=1 pi：Aipj：AJj，cJ4A，dHdA，c5<$p（y），c<$−→1<$A，c<$p（x）：−A∈PPCCP的操作语义在概率转移系统（Conf，−→p）方面有一个简单的定义，其中Conf是表示系统在某个时刻的状态的配置集，p的定义见表2。系统的状态由仍然要执行的代理A和公共存储器d描述。转移关系中的指数p表示发生转移的概率。这些规则与（非确定性）CCP的规则密切相关，我们参考[2]进行详细描述。规则1描述了e（c）的效应这个代理总是以概率1成功终止，并且新的存储是约束c和当前存储d的最小上界，即c d。 请注意，代理p表示成功终止，并用于区分成功与其他形式的终止，例如。死锁（未启用保护）或一般情况下代理人陷入困境的情况。两个规则2和3指的是正态概率pi。规范化可以定义为一个通用的实数集X={xi}，作为替换eachxibyxi的过程，定义如下：Σnn2.1设x=ixi，n是X={xi}的基数y。然后十月 =xX=阿维尼翁一世X1n如果x/= 0，否则我们规范化的符号中的上标。xX用于表示集合X，规则2描述了概率选择。代理Ai称为启用的iDIPIERRO，H ANKIN和WIKLICKY6X∃--|∃{|}⟨ ⟩ ∈⟨⟨⟩−→⟩它的保护ci由存储，即d_ci所限定。上述归一化过程仅应用于与启用的代理相关联的那些pi因此，p_i然后仅在启用的代理中进行选择第3条 描述了一种优先级交织：每次调度器必须选择要执行的代理时，它将根据概率pi进行选择，即相对于集合pi归一化的概率Ai是活动的。一个代理A被称为活动的，如果它可以进行转换，即。存在AJ，dJConf这样， A、dp AJ，dJ. 同样，归一化和连续选择仅适用于活性剂这样，一个智能体的成功概率实际上代表了它的优先级[6]。请注意，从p代理到任何其他代理的转换没有规则，即p 从来没有活跃过。表2中的规则4处理局部变量的引入;我们使用符号dA表示代理A，其中局部存储d包含关于x的信息，该信息对外部存储是隐藏的（更多细节请参见[15，16，2]）。显然，转移概率p不会因隐藏而改变。在过程调用p（y）的递归规则5中，我们假设在p（y）被程序P中它的定义体替换之前，实际参数y和形式参数x之间的联系已经正确建立。在[16]中，这个链接通过使用隐藏操作x和仅一个新变量来优雅地表达。由于这是一个确定性操作，因此该规则中的转移概率为1。基于这些转换规则，我们现在定义了PCCP的操作语义，即观察量的概念，它捕获给定代理的有限次执行结果及其概率。首先，让我们介绍一些基本的定义。enn二、2设A是一个年龄为nt的PCCP。A的计算路径可定义为：= A1，c1 ... −→pn<$An，cn<$，其中A0= A，c0=真，An=pn<∞。请注意，此定义仅适用于成功终止。我们的可观察量将不包括无限计算，也不包括最终配置中的代理人不是p代理人但无法进行转换的情况，即暂停计算的情况。enn二、3设e为A的计算路径，A0，c0 A1，c1 ... −→ pn <$A n，c n <$.我们将结果定义为res（n）=cn，将其概率定义为prob（n）=ni=1 皮岛我们用Comp（A）表示A的所有计算路径的集合。给定一个PCCP程序，代理A的结果的集合RP是DIPIERRO，H ANKIN和WIKLICKY7⟨⟩∈⟨ ⟩ −→ ⟨ ⟩·所有对c，p的（多）集合，其中c是对应于在计算路径期间累积的部分约束的最小上界的最终存储，并且p是达到该结果的概率。RP（A）={\displaystyle\，p\，}|C = res（A）and p = prob（A）}。由于非确定性，可能有不同的计算路径导致相同的结果。因此，我们需要对结果进行该操作的正式定义如下。nn2.4设S={{ci j，pi j}i，j是一个（多）结果集，其中ci j表示约束ci的第j次出现，并令Pci=cipci为与ci相关联的集合中出现的所有概率的总和。的S的定义如下：K（S）={\displaystyle\pi\，\pi\pi}|Pci=cipci=jpi j}i.我们观察到，当涉及无限计算时，这种操作可能并特别是，当派生树有无限多无限分支时，可能会发生这种情况这种情况需要一种更复杂的、测度论的处理，我们在这里不展开这种处理，因为它对本文的目的不是必要的。我们现在可以将与一个主体A相关联的可观测量定义为：OP（A）= K（RP（A））。请注意，这种可观测量的概念不同于CCP中输入/输出行为的经典概念。在经典情况下，如果至少有一条路径从初始存储d通向最终结果c，则约束c属于给定主体A的输入/输出可观量。在概率的情况下，我们必须考虑所有可能导致相同结果c的路径，并结合相关的概率。可以定义一个更一般的计算路径的概念，它对应于从任何存储c开始的计算，而不一定是空的。给定一个代理A，我们用Comp（A，c）表示从存储c开始的所有一般计算路径的集合。当然，Comp（A）对应于Comp（A，true）。计算路径上的一个运算--这将在第5节中被证明是有用的--是prefixing。其正式定义如下：nn2.5设A是PCCP年龄nt，并且WPComp（A，c）是一般计算路径A，c −→ pn <$A n，c n <$.考虑跃迁s=B，dp A，c。我们定义了组成S作为通用计算路径，d B，d −→ pA，c −→ p1A1，c1 −→ p2... −→ pn <$A n，c n <$.DIPIERRO，H ANKIN和WIKLICKY8/i=1Xi=1ΣKi下面的命题陈述了表2中给出的跃迁系统的一个重要性质Ppn2.6LetA，c是一个有A=p和c的函数。则以下条件成立：Σp i= 1。A，c也就是说，从λ A，λ C的转换被归一化。P. 证明是通过归纳A的结构。A= e（d） 根据规则1，只有一个标准化的过渡。nA=i=1k（di）→pi：Ai 规则2中的转移概率p∈j为通过定义进行规范化。A=<$npi：Ai 通过归纳假设，跃迁<$Ai，c<$−→p对于所有的Ai，都归一化Aki，cki，即kipki= 1。而且通过定义对p_i进行归一化。因此，跃迁为npi：Ai，c<$−→p·p巴恩/pi：Aipj：Ak，ck是归一化的，如kj jj=i=1.J J- 是的- 是的ΣΣΣikip˜i·pkiΣ=pi我Σ·pkiKi=1。A=<$dAJ通过归纳假设，跃迁<$AJ，dH <$xc<$−→p<$AJJ，dJ<$是归一化的，因此跃迁dAJ，c− →pdJAJJ，cHxdJ是X x也正常化A=p（y） 根据规则5，过程调用是确定性的，因此是标准化的。✷3ecveCnnen约束的概念通常是根据变量的值为命令式语言制定的在声明式编程中，变量的作用与它们在命令式编程中的作用有很大的不同因此，我们将引入一个在我们的陈述式设置中更合适的确信概念。它指的是一些代理的身份，而不是一些变量的值：如果不可能指定一个上下文，可以确定哪个代理实际上被执行，则代理集合Ai我们可以想到由某个商店给出的上下文，或者更一般地说，由一个代理C给出的上下文，只要它与每个Ai组合运行当C与每个Ai并行执行所获得的结果不同时，情况就是这样，这允许我们区分Ai请注意，商店上下文的第一种情况是通过限制某个商店c的代理C=e（c）来获得的。DIPIERRO，H ANKIN和WIKLICKY9ǁ≡≡ǁǁ在我们的设置中唯一有趣的上下文是并行组合，因为在其他结构化代理中的子代理之间没有交互，就像选择一样。enn 3.第三章。1一组年龄ntsAi是恒等的，如果对于所有年龄ntsC，并行执行A i<$C在观测上都是等价的，即如果所有的观测量O（A i<$C）都是相同的。根据人们可能提到的可观测量的概念，人们可以获得不同的确认属性。特别是，如果我们基于经典的非确定性I/O观测量OC进行分析，我们可以区分非确定性身份确认和概率身份确认，如果我们查看概率I/O观测量OP。3.1更多关于战争或和平的例子第1.2节中描述的例子可以在（P）CCP框架中公式化我们引入一个代理P，P（entagon），定义为：波多克 （战争）→ 1：A k （和平）→1：B根据是或B定义为：1 1A2：e（c）2：e（d）和B e（cH d）也就是说，在“战争”时期，“战争”和“和平”的约束如果我们现在看一下非确定性确认，我们看到对于代表世界C（真实性）的主体C，整个系统P C在“战争”和“和平”时期具有相同的I/O行为OC（AC）=OC（BC）也就是说，非确定性观测量A<$C和B<$C是相同的。国际社会不能决定这是战争还是和平，仅仅因为五角大楼仍然产生同样的可能结果。 P A或P B的身份受到保护，没有C可以测试差异。因此，“高”层次的信息（“和平”或“战争”）被限定在非确定性的意义上。然而，如果我们看一下概率确认，我们会看到A C和B C可能有稍微不同的行为（语义）。事实上，代理人：2 1C.克尔克 （c）→3：e（e） k （d）→3： e（f）。如果我们将A和B与C组合，我们将得到图1和图2中描述的两个派生树（根据表2中给出的操作语义DIPIERRO，H ANKIN和WIKLICKY10222222222211第2章：A ǁ2：C，真核1122一曰： e（d）1：C，c 1：e（c）1：C，d（d）、c1121998年12月 20日///e（c），dHf13联系我们p，cHdHeFig. 1.1：A的执行1：C1：B1：C，真11998年12月 20日/2个/3///✠p，cHd He图二.1：B1：C的执行因此，相应的概率观测值分别为：.Σ1 1 7 5OP2：A2：C={cHdHe，12，cHdHf，12}.Σ1 121OP2：B2：C={cHdHe，3，cHdHf，3}因此，通过反复询问P或与P交流，我们能够弄清楚它是“战争”还是“和平”。例如，如果我们执行120次PC，我们将得到大约70次cHdHe和50次cHdHf作为结果iPA（五角大楼正在准备战争），但大约80次cHdHe和40次/DIPIERRO，H ANKIN和WIKLICKY11cHdHf作为结果iPB（五角大楼正在维持和平）。DIPIERRO，H ANKIN和WIKLICKY12⟨⟩i=1⟨⟩我我我 我 我我i=i我我我 我我表3PCCP药剂[[p]]=0[[e（c）]]={true，c， 1}[[nK （c）→p：A]]=（p，c，[[A]]）[[q：A]]=（q，[[A]]）[[xA]]=[[A]][[p（x）]]=[A]]p（x）：−A∈P4nnA n我们的目标是开发一个分析PCCP程序的置信属性的框架。我们的分析旨在为程序构建所有可能的转换集，以检测代理的不同行为结构，这最终将使我们能够揭示他们的身份。对于这个分析，我们抽象了全部语义，因为我们忽略了每个计算步骤中涉及的具体代理，并且只记录了存储（约束）之间可能的转换及其概率。这些转换--形式上用三元组c、d、p表示--可以看作是图的弧，它表示真实派生树的抽象版本通过考虑通过图的最大无环路径，可以恢复程序意义的近似一般来说，抽象图将大于真实语义。4.1抽象语义为了分析PCCP程序，我们将每个代理关联到一组三元组c，d，p。每个三元组由两个约束和一个概率组成对这样一个三元组的解释是，从第一个约束标记的节点到第二个约束标记的节点有一个过渡-这种过渡的概率是第三个分量。表3给出了这种语义的正式组合目前我们只考虑有限约束系统。表3中的操作需要一些辅助结构，我们将在下面介绍。我DIPIERRO，H ANKIN和WIKLICKY13联系我们关于我们⟨⟩4.1.1起始组对于一个三元组c，d，p以及一组可能的转换ci，di，pii，我们可以通过投影到其中一个分量，即和i（c，d，p）=cτ（τc，d，p）=dπ（πc，d，pπ）=pi（{ci，di，pi}）={ci}τ（{ci，di，pi}）={di}π（{πc i，di，p i}）={p i}.对于一组三元组ci，di，pi，我们定义初始或前缀转换为第一个分量在任何其他转换中从未出现的转换形式上：I（{c i，di，p i}i）={e，f，q <$∈ {c i，di，p i}i|ci，d i，p i= c i，/ci，di，pi：e=di}通过投影，我们可以简单地将初始外挂、概率等提取为i（I（{ci，di，pi}））、π（I（{ci，di，pi}））等。4.1.2辅助操作给定一个三元组c，d，p（表示从存储c到存储d的可能转换，概率为p），我们将其在另一个约束e的上下文中的执行定义为：ec，d，p=eHc，eHd，p我们可以将这个概念扩展到可能的转换的集合{ci，di，pi<$}ie{ci，di，pi}i={eci，di，pi}i={eHci，eHdi，pi}i类似地，也可以改变单个三元组的转移概率或一整套：q·dc，d，p=dc，d，q·pq·{ci，di，pi}i={q·ci，di，pi}i={ci，di，q·pi}i对于一组转移，我们也可以定义一个prefix乘法，其中只有初始概率乘以q：q×{ci，di，pi}i=q·I（{ci，di，pi}i）{ci，di，pi}i\I（{ci，di，pi}i）最后，我们需要类似的操作来引入选择：xDIPIERRO，H ANKIN和WIKLICKY14我再一次，一整套：x{4.1.3集合构造对于选择操作，可能的转换集取决于当前存储。特别是，根据启用了多少个警卫，我们得到不同的规范化。因此，选择的模型如下：（pi，ci，Xi）=.Σp<$G×（G<$Xi）iG∈P（{ci}i） G<$ci即表示可能的保护组合4的所有集合的并集。在每个这样的组合中，查看所有启用的防护，归一化它们的概率（相对于该组合中的其他启用的防护），然后初始转换乘以归一化概率。通过滥用符号，我们使用G来表示一组约束（或等效地表示它们的最小上界）和与启用的防护相关联的概率集对于并行构造，我们必须看一个前缀构造，它源于一个隐式的顺序组合：c，d，p={kc，d，pk，kd H e，d H f，qk}。那么一组三元组的前缀构造是：c，d，p={c，d，p，dHei，dHfi，qi}并行构造的主要元素是合并操作。两组可能的转换X={ki，di，pi}i和Y={kj，fj，qj}j之间的合并可以递归地定义为：XY=c，d，pc，d，p<$∈I（X）<$∪我们有：e，f，qf，p∈I（Y）作为基础案例。X=X=X[4]事实上，只考虑相容的组合，即如果一个保护c需要另一个保护d，则包含c的集合G也必须包含d。DIPIERRO，H ANKIN和WIKLICKY15公司简介很容易看出如何将这种二进制运算推广到n进制运算。国家：你...ΣΣXi=我（b）不受影响;it∈I（Xi）XJj/=ix（X i\ {t}） - 是的因为我们只考虑有限结构，所以合并的递归定义是明确的。为了公式化并行构造的语义，我们需要修改这个通用的合并构造，以便允许加权版本：你...Σ Σ（qi，Xi）=我我t∈I（Xi）（qi·t）;j/=i（qj，Xj）n（qi，Xi\{t}）n，其中我们理解qi的归一化是关于所有qj的对于任何q，对（q，）为我们提供了加权合并操作的基本情况。在仅两个元素之间合并的情况下，这对应于以下要求：（q1，X）<$（q2，<$）=（1，X）=（q1，<$）<$（q2，X）=X.4.2语义近似表3中的分析乍一看几乎可以看作是PCCP的结构化（完整）语义。然而，仔细观察就会发现，情况并非如此。语义近似，我们introduce基本上包括在删除信息的代理人参与的过渡，只记录的可能性，两个商店之间的过渡连同相关的概率。通常，通过考虑最大路径，可以从这种近似语义中重建完整的语义。直观地说，最大路径是从storetrue中的初始转换开始，在图中尽可能深入的路径。形式上，这个概念可以定义如下。enn四、1若一个元组集合S={cj，dj，pj}j，则S的一个序列是一个ny序列{c i，d i，p i}i∈[0，n]<$S，使得c0，d0，p0 <$∈I（S）且对所有1≤i≤n，ci=d i−1.我们现在定义一个关于迹的前缀序≤如下。enn四、2设tr1={ci，di，pi<$}i∈[0，n1]和tr2={ei，fi，qi<$}i∈[0，n2]是S中的两条迹.我们定义prefix order≤：tr1≤tr2i ≥0≤n1≤n2，对于所有i ≤ n 1，均为εc i，di，p iε = εe i，fi，q iε。DIPIERRO，H ANKIN和WIKLICKY16↓{|联系我们对于跟踪树，我们表示为（三）集 TRJSTRJTR，所有 的前缀。DIPIERRO，H ANKIN和WIKLICKY1722nn4.3迹tr_S的最大值为i_tr=l_ub≤↓（tr）。我们用T（S）表示S的所有极大迹的集合。nn4.4我们将最大迹树的结果定义为.其概率为res（tr）=prob（tr）=τ（tr），p.p∈π（tr）A的最大迹的结果定义为：R（[[A]]）={res（tr），prob（tr）|tr ∈ T（[[A]]）}.4.3计算及其近似在某些情况下，我们的近似确实不如完整语义精确，也就是说，最大迹比实际的计算路径要多例如，考虑代理的执行：1 1 1德鲁克（true）→4：（： e（d）2：（k （d）→1： （e））3 1 1K （true）→4：（： e（d）2：（k （d）→1： （e（f）。在storetrue中执行的代理D的语义由图3中描述我们为这个代理获得的可能转换集是：[[D]]={true，d， 1/4，true，d， 3/4，d，d He，1dHe，d He， 1从其中不可能重建实际的语义，（参见。图4）。我们观察到，表示真实语义的派生树（同构于）对应于近似语义的重构树的子树。这显然意味着由真语义给出的观测量是通过近似语义中的最大路径构造的观测量的子集这反映了这样一个事实，即正如我们将在第5节中展示的那样，近似语义是正确的。4.4分析声明性确认作为使用这种转换语义来分析安全概念的一个例子，让我们看看考虑第3.1节中的PCCP代理：1 1A2：e（c）2：e（d）和B e（cH d）DIPIERRO，H ANKIN和WIKLICKY18D，真/1/4/联系我们K （d）→ 1： e（e）、d1p，dHeK （d）→ 1： e（f）、d普，dHf图三. D的执行真/1/4/联系我们Dd1dHedHfdHedHf以及：见图4。 D的失败重建2 1C.克尔克 （c）→3：e（e） k （d）→3： e（f）。A和B分别与C组合的真实语义导致概率性输入/输出可观测量：.Σ1 1 7 5OP2：A2：C.={cHdHe，12，cHdHf，12}Σ1 121OP2：B2：C={c H d H e，3，c H d H f，3}.因此，上下文C允许我们区分A和B。可以使用表3中的语义精确地重构该A的分析给出了[[A]]={1/2真，c， 1/2假，1/2真，d， 1/2假，c，c Hd，1对于B，我们得到：DIPIERRO，H ANKIN和WIKLICKY19[[B]]={true，cHd，1}最后，对于C：DIPIERRO，H ANKIN和WIKLICKY20·[[C]]={\displaystyle\frac，cHe，1\displaystyle\frac，dHf，1\displaystyle\frac，d H f，1\，cHd，cHdHe，2/3cHd，cHd Hf，1/3通过将这些语义与并行规则相结合，我们得到：1 1和[[2：A2：C]]={true，c， 1/2，true，d， 1/2，c，cHd，1/2c，cHe，1/2cHd，cHdHe，2/3cHe，cHdHe，11 1[[2：B2：C]] ={true，cHd，1，cHd，cHdHe，2/3cHd，cHd Hf，1/3通过这些图的最大路径给出与真实语义相同的概率的相同结果。由于我们发现至少有一个语境，即C，在这个语境中，这两个主体的行为是不同的--正如分析所揭示的那样--我们可以断言A和B不是身份限定的。请注意，在经典的CCP情况下（其中所有的概率信息都被删除），AC和BC的非确定性可观测量是相同的：OC（A<$C）= OC（B<$C）={cHdHe，cHdH f}.5Cecne eAn为了表明第4节中介绍的抽象语义为正确分析PCCP程序提供了一个安全的基础，我们研究了表2中根据转换系统给出的具体语义与表3中定义的语义[]在正确性论证中，我们将集中讨论选择和并行结构，并暂时从隐藏和递归中抽象出来如前所述，程序P的语义[P]包括收集P从storetrue开始可以进行的所有可能的转换。每个转换都由一个元组描述，该元组记录初始和最终存储以及转换的概率，而中间代理被抽象掉。直观地说，这使得语义5.1我们定义了与计算相关的最大迹