命令式编程语言中变量干扰的定量分析及其在信息流安全中的重要性

理论计算机科学电子笔记112（2005）149-166www.elsevier.com/locate/entcs量化干扰一段时间语言大卫·克拉克1伦敦国王学院计算机科学系英国伦敦塞巴斯蒂安·亨特2英国伦敦城市大学计算机系Pasquale Malacaria3伦敦大学玛丽皇后学院英国伦敦摘要我们展示了如何使用信息论来定量定义命令式编程语言中变量之间的干扰。在本文中，我们专注于这种干扰定义的一个特殊情况：在While语言程序中，信息从私有变量泄漏到公共变量本文的主要结果是对这种语言进行定量分析，该语言采用使用定义图来计算泄漏到每个变量的界限。关键词：安全，程序分析，信息论，信息流，干扰1介绍量化干扰是评估安全设备中的隐蔽通道的重要部分，并且这样做对于可编程1 电子邮件地址：david@dcs.kcl.ac.uk2电子邮件地址：seb@soi.city.ac.uk3电子邮件：pm@dcs.qmul.ac.uk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.018150D. Clark等人理论计算机科学电子笔记112（2005）149而不是简单的硬件组件。采用程序变量之间的干扰[5，10无干扰（不干扰）通常用于证明系统行为良好，而干扰可能导致神秘的（错误）行为。然而，由干扰引起的重大不当行为通常只有在有足够干扰时才会发生这方面的具体例子有由基于访问控制的软件系统提供进入这样一个系统用户必须通过识别阶段;无论该阶段的结果（授权或失败）如何，某些信息已经被泄露（在失败的情况下，用于正确密钥的搜索空间现在变得更小）。因此，这些系统存在干扰[5]，因此它们在定性意义上不是“安全的”。然而，常识表明，如果干扰非常小，则认为它们是安全的。本文使用Shannon我们简要回顾了Shannon然后，我们使用这些定义作为程序分析的基础，该程序分析推导出程序泄漏的机密信息量的界限。在以前的论文[1]中，我们概述了一个基于信息论的程序分析的一个简单的语言没有循环。本文介绍的成果是：分析结构和循环：现在的分析是图形化的，而不是基于语法的;这允许我们处理循环。相等性测试：我们分析一般的相等性测试（不像以前那样只针对常数进行测试）。算术表达式：我们提出了一个显着改进的算术运算符的分析，利用其代数属性。1.1相关工作我们在本文中描述的工作并不是第一次尝试将信息理论应用于分析保密性。我们所知道的最早的例子是在Denning然而，她并没有发展一个系统的，正式的方法来解决这个问题，因为我们在这篇文章。另一个早期的例子是米伦[8]，它指出了相关性，D. Clark等人理论计算机科学电子笔记112（2005）149151香农在信道容量分析中使用有限状态系统。最近的工作是格雷[14]，它开发了一个相当复杂的计算操作模型，并将非干扰属性与信息论属性联系起来。然而，这两种方法都不涉及编程语言语法的分析，就像我们在这里所做的那样。与我们自己的工作同时代的是迪·皮耶罗、汉金和维基基[9]。他们的兴趣是在概率并发约束设置的上下文中测量干扰，其中干扰通过概率运算符来实现。他们得出一个定量的措施，在概率并发约束语言编写的代理之间的相似性。这可以被解释为一个间谍（代理人）将如何难以找到它来区分使用概率隐蔽通道的两个代理人的度量，度量为0意味着两个代理人是不可区分的。他们的方法并不处理信息理论意义上的信息，尽管在该论文的例子4中隐含的假设是值空间的概率分布是均匀的。相比之下，更多的已经做了关于语法直接分析的非干扰属性。特别是看到工作的桑兹和Sabelfeld [11，12]。然而，我们最近引起作者注意的一篇关于保密性质的论文是[ 7 ]，它确实使用了他们对“信息逃逸”的定义[7]的重点是安全属性和加密之间的关系，而不是分析程序泄露的信息量。与本文件工作的联系值得进一步研究。2信息理论与泄漏分析2.1语言该语言只包含以下控制结构：赋值、while语句、if语句、顺序组合.as-1的左边是变量标识符，右边是整数或布尔表达式;而循环和if-语句则以标准方式涉及布尔表达式。我们不完全指定表达式的语言，但我们假设所有表达式都定义商店的总函数。语言是确定性的，因此，对于每个程序P，语义诱导一个偏函数[P]]：n→ n，其中n是存储区域。存储器σ∈ε152D. Clark等人理论计算机科学电子笔记112（2005）149ZHy|X只是一个从变量名到k位整数（整数n在−2k−1≤n2k−1范围内）和布尔值的有限映射。我们注意到，处理循环的主要兴趣不是非终止的可能性，而是通过包含隐式信息流的迭代泄露任意数量信息的可能性（隐式信息流是通过控制流而不是从机密源分配来实现的）。给定一个程序P，一个程序点是特殊节点ω（出口点），或者是在P中出现的任何赋值语句，if-语句或while-语句。我们称最上面的程序点为I（入口点）。操作语义是标准的，定义了一个关于配置（n，σ）的转移关系→，其中n是程序点，σ是存储。迹是一个配置序列（n1，σ1）···（nj，σj）使得（ni，σi）→（ni+1，σi+1），其中1≤ij。2.2干扰与信息论我们假设一个程序的变量被划分为两个集合，H（高）和L（低）。当程序运行时，高变量可能包含机密信息低变量在程序运行之前不包含机密信息，并且可以在程序执行之前和之后（但不是在程序执行期间）由攻击者自由检查这就提出了一个问题，即攻击者可以通过检查低变量输出来了解机密输入。一种被广泛研究的保密方法[5]是基于这样一种概念：不干涉：程序是否泄露机密信息。在这里，我们通过对比来解决有多少可能被泄露的问题。我们使用香农有关当前工作的信息论背景的讨论，请参见我们以前的论文[1，2]。回想一下，香农（一）（X）d=ef p（x）log1p（x）X其中X是一个随机变量，p（x）是P（X=x）的简写，即随机变量X=x的概率，其和在X的范围内。的导出了一致性函数为H（X）的条件|Y）d=efp（y）H（X|Y=y），当r为H（X|Y=y）d=efp（x）log1，p（x y）是p（x）|年）的D. Clark等人理论计算机科学电子笔记112（2005）149153defι{|{\fnSimHei\bord1\shad1\pos（200，288）}≤defΣ假设随机变量Y=y，则随机变量X=x。2.3随机变量和程序点我们为每个程序点定义一个随机变量，该变量对应于该点上变量值的观测值。特别是，我们感兴趣的是，有多少信息所携带的高输入到一个程序可以通过观察低输出，假设低输入是已知的。由于我们的语言是确定性的，输出的任何变化都是输入变化的结果。因此，一旦我们考虑到程序的低输入的知识，输出中唯一可能的意外来源就是高输入的干扰。给定一个程序变量（或一组程序变量）X，设Xi和Xω分别是进入和退出程序时的相应随机变量（现在假设终止;这在下面是放松的）。我们把由于程序而泄漏到X（二）L（X）=H（X|L)（其中L1是描述程序非机密输入分布的随机变量）。我们注意到，此设置中的无干扰只是0泄漏的特殊情况。(We在[2]中给出了这个结果的精确的形式化描述，并更一般地讨论了为什么这个定义是合适的。）在程序点n处X的随机变量被定义为使得P（Xn=x）是给定控制通过程序点n时X取值x的概率。然而，n可能是不可达的，或者对于给定的输入存储σ，控制实际上可能多次通过n，其中X在不同的时间取不同的值由于这些原因，Xn仅定义为程序点的子集。设t是迹（n1，σ1）···（nj，σj），其中n1=1。的迹t决定 nj，如果对于所有延伸t的迹，ni=nj意味着i j。给定一个程序点n，设n（n）为集合（σ，σJ）（i，σ）（n，σJ）决定n.我们将p（n）写为n（n）的域的概率之和p（n）=（σ，σ<$J）∈<$（n）p（σ）可以将n（n）解释为在其定义域上的随机变量，但一般来说，我们感兴趣的是n（n）的特定投影特别地，随机变量Xn具有与p（n）相同的域，并且仅在p（n）>0时定义P（Xn=x）d=ef（σ，σJ）∈N（n），σJ（X）=xp（σ）p（n）ω154D. Clark等人理论计算机科学电子笔记112（2005）149def≤−−→（X可以是一个变量向量，在这种情况下，σJ（X）意味着σ对其元素的逐元素应用）。 注意，Xn描述了X在n处执行任何指令之前立即采用的值。 随机变量Xn的定义自动扩展到随机变量En的类似定义，其中E是语言中的任何表达式（En是描述E在n处求值时取的值的随机变量）。我们将上述泄漏的定义（公式2）概括如下。 让我们做一个新的程序。 n对E在n处的代数为Ln（E）d=efp（n）H（En|L1），当p（n）= 0时取Ln（E）为0。注意，对于总是终止的程序，p（ω）= 1，所以这推广了前面的定义L（X）=Lω（X）。本文的其余部分致力于展示如何在Ln（E）的界限可能被计算。3泄漏分析程序本节介绍分析，其中有两个主要部分：• 一个定性的（3.1• 一个定量的（3.3本节以正确性结果结束。我们使用的图是一种使用定义图。我们更喜欢这些语法，因为它们公开了我们用来处理循环的结构。应该注意的是，回路是泄漏分析中的一个重要障碍。考虑3.1节中的程序。稍微想一想就可以看出，对于取0i216 1中的值，这个程序通过变量high和low复制到out，即使没有从high赋值到low。3.1使用定义图给定一个程序，使用定义图（UDG）是一个有向图，其节点是程序点。如果n是一个赋值X=E的出现，我们称n为一个定义节点，并说n定义X。一个节点n称为一个使用对于变量Y，如果Y出现在表达式中的n处（即，控制构造的布尔表达式或赋值的右侧）。有两种类型的边：(i) data edges（n p）：有一个从n到p的数据边i，如果程序从n开始到p，在没有任何X插入的定义的情况下，程序的流程图中有一条非空路径，n是一个定义D. Clark等人理论计算机科学电子笔记112（2005）149155其中n=1，并且p是X或p=ω的用途;(ii) 控制边（n−−·p）：存在从n到p的控制边i，n是while或if语句，p是在该语句中发生的赋值。对于−→−·，Werite=，对于其transiti ve-re x i veclo sure，W e r i t e =。考虑以下示例程序：int maximum = in;int b = 15，low = 0;while（b >= 0）{intm =（int）Math.pow（2，b）;if（high>= m）{low = low + m; high = high- m;}b = b- 1;}return low;图1显示了该程序的数据边沿（a）和控制边沿（b）。3.2源节点当计算在一个特定程序点上已经嵌入到一个变量中的信息量时，我们使用UDG来识别程序的其他部分，这些部分立即做出贡献;我们称这些为变量给定出现的源节点在定义这些源节点时，我们需要区分那些位于while语句中的程序点和那些不位于while语句中的程序点我们之所以需要做出这种区分，是因为我们的分析是从循环中可能的循环信息流的复杂性中抽象出来的：循环中的方法（粗略地说）是以处理外部边缘的相同方式处理UDG路径为了理解以下定义，请记住：a−−·bib位于控制结构a内（if或while）。设n是变量X的用法;有两种类型的源节点，n处 X的控制源节点，记为conn（X），以及n处 X的数据源，记为datn（X）。当n出现在程序中时，conn（X）是集合m∈datn（X）{mJ/∈W：mJ−−·m和mJ−−·n}156D. Clark等人理论计算机科学电子笔记112（2005）149高=在b=15低=0while（b>=0）m=pow（2，b）if（high>=m）低=低+m高=高−mb = b−1out=低out=低（a）数据边缘（b）控制边缘Fig. 1.一个简单的Java程序datn（X）的定义根据n是否位于a内而变化while-语句：(i) 如果n位于while语句中，设w是包含n的最外层，则dat n（X）是集合：{m：w−−·m，<$mJ。w−−·mjn}。(ii) 如果n不在while语句中，则datn（X）是集合：{m：m定义X，m −→ n}。在conn（X）的定义中，请注意，将mJ限制为不在任何while语句中的点，其结果是所有控制源节点都是if-语句，并且没有控制源节点位于while-语句中。这并不是因为while条件不能直接控制while语句（它们显然可以），而是因为我们对循环的分析比对if语句的分析更悲观。因此，X在n处的数据源节点是紧接在n之前的赋值（或在包含n时到最外面的赋值）;控制源节点是那些if-语句，它们确定那些赋值中的哪一个（如果有的话）实际发生（假设控制通过n传递）。无需区分数据和控制源的情况高=在b=15低=0while（b>=0）m=pow（2，b）if（high>=m）低=低+m高=高−mb = b−1D. Clark等人理论计算机科学电子笔记112（2005）149157while（b>=0）m=pow（2，b）if（high>=m）def节点，我们考虑联合：srcn（X）= datn（X）conn（X）。UDG中的每个内部节点（即，除了i和ω之外的每个节点）都具有一个关联的表达式：右边的赋值，控制语句的布尔条件;我们称之为n处的表达式，写为E（n）。通常有必要考虑表达式中出现在节点或其子表达式之一的所有变量的所有源节点的集合;给定任何这样的表达式E，我们表示这个集合srcn（E）：srcn（E）={ src（X）：X出现在E中}defn图2（a）说明了while循环中的定义，所有源节点都位于循环之外。它显示了一个典型的源节点集合，用于在循环内的程序点p处的赋值X=E的rhs。高=在b=15低=0低=低+m高=高−mb = b−1out=低(a)（b）第（1）款图二.计算循环图2（b）显示了从其数据源节点到分配low=low+m的一组可能路径（遵守上述定义的存在性由此我们可以看出，在3.1节的例子中，循环内相应赋值的rhs与源节点集合{high=in，b=15，low=0}相关联。Y1=E1 Yn=En循环节点X=E158D. Clark等人理论计算机科学电子笔记112（2005）149defλλ{∈}λλλλλλλλ3.3恶魔袭击者到目前为止，我们（隐含地）假定初始外挂物空间上的概率分布这个假设有两个潜在的问题：(i) 虽然可以合理地假设，人们对高投入的分布情况会有一些了解，但对低投入的情况可能了解甚少或一无所知;(ii) 低输入的分布实际上可能在攻击者的控制下;在这种情况下，假设攻击者选择L1以最大化泄漏将是保守的。我们通过构建我们的分析来处理这两个问题，以给出对低输入的所有可能分布都是安全的结果。该方法本质上是假设低输入取某个固定（但未知）值λ。这种方法的安全性由命题3.1验证。请注意，我们假设高输入不在攻击者的控制之下。因此，我们正在模拟一种情况，在这种情况下，向程序提供高输入的环境是可信的，即使程序本身不是。 例如，这适用于分析要下载并在用户计算机上运行的不可信代码对于每个可能的选择Li=λ，我们定义pλ（n）为给定Li=λ，程序点n最终被决定的概率（见2.3节）。形式上：pλ（n）=（σ，σJ<$）∈<$λ（n）p（σ）/P（L1=λ），当re（n）d=ef（σ，σJ）σ（n）：σ（L）=λ。在给定L i = λ的情况下，我们可以在程序点定义第n个随机变量：当p λ（n）> 0时，我们定义eXnd=efXn|L1=λ。最后，我们可以定义在n处i n到X的lea k age，给定Li=λ：Ln（X ）d=efp（n）H（X n），假定Ln（X）d=ef0，其中np（n）=0。从这里开始，我们假设λ是固定的，但不假设它的身份这对于Ln（X）是保守的，如下所示：建议3.1（A）. Ln（X）≤a）<$Ln（X）≤a注意，对于所有X∈L和所有λ，Li（X）=Li（X）= 0。此外，当高安全性输入和低安全性输入独立时，Li（Y）=H（Yi），对所有Y∈H。D. Clark等人理论计算机科学电子笔记112（2005）149159λ−H|λ- -Xλλdef3.4总体与部分随机变量我们下面提出的规则旨在推导出泄漏到程序点的变量的界限，仅假设入口点处的置信变量的熵。这样的假设实际上给出了非常有限的输入值分布的知识，这意味着在程序点直接计算泄漏通常是不可能的。为了说明，假设程序点n是以下程序中的赋值L = H：if（H 0）then L =Helse L = 1 fi现在假设H和L是独立的32位变量，并且H（H）= 16。为了直接计算泄漏到L中的量，我们需要计算Ln（H），但这又要求我们计算p（n）和H的熵，p（n）是条件（H <0）为真的概率，而H的熵是条件（H<0）为真的概率。但是只知道H（H）= 16，我们不能计算这两个量。特别地，（HH<0）基本上可以取0和31之间的任何值。(For下界，对于h的最小值（232216），设p（h）= 0，对于其余值，设p（h）= 1/216对 于 上界，设b= 2 31−a且ab（1 b）log（1b）= 16;则令p（h）= 1/ 2a，当h0，p（0）= 1时b，当h >0时，p（h）= 0。我们通过计算一个hypotical随机变量X n 的 熵 的 界 来 处 理这个困难，其中X n在每个地方都有定义。Letχnbethedef定义域的特征函数：χ n（σ）= 1，若σJ. （σ，σJ）∈N（n）;否则，Xn（σ）= 0。然后，将n定义为全随机变量，suchthatX n=X<$ n|χη=1。正确性原则中定义了X值λ λ λ（定理3.2）。3.5分析规则基本分析由表1所示的规则给出。为了便于说明，我们假设如下：(i) 高变量（H1，H2，. . ）只被用作形式X=Hi的赋值的rhs，然后最多一次(ii) 没有高变量被赋值请注意，这些假设仅具有表示意义，因为一旦Hi已复制到X中，该副本可自由使用和分配一个判断n<$[E]<$a（其中<$是≤，≥，=之一）应被读作一个证明H（E<$n）<$a的命题。分析的初始假设将160D. Clark等人理论计算机科学电子笔记112（2005）149[Min][麦克斯]n[E]≥ 0n [E]≤ bits（E）[DP]n1<$[E（n1）] ≤b1，.，nk<$[E（nk）] ≤ bkn≤[E]ΣKi=1KBsrc n（E）={n1，.，n k}[常数]n[E]= 0srcn（E）=0[低]p<$[E（p）]≥an[X]≥an/∈W，srcn（X）={p}表1分析规则作为高变量的特殊初始化公理给出，每个形式：n[Hi]a其中n是Hi的第一个也是唯一的用途。在所有其余的判断中，有两件事是不言而喻的：(i) E是E（n）或E（n）(ii) E不是高变量Hi在规则[Max]中，bits（E）表示由表达式E的类型确定的存储位数（例如，如果E是布尔型，则bits（E）为1;如果E是Java注意，与其他规则不同，规则[Low]的结论仅适用于变量，而不是任意表达式，并且仅适用于不在任何while语句中的程序点。规则[DP]之所以如此命名，是因为它本质上是由信息理论的所谓数据处理定理[3]所证明的：函数输出的信息量不能超过输入量。规则[Const]实际上是规则[DP]的一个特例，但为了强调而单独声明：常量表达式传输零信息。例如，考虑如何在语句low=low+m在3.1节的循环示例中。如果我们假设in在0≤i 216上均匀分布，那么很容易看到，使用规则，我们得到所有16位泄漏到低。D. Clark等人理论计算机科学电子笔记112（2005）149161λλλλλλ^^3.6正确性定理3.2假设，对于每个初始化公理，导出n<$[H]a对于所有λ，H（H i）≠ a。 然后，对于每个程序点n，每个子E（n）的表达式E，并且每个λ，存在一个随机变量：(i) En=En|χn=1乌斯季(ii) 只要表1中的规则导出n<$[E]<$a，则H（E<$n）<$a推论3.3n<$[E] ≤b蕴涵Ln（E）≤ b。定理第二部分的证明取决于以下引理：Lemma3. 4LetEnbeasgivenbypart1ofthethe o r em. 那么，如果srcn（E）=λn1{n1， . . . ，nk}，存在函数f∈h，使E∈n=f（E（n1）λnk，...，E（nk）λ）。表1中的规则的正确性如下，因为f（X）的熵不能大于X的熵（所谓的信息论数据处理定理[3]）。4重新定义表达式表1中的规则允许我们通过程序来测量信息流，但以一种粗略的方式，类似于管道连接。根据我们的方法实施的分析的效用将取决于其敏感性，即能够建立严格的，而不是松散的界限上的信息泄漏虽然我们仅限于循环内部的基本分析规则这些细化规则的发现是一个正在进行的项目。在本节的其余部分，由此产生的规则见表2。请注意，这些规则仅适用于循环外部。4.1平等测试在本节中，我们将开发一个用于分析形式为E1==E2的检验的细化规则。这一发展表明，计算中间点处表达式熵的良好下限有时将能够计算泄漏的良好上限。我们的开发是出于一个简单的观察：当E1的值的分布接近E162D. Clark等人理论计算机科学电子笔记112（2005）149defB ≤≤如果E1和E2的分布是均匀的（高熵），而E2的分布集中在少数几个值上（低熵），那么在大多数情况下，E1和E2将不相等。假设X是k位随机变量并且假设P（X=x）=q，对于某个q，H（X）的最大可能值是多少？我们称这个最大值为k比特中 q的上熵，记为Uk（q）。由于熵通过均匀分布而最大化，因此在P（X=xJ）对所有xJ/=x均匀分布的情况下获得H（V）可能的最大值。有2k− 1个这样的xJ，应用H的定义（方程n）。1）给出：def12k− 1（三）Uk（q）=qlogq+（1−q）log1−q如下面的命题所示，如果P（X=Y）=q，则Uk（q）是H（X）和H（Y）之间的差的上界命题4.1给定一个k比特的随机变量X和任何其他随机变量Y，设q= P（X = Y）。则H（X|Y）≤ Uk（q）。作为直接推论，我们有H（X）− H（Y）≤Uk（q）。现在感兴趣的量（H（X==Y））就是B（q），其中def1 1（4）B（q）=qlogq+（1−q）log1−q显而易见，（q）是q在0区域内的递增函数Q0的情况。5，这足以证明等式检验的精炼规则[Eq]（见表2）。(We不用说明伴随规则，由=的交换性证明，它颠倒了E1和E2的角色。）我们注意到，[Eq]将在a为高而b为低的情况下给出有用的结果（即，远小于1），也就是说，当已知E1包含大量机密信息而E2包含很少时。图1所示的例子说明了规则[Eq]的应用方式。3 .第三章。 图中画出了当k = 4时Uk（q）和B（q）对q的关系，并显示了当（a-b）= 3时的下界。75，q的界为0 ≤q≤ 0。25（精确的上限略低于此）。为了找到q的最大值，我们需要求解形式为Uk（q）−（a-b）=0的方程，为此，需要使用简单的数值方法[6]。(NoteB（q）+（1−q）k是Uk（q）的上界，除非k很小，否则这个界是非常紧的。作为一个例子，考虑程序P：Y = H;[p]if（Y == 0）then[n0]X = 0 else[n1]X = 1fi;[n2]Z = X假设k=32，H的输入分布是均匀的。因此，我们可以从假设<$K[H]≥ 32开始分析程序。 基本规则加上[Eq]可以很容易地推导出：D. Clark等人理论计算机科学电子笔记112（2005）149163图三. 4比特中q的上熵表2某些细化分析规则（仅限外部循环）B（1/2 32）107. 8× 10−9。 因此，使用[Const]和[DP]，我们导出n2<$[Z] ≤<$。4.2算术表达式我们可以通过利用运算的代数知识以及以下信息来改进算术表达式的泄漏分析164D. Clark等人理论计算机科学电子笔记112（2005）149H--·∗def公司简介HH通过奇偶性分析、常数传播分析等补充分析得到的操作数，考虑了k位整数的二补表示的一元求反、加法和乘法（，+，）.一元否定只是一个置换，因此很容易被看作是关于熵的恒等式，因此[Neg]。我们用来表示任何二元运算符。对于随机变量X，Y，Z，其中Z=X<$Y，我们知道（通过数据处理定理）H（Z）≤ H（X）+（Y）。这就是[OpMax]。就其本身而言，这个规则并没有比[DP]更好然而，我们可以实现改进的下界（因此，通过[Eq]，改进的上界）。众所周知，+使得k位数的集合为二补数，即具有单位元0和生成元1的循环加法群。我们利用的键群性质是，每当x=y+z时，x，y，z中的每一 个 都 由 其 他 两 个 唯 一 确 定 。 这 足 以 建 立 以 下 结 果 ， 从 而 证 明[AddMin]：命题4.2设Z= X + Y。 然后H（Z）≥max（H（X），H（Y））−min（H（X），H（Y））乘法不像加法那么容易分析，因为运算的代数结构更复杂。然而，当其中一个操作数是常数时，我们有时可以在输出的熵上建立好的界限。例如，X0总是零，因此（X0）= 0，故[ZeroMult]。事实上，这可以被看作是一个更一般的群性质的结果，即·n生成一个子群，其阶由n的阶决定。特别地，当n是奇数时，n的阶数就是整个群（2k）的阶数由此可以得出，对于奇数n，n（像一元否定）是关于熵的恒等式。我们注意到，在这种情况下，不需要确定n的值，只需要n是常数（一旦低输入为已知），且n是奇数。我们的分析已经捕捉到了恒定性（n=[E] =0 ） ，但需要进行单独的分析 以确定奇偶性。这些事实足 以证明[OddMult]。建立一个更一般的公式，涉及（X），（X n）和n的顺序，仍然是未来工作的主题。4.3正确性引理3.4和定理3.2很容易扩展以适应表2中的附加规则。关键的观察结果是，D. Clark等人理论计算机科学电子笔记112（2005）149165λλ►≤B −►≤H ≤ HH32 32−8当应用新的规则时，我们不仅知道引理的函数f存在，而且知道它实际上是哪个函数上述结果直接证明了新规则的合理性。5进一步改进分析我们对if语句的分析有效地分布在UDG结构的定义和规则[DP]之间。如正确性证明（定理3.2）所示，基本原理是，在点n处，在定义了Xm之后，可以查看XmB、Y和Z的函数，对应于X分别在真分支和假分支的末尾数据处理Theoremthenimpliesthat（Xn）（B）+（Y）+（Z）. 这种方法的一个特点是，它没有考虑任何一个分支被选择的相对概率。概率的界限在很多情况下（例如，通过分析平等测试提供）。作为一个例子，让PJ是程序Y = H;如果（Y==0），则X = Y，否则X = 1fi; Z = X;这在语义上等同于4.1节例子中的P，但我们对PJ最多只能推导出完全无信息的：n[Z] 32。这个问题是由语句X = Y引起的。孤立地说，这会将Y中的所有信息泄漏到X中，但在这个if语句的上下文中，它实际上没有泄漏任何信息。我们可以通过使用我们所知道的关于q的知识来改进这样的例子，其中q是条件评估为真的概率。对于等式检验（见4.1节），由于应用了[Eq]规则，我们可以得到q的显式界。更一般地说，给定布尔表达式B的n[B]b，我们可以反转（q）来找到q或1q的上界（尽管通常我们不知道是哪个）。在某些情况下，这可以用来收紧导出的上限。在上面的例子中，[Eq]规则的应用提供了q的界限1/ 232 因为我们知道H（X|B = 1）≤ k对于任何k位变量X，我们是能够得到大大改进的：n<$[Z] ≤32/2+ B（1/ 2）1. 5 × 10。6结论和今后的工作本文介绍的工作是第一次信息理论已被用于自动化分析测量变量之间的干扰一个明显的和非常可取的工作扩展将是一个语言的概率运算符。166D. Clark等人理论计算机科学电子笔记112（2005）149作者要感谢Peter引用[1] 克拉克，D.，S. Hunt和P.Malacaria，机密数据泄漏的定量分析，电子笔记理论计算机科学59（2002）。[2] 克 拉 克 ， D. ， S. Hunt 和 P.Malacaria ， Quantified interference for a while language ，Technical report，King[3] 掩护T M.和J.A.。托马斯，[4] Denning，D. E. R.，“Cryptography and Data Security,” Addison-Wesley,[5] Goguen，J.和J. Meseguer，安全策略和安全模型，在：IEEE安全和隐私研讨会（1982），pp.11-20[6] 伯登河和j.D. 张文龙，[7] McIver ， A. 和 C. Morgan ， A probabilistic approach to information hiding ， in ：Programming methodology，Springer-Verlag New York，Inc.，2003年，pp. 441-460[8] Millen，J.， 隐通道容量，单位：Proc. IEEE Symposium on Research in Security andPrivacy（1987）[9] Pierro，A. D、C. Hankin和H. Wiklicky，近似不干涉，在：I. Cervesato，编辑，CSFW[10] 雷诺兹，J.C.，干扰的语法控制，在：会议记录第五届ACM研讨会。《程序设计语言原理》，ACM，纽约，图森，亚利桑那州，1978年，pp. 39比46[11] Sabelfeld，A.和D.Sands，顺序程序中的安全信息流的每个模型，在：Proc. 欧洲方案拟订专题讨论会（1999年）。[12] Sabelfeld，A.和D.Sands，Probably noninterference for multi-threaded programs，in：Proc.13th IEEE Computer Security Foundations Workshop（2000）。[13] 香农，C.，通信的数学理论，贝尔系统技术杂志27（1948），页。379- http://cm.bell-423和623-656，可在www.example.com上在线获得。HTM L.[14] W.格雷，J.，III，Toward a mathematical foundation for information security，in：Proc.1991 IEEE Symposium on Security and Privacy，Oakland，CA，1991，pp. 21-34号。