《定量分析：程序泄漏机密数据的信息论方法》-基本信息论分析程序可能泄漏的机密信息量

《理论计算机科学电子札记》59卷第3期（2002年）网址：http://www.elsevier.nl/locate/entcs/volume59.html14页机密数据泄漏的定量分析大卫·克拉克1伦敦国王学院计算机科学系塞巴斯蒂安·亨特2伦敦城市大学计算机系Pasquale Malacaria3伦敦大学玛丽皇后学院计算机科学系摘要基本信息论是用来分析由一种非常简单的命令式语言编写的程序可能泄漏的机密信息量特别是，给出了一个详细的分析，可能泄漏由于平等测试和如果声明。该分析是作为一组语法导向的推理规则，可以很容易地自动化。1引言我们使用基本信息论来分析由非常简单的命令式语言（无迭代）编写的程序可能泄漏的机密信息量。我们处理与[VS00]主题相同的问题，但使用不同的方法。我们的工作是出于这样一个事实，这是相当普遍的程序泄漏可接受的少量敏感数据的信息[RMMG01]。原型是在允许访问敏感资源之前执行密码检查的程序。虽然密码检查保护资源，1 电子邮件地址：david@dcs.kcl.ac.uk2 电子邮件地址：seb@soi.city.ac.uk3 电子邮件地址：pm@dcs.qmw.ac.uk在CC BY-NC-ND许可下开放访问。克拉克、亨特和马拉卡瑞亚2210.80.60.40.2001020 3040熵50 60图1.一、作为密码熵的函数的密码校验的泄漏由于失败的尝试（略微地）缩小了攻击者需要探索的空间，所以它还泄漏了关于密码LE的少量信息。我们首先使用非常基本的信息理论，正式定义“信息量”的含义我们继续开发语法指导的规则，允许由程序泄漏的信息量的界限被自动确定。为了说明关键思想，考虑一个执行单个密码检查的程序，其中密码存储在k位变量中。密码有2k个可能的值如果密码是随机分配的，我们可以假设变量的概率分布是均匀的根据熵的基本信息理论度量（见第二节），2.1）变量则“包含”其k位的最大信息内容（但注意，通常占用内存中k位的变量完全可能包含少于k位的信息）。在这种情况下，要在一次检查中发现密码是非常困难的，特别是对于大k。然而，如果可能值的分布变得不那么均匀，通过使某些值比其他值更可能，通过一次测试就可以更容易地学习下面给出的分析取决于这样一个测试的有效性如何随k和变量的熵而变化的精确说明，该测试的有效性图1绘制了一个简单的等式测试对熵的最大可能泄漏，对于几个k值注意，当熵增加超过某个点（1 +1 log（2k 1））时，最大可能泄漏下降到接近零的最小值。1.1相关工作我们在本文中描述的工作并不是首次尝试将信息理论应用于分析导电性。最早的例子8位变量32位变量64位变量泄漏克拉克、亨特和马拉卡瑞亚3我们所知道的是在Denning的书[Den82]中，她给出了一些信息理论如何通过一些命令式语言程序结构来计算机密数据泄漏的例子。然而，她没有开发一个系统的，正式的方法来解决这个问题，因为我们在本文中。另一个早期的例子是乔纳森·米伦[Mil87]，它指出了香农在信道容量分析中使用nite状态系统的相关性。最近的工作是詹姆斯W。Gray [III91]，它开发了一个相当复杂的计算操作模型，并将非干扰属性与信息论属性联系起来。然而，这两种方法都不涉及编程语言语法的分析，就像我们在这里所做的那样。与我们自己的工作同时代的是Di Pierro，Hankin和Wiklicky [PHW02]。他们得出一个定量的措施，在概率并发约束语言编写的代理之间的相似性这可以被解释为一个间谍（代理人）如何使用概率隐蔽通道区分两个代理人的难度的度量，度量为0意味着两个代理人是不可区分的。他们的方法不处理信息理论意义上的信息，尽管[PHW02]中示例4中的隐含假设是值空间的熵是均匀的。相比之下，更多的已经做了关于语法直接分析的非干扰属性。特别是看到工作的桑兹和Sabelfeld [SS99，SS00]。2泄漏我们假设程序的变量Var被两个向量划分~xh 高安全性变量~xl低安全性变量我们假设固定一些概率分布p上：这是分布的初始值，即输入到程序进行分析。我们在这里注意到，第3节所作的分析并不要求p被完全指定。我们在这篇文章中关注的是最初在~xh中的信息量，攻击者可以通过观察程序的运行来学习这些信息。攻击者只有很低的安全特权：它无法观察到ve~xh 但能直接观察到~ xl的初值和终值。F或x2Var，对x的解释旨在对可以学习的关于~xh 从x的最终值。 我们的观点是，如果lea kage为零，则程序满足非干扰性。克拉克、亨特和马拉卡瑞亚4defdef2.1信息论如上所述，在安全分析中使用信息论并不新鲜。尽管如此，它与我们所处理的问题的相关性可能不是立即显而易见的。在这里，我们试图通过呼吁一类可能的攻击者的直观合理的操作模型来激励其使用。我们首先回顾香农的基本定义。[Sha48].为了我们的目的，一个随机变量在一个集合V是一个变量V采取值在V和配备了概率分布。 P（v=v）是v取v值的概率。 香农定义了v的信息量的以下度量，他称之为entrop y：（一）H（v）d=efXP（v1= v）logP（v=v）在这里和本文的其余部分，log以2为底。假设我们（不知何故）确定，根据这个度量，程序的可信输入的信息内容减去泄露的信息量，是n比特。这告诉了我们什么关于确定我们的秘密有多难？ 当然，这取决于攻击者能够做什么。 我们假设攻击者能够猜测秘密v的值，并且有一个可以（廉价地）证实或反驳猜测的预言。这里很关键的一点是，神谕只能回答这样的问题：“是v = v吗？”“而不是更一般的是/否问题。 假设atta ck知道v的分布，最好的策略显然是从猜测最可能的v开始，并以可能性的降序进行，直到确定秘密。熵的相关性由以下结果给出，这是由James L. Massey [Mas94]：猜测秘密所需的平均猜测次数至少为（1=4）2n+1。2.2随机变量和程序变量假设f：A！B. b=f（a）是指b是B中的随机变量，使得P（b = b）=Xa2 f1bP（a= a）假设给定随机变量a在A中，函数f：A！B和G：A！C、对def def以及关联的随机变量b=f（a）和c=g（a）。我们的新产品随机变量b和c的两种主要方式：配对We写，用于随机变量（a）。 这是以明显的方式扩展到更高arity的向量。我们通常写P（ b1=b1;b2=b2 ） 而不写P（=）。对于随机变量，我们写为bc=cP（bc=c=b）=P（b=bjc=c）=P（b=b;c=c）Pv克拉克、亨特和马拉卡瑞亚5（c=c）克拉克、亨特和马拉卡瑞亚6defdefdefI（0def00def设s0为随机变量，使得P（s0=）= p（）。其余部分中的所有感兴趣的随机变量将是s 0的函数。F或x2Var，我们设x=（：x）（s0）：因此，P（x=n）计算如下：P（x=n） =P（（：x）（s0）=n）= P（s0x = n）=X8：x =np（）在状态Transformer f：！ 是理解的，我们也德内输出随机变量0d=ef（：fx）（s0）：对于向量~xh和~xl 的高安全性变量和低安全性变量，我们将随机变量关联起来：h=（：（~xh））（s0）l=（：（~xl））（s0）其中是的元素扩展到变量向量。 我们让h和l的取值范围分别超过h和l的取值范围。2.3泄漏定义我们对泄漏的定义可以被看作是Gray [III91]基于两个系统之间的互信息概念提出的建议的专门化这里我们需要条件熵的概念。给定b的条件熵为：(2)H（j）=XP（= b）H（）defab bab=bB在这些条款中重新陈述并专门针对当前设置，Gray的建议是将泄露到x的信息量定义为：（3）h;x j l）=H（x j l）H（x （j h;l）其原理是，I（h;x0jl）是h和x0h共同给出的信息量，l是已知的，并且它被定义为eH（x0 jl），即，给定低输入的完全知识，x的最终值的不确定性减去H（x0 jl j h;l），即x的最终值中的“内在不确定性y”，即，即使在完全知道所有输入变量的初始值的情况下，x的最终值的不确定性仍然存在。 在当前设置中，H（x0j h;l）始终为0，因为我们的编程语言是确定性的（状态Transformerf是一个函数）。这很容易检查。令f：！ 设v=f（s0）. 下一个：(4)L（）= H（j）=XP（= 1）H（）defV V l lvl=lL我们使用v是为了表示一个随机变量，它接受表达式的值，就像接受变X克拉克、亨特和马拉卡瑞亚7量的值一样。 或状态为Transformerf：！ ，我 们 将 n 到 x 的leakage定义为eL（x0）。克拉克、亨特和马拉卡瑞亚8vH lvlvhl;v>=l;v>defc 2 Comx 2 Var e 2 Exp n 2c：：= skipjx：= e jc1; c2 jif e then c1else c2e：：= x J N j e 1 + e 2 j e 1e 2 j e 1e2j：e j e1 ^e2 j e1< e2 j e1e2 j e =n表1语言2.4关于定义的意见我们选择的衡量标准意味着，可供泄露的机密信息总量由下式给出：（5）H（hjl）=XP（l=l）H（hl=l）L实际上，这是L（10）的上界。我们还注意到，当h和l是indepnt：H（hjl）=H（h）：我们本可以选择衡量“安全性”，而不是衡量泄漏：S（）d=efH（j;）=XP（=l;=v）H（）l;v当然，这就是l和v的完全知识中的不确定性：攻击者越不确定，程序就越安全。 很容易证明S（v）只是H（hj l）中h不被lea ked的部分：S（v）=H（hjl）L（v）3分析我们分析的语言如表1所示。我们假设以下形式的标准状态- Transformer语义：Vd=eff0;1gk（k位向量2=Var！VC[[ ]]：Com！！E[[ ]]：Exp！！V为了简化表示，我们选择了单个k位整数数据类型，在需要布尔值的地方将0视为false，将1视为true。我们假设一个基本的格式良好性检查，保证表达式在布尔上下文中不接受0，1以外的值。语义学中的+运算符应该被理解为对二进制字的运算，比如二进制补码加法（我们的分析太克拉克、亨特和马拉卡瑞亚9粗糙了，准确的选择无关紧要）。克拉克、亨特和马拉卡瑞亚10defdef有了上述附带条件，语义的细节是例行的，被省略了。这显然是一种非常有限的语言。最严重的限制是它没有提供任何形式的迭代。扩展我们的分析以处理有界迭代是相当简单的，但无界迭代提出了更基本的问题。这一点将在第3.8节中进一步讨论。一个不太明显的限制是，该语言的相等性测试要求一个参数是一个常数然而，分析可以扩展到应付一般的平等测试，这一点也讨论了节。三点八3.1分析如何工作分析程序的最终目的是对每个低安全变量x给L（x0）设置一个上界。我们的目标是以一种组合和增量的方式分析程序。我们从输入（s0-见第2.2节）的概率分布的部分指定开始。更确切地说，我们开始为每个变量x指定一个包含H（x，j）的整数。直接分析程序的H（x0jl）值是有问题的，因为它需要知道l个变量~xl 而这样 的人不 知道什么是不可能的。或者，攻击者实际上可能提供低输入。我们提出的分析避免了这个问题，通过计算低变量的完整的一组可能的输入值的泄漏的最好和最坏的情况下的界限。这些界限定义如下：（六）L（vH（1）=minH（1vl=l）（七）L+（vH（1）=maxH（1vl=l）这里的最小值和最大值是针对定义H（vl=l）的所有l（也就是说，所有l都满足P（l=l）>0）来计算的。这些量boundL（v）：提案3.1L（v） L（v） L+（v）3.2推理规则该分析作为表2和表3中的推理规则的集合来呈现。3.用于命令的规则NoAss在命令上使用了一个辅助函数X：=：这只是返回所有变量x的集合，这些变量在命令中的任何地方都是赋值的目标;它的定义对于所考虑的简单语言来说是显而易见的，因此被省略了。我们注意到，这些规则可以很容易地以函数形式呈现并自动化。公式（2）和公式（3）的规则需要一些简单的数值方法，在第二节中简要讨论。三点五在这些规则中，是从Var到闭区间[a; b]的部分函数， 范围0 a b k。我们写x：[a; b]来表示部分函数克拉克、亨特和马拉卡瑞亚11nEConj[a1;b1]`e：[a2;b2]`e：[max（a1; a2）; min（b1; b2）]常数变量`n：[0; 0];x：[a; b]`x：[a; b]和ei：[ ;bi]`（e1^e2）：[0;b1+1b2]Neg`e：[a; b]`：e：[a; b]加上ei：[ ;bi]`（e1+e2）：[0;b1+kb2]等式⑴`e：[ ; b]`（e =n）：[0; min（1;b）]e：[a; ]1.等式（2）Qk; U k（q） 一（e = ）：[B（q）; 1]2’e：[a;]11等式⑶（e =n）：[0; B（q）]2KQ2; U k（q） 一表2表达式的泄漏推理CConj`c#x：[a1;b1]`c#x：[a2;b2]`c #x：[max（a1; a2）; min（b1; b2）]加入`c #1`c#2`c#1; 2dom（1）\dom（2）;`e：[a; b]`c1 #00 `C00号屁股`x ：= e#xSeq：[a; b]`c1;c200号NoAsx62X：=（c）;x：[a; b]` c #x：[a; b]如果（1）ci#x：[ ;bi]`ifethenc1elsec2#x：[0; b+kb1+kb2]2克拉克、亨特和马拉卡瑞亚12如果（2）`e：[0; 0]` ci #x：[ai; bi]`ifethenc1elsec2#x：[min（a1; a2）; max（b1; b2）]表3命令泄漏推理克拉克、亨特和马拉卡瑞亚13xxxs0将x发送到[a; b]并且具有域f x g。1;2表示具有不相交域的部分函数的并集。非正式地，蕴涵`c#x：[a; b]的含义是程序cm o在这样的情况下对x进行操作，即 L （ x0 ） a 和 bL+ （ x0 ） 。为了正 式 化 这 一 点 ，givenf：！，对于一个新的y2Var，让fd=ef （：f）（）。 Say，fj=x：[a;b]，若L（xf）a且bL+（xf）. 进一步地，如果fj=（x）对于所有x2dom（），则f j=（x）。那么`c#0的含义由下面的定理给出。定理3.2对于所有命令c和所有f：，如果`c#0然后（8）fj=）f; C[[c]]j=0证明：通过归纳法对高度的推导`c#0。由于篇幅的原因，我们省略了证明的细节推论3.3对于任何初始值，使得 [L（ x）;L+ （ x）]（x），对于llx2dom（），分析给出了正确的结果（假设x是描述x的输入分布的随机变量）。注意，对于低安全性yx，L（x）=L+（x）=0，并且当高安全性y和低安全性y输入不同时，对于高安全性y，L（y）=L+（y）=H（y）。的表达式规则; 的情况。基本上与那些+ 和^和被省略。许多规则都是粗略保守的，仅仅基于这样的观察：随机变量向量的函数的熵不能小于0，也不能超过组成随机变量的熵之和。这适用于And，Plus和If（1）。 下面讨论其余规则中不太明显的规则3.3逻辑规则EConj、CConj和Join是通用逻辑规则，允许子分析的结果被联合。他们的正确性或多或少是显而易见的。3.4分配规则Ass是立即的，因为赋值使变量的随机变量与表达式关联的随机变量一致规则NoAss反映了这样一个事实，即泄漏到变量中的信息不会被任何保持该变量不变的命令所改变（尽管在这一点上参见3.8节）。3.5平等测试形式e =n的测试的分析由Eq规则确定。Eq（1）很简单。通过简单的观察，布尔表达式可以泄漏的信息总量克拉克、亨特和马拉卡瑞亚14def43.532.521.510.5000.20.40.60.8 1图二. 4比特中q的上熵不能超过1，并且由于e =n的含义仅仅是e的含义的函数，因此e =n泄漏的量不能超过e泄漏等式（2）和等式（3）由以下问题的答案来证明。假设v是一个k位随机变量（即，最多有2k个可能的值，hv可以选择e）。 我们假设P（v=n）=q，对某些q. 什么是最大可能值为entrpyH（v）？我们称这个最大值为k比特中q的上熵，记为Uk（q）。由于均匀分布使熵最大化，所以当P（v=n0）对所有n0都 均 匀 分 布 时 ， H （ v ） 可 能 达 到 最 大 值6=n。有2个k1suchn0 并应用H的定义（等式10）。1)立即给予。def12k1（九）Uk（q）= q logq+（1q）日志1 Q规则Eq（2）和Eq（3）是基于这样的观察：q被约束为使得L（v）Uk（q）的值。一旦我们已经确定了q的可能值的范围（十）B（q）= qlog1Q+（1）q）日志11 Q这个想法是由g中所示的例子来说明的。2.图中画出了当k = 4时，Uk（q）和B（q）与q的关系，并表明当a = 3：75的熵下界时很容易看出，当q = 1=2时，B（q）达到其最大值1，而当q = 1=2k时，Uk（q）达到其最大值k。这留下两个感兴趣的区域：q 1=2k和1=2k q 1=2，对应于a = 3：75Uk（q）B（q）q=1=2kq = 1=2克拉克、亨特和马拉卡瑞亚15规则Eq（2）和Eq（3）。ND最大和最小的q在这些地区，我们需要解决方程的形式Uk（q）a = 0，为此，简单的数值技术success [BF 89]。(In事实上，随着k的增加，Uk变得接近线性，因此非常简单的几何近似可能就足够了。）3.6对if-then-else如上所述，如果（1）是非常保守的。我们注意到，条件e的熵的贡献对应于丹宁所谓的隐式信息ow。如果（2）适用于布尔条件具有零熵的情况。这意味着条件的值完全独立于高安全性输入的值。因此，最小化和最大化程序的总体泄漏的低安全性输入的选择将各自仅选择两个分支中的一个，并且取下限中的较小者和上限中的较大者是安全的。3.7例如设c为命令，如果y = 0，则x：= 0，否则x：= 1，其中y为高安全性，x为低安全性。 假设k = 32，并且输入分布使y均匀地超过其232x的可能值和指数。 这样我们可以从0= f x：[0; 0]; y：[32; 32]g开始分析c。上面提出的规则很容易得出：0`y= 0：[;]哪里= B（1=232）七点八分，十点七分。(The最终规则是EConj，前提由等式（2）和等式（3）给出。因此，使用If（1），我们得到：0`c#x：[0;]3.8分析的改进第一个可以很容易地作出的改进是记录在明确的界限上的基数的空间，在该空间上的随机变量是defned的。目前，规则隐含地假设边界为2k，其中k是原始数据类型的长度。显式地将允许我们很好地处理均匀或接近均匀但稀疏的输入分布（将概率0分配给2k个可能的输入中的许多）。这也有助于将Eq规则推广到形式为e1 =e2的任意等式检验。 这里的问题是，如果没有对ei的范围的基数的限制，我们可能会天真地做出最坏的情况假设，即q可以均匀分布在大小为2k的整个对角线上。事实上，在许多情况下，当其中一个表达式的熵非常低时，我们可以做得比这好得多，通过计算可以携带给定q的集合的大小的上限。克拉克、亨特和马拉卡瑞亚160def我们还可以更好地处理if语句。规则If（2）是弱的，因为它没有考虑任何一个分支被选择的相对概率在许多情况下，概率的界限是可用的（例如，通过相等性测试的分析为了说明If（2）的弱点，让c0成为命令ify= 0thenx：=yelsex：= 1，这在语义上等同于3.7节中的c，但我们可以为c0导出的最好结果是完全没有信息的：`c0 #x：[0; 32]这个问题是由语句x：= y引起的，孤立地说，它会将y中的所有信息泄漏到x中。但是，在这个if语句的上下文中，它实际上没有泄漏任何信息。仔细分析条件句会得出以下结果。命题3.4设c为命令，如果e then c1 else c2。让V成为一个跑-defdefdefdom变量in，设b=[[e]]（v），t=（：[[c1]]x）（v），f=（：[[c2]]x）（v），i=（：[[c]]x）（v）。 Letq=P（b=1）（当ce1q=P（b=0））。然后（11）0H（i）（qH（tb=1） +（1q）H（fb=0））H（b）使用这个结果可以导出If（2）的另一个（但更复杂）版本，对于c0这样的例子给出更好的结果。这个结果也可以用来将一个非均匀输入分布分解为两个更接近均匀分布的分布，分布在一对划分域的子集上，然后将对这些划分的单独分析的结果组合起来（这里b将表示划分域的属性最后，我们简要地讨论了迭代的棘手问题。在现有规则的基础上，有可能处理有界形式的迭代，只需将它们视为nite深度的嵌套if语句。 在许多安全敏感的上下文中，有界迭代可能是足够的，因此值得追求这样的扩展的细节。然而，最终我们希望能够有效地分析相当一般的程序，所以我们需要处理无界迭代。但是，当然，由于非终止的可能性，这使我们超出了我们在这里假设的简单状态转换器语义。这提出了一个基本的理论问题，因为（至少）有必要定义一个对部分函数的图像有意义的信息度量。 我们猜想，熵的形式定义可以在作必要的修改后应用于“分布”之和可能小于1的情况，并且这将给出一个合理的度量（直观地说，非终止性不是可以观察到的东西，而是没有观察）。即使这是真的，重大问题仍然存在。首先，非终止的可能性会使NoAss规则无效：使用高安全性输入到ect终止，while循环即使没有进行任何变量分配也可能泄漏信息。其次，我们认为，在迭代（甚至有界迭代）的存在下，考虑信息的速率变得更合适克拉克、亨特和马拉卡瑞亚17信息可能泄漏，而不是泄漏的绝对量。这是正在进行的研究的主题。4结论和未来工作我们已经提出了初步的结果，在一个正在进行的尝试，以开发一个通用的和实际有用的分析，为混凝土性能。我们的结果处理程序，可能会泄漏一些机密信息，我们关心的是，以确定泄漏的信息量的界限。像我们之前的其他人一样，我们已经将信息论应用于这个问题。我们的工作与以前的工作不同之处在于，我们强调的是可以自动化的分析，因此，必须直接根据程序的语法来定义（当然，正确性是根据语言的语义来建立的）。与[VS00]中的Volpano和Smith不同，我们关注的不是建立渐近极限，而是量化实际泄漏量。我们的方法是能够得到很好的结果，通过平等测试泄漏少量的信息的程序。到目前为止，我们还不能以令人满意的方式处理无界迭代。 我们的攻击者可以观察到的模型过于简单，无法解决更微妙的泄漏形式，例如可能由定时属性引起的泄漏。显然，要做的事情很多。作为优先事项，我们希望将上述工作扩展到攻击者可以观察到的更现实的模型，并从强调绝对泄漏转移到[VS00]中的泄漏率分析这意味着从简单的指称语义设置到操作设置（或更复杂的指称设置）的转变。特别是，看看是否可以调整[SS 00]的操作设置将是有趣的。引用[BF89] Richard L. Burden和J. Douglas Faires。数值分析PWS-肯特，1989年。ISBN 0-534-93219-3。[Den82] D. E. R.丹宁密码学和数据安全。1982年的艾迪森-韦斯利。[III91] James W.格雷三世信息的数学基础安全性低。在Proc.1991 IEEE Symposium on Security and Privacy，第21页，第34页，Oakland，CA，1991年5月中[Mas94] James L. 梅 西 猜 测 和 熵 。 IEEEInternational Symposium onInformation Theory，Trondheim，Norway，1994.[Mil87] I'm sorry.隐蔽通道容量。1987年IEEE Symposium on Research inSecurity and Privacy。 IEEE Computer Society Press，1987.克拉克、亨特和马拉卡瑞亚18[PHW 02] A.迪皮耶罗角Hankin和H.维基基几乎不干涉。在CSFW'02 {第15届IEEE计算机安全基础研讨会，布雷顿角，新斯科舍省，加拿大，2002年。[RMMG01] P.Y.A. Ryan，J. McLean，J. Millen，and V. Gilgor.不干涉，谁需要它？在第14届IEEE计算机安全基础研讨会的会议记录中，第237页，238页，Cape Breton，Nova Scotia，Canada，2001年6月。美国电气与电子工程师协会。[Sha48] ClaudeShannon. 沟通的数学理论。The Bell System Technical日记，27：379{423和623{656，1948年7月和10月。可在labs.com/cm/ms/what/shannonday/paper.html 网 站 上 查 阅 。http://cm.bell-[SS99] Andrei Sabelfeld和David Sands.安全信息的每个模型在顺序程序中。欧洲方案拟订专题讨论会论文集，荷兰阿姆斯特丹，1999年3月。Press.[SS00] Andrei Sabelfeld和David Sands。多线程程序的可能无干扰。 在第13届IEEE计算机安全基础研讨会，英国剑桥，2000年7月。IEEE计算机学会出版社.[VS00] Dennis Volpano和Geo rey Smith。秘密和相对秘密。在Proc.27thACM Symposium on Principles of Programming Languages ， pages268{276，Boston MA，Jan 2000.