理论计算机科学电子笔记173（2007）47-66www.elsevier.com/locate/entcs你所失去的就是你所泄漏的：取消分类政策中的信息泄漏Anindya Banerjeea，1RobertoGiacobazzib，2 Isabella Mastroenib，2a堪萨斯州立大学，曼哈顿，KS 66506，美国bUniversita`diVerona，Verona，Italy摘要本文提出了以下方法来检查程序是否满足可能解密秘密信息的信息流策略：（a）计算过近似的有限抽象域由策略释放的信息，以及（b）通过完成有限抽象域wrt来检查程序执行是否可以释放比策略所允许的更多的信息。最弱的自由主义前提。此外，基于Paige-Tarjan算法的分区细化技术可以用来生成去分类策略的反例：反例表明程序释放的信息比策略允许的更多。随后，可以对策略进行细化，以便使程序安全所需的最少量的机密信息被解密。保留字：抽象解释、完整性、非经典化、信息流1介绍安全信息流问题涉及通过检查秘密在程序执行期间不被泄露来保护数据机密性。在最简单的设置中，程序变量首先被划分为高安全性（或私有或分类）和低安全性（或公共或未分类）变量，其中高（H）和低（L）是两点安全网格中的级别，L≤H;接下来，检查L个输出变量不会泄漏H个输入变量的初始值的信息。为了执行检查，已经使用数据流分析等技术开发了用于保密策略的1电子邮件：ab@cis.ksu.edu2电邮地址：roberto. univr.it，isabella. univr.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.02748A. Banerjee等人理论计算机科学电子笔记173（2007）47安全类型系统、程序逻辑等（参见Sabelfeld和My- ers的调查[23]和其中的参考文献）。这种分析的正确性由无干扰（NI）[13]控制：对于程序的任何两次运行，L个不可区分的输入状态产生L个不可区分的输出状态，其中两个程序状态被称为L个不可区分的，如果它们在L个变量的值上一致Joshi和Leino [15]给出了安全信息流的语义定义（已经证明等价于NI [24]）：包含H和L变量（分别由h和l覆盖）的程序P是安全的i =HH;P;HH=P;HH，其中HH是对h的任意值的赋值。“The postfix occurrences of 在实践中，不干涉是一个太强的属性，无法强制执行，信息降级或取消分类是必要的。例如，密码检查器公开实际密码与在登录提示符处输入的密码之间的比较结果（H）。本文基于Joshi和Leino的语义定义允许将不干涉视为抽象解释的完整性[ 10 ]的中心观察一个抽象的解释是（向后）完整的函数，f，如果得到的结果时，f被应用到任何具体的输入，x，和得到的结果时， f被应用于具体输入x的抽象，两者都抽象为相同的值。因此，完整性的本质是这样的：一个观察者只能看到最终抽象无法区分具体输入值是x还是任何其他具有与x相同抽象值的具体值xJ。完整性连接隐含在Joshi和Leino所有可能的H值的集合（这一点已在本书中讨论过2和3）。在本文中，我们考虑了比Joshi和Leino考虑的抽象更灵活的抽象，并表明这种抽象自然地描述了与什么信息被去分类有关的去分类策略[25]。我们的主要贡献（Sects。4，5.1）是为了表明因此，我们可以通过检查一个程序的语义是否是完备的来机械地检查它是否满足去类化策略保单此外，我们证明了当程序不满足去类化策略时（即当完备性失败时），（a）可以生成暴露失败的反例（5.2节）;（b）存在一个算法，该算法生成给定策略的最佳细化，使得程序遵守细化策略（5.3节）。最后，（c）我们将抽象模型检验与安全信息流联系起来，表明前者中不存在虚假的反例可以在站在作为信息泄漏的情况下，在后者（节。6）。A. Banerjee等人理论计算机科学电子笔记173（2007）4749VH2概述注释摘要。 VH，VL是可能的H和L值的集合。编程状态的集合是VH× VL。是由H变量后面跟着L变量隐式索引的对于任何X，XH（分别为XL）是H（resp.L）变量。状态s1，s2∈S的L不变性，记为s1=Ls2，表示当用L个变量索引时，s1，s2Semanticnoninterferencea`laJoshi-Lei no. 我们和约翰还有莱诺一起去-安全性的一个重要定义[15]，HH;P;HH=P;HH，其中HH赋予h一个任意值。由于这种任意赋值，HH的语义可以建模为一个抽象函数H，在具体的程序状态集合上，也就是H：H（n）→H（n），其中H（n）由子集包含±来排序。对于L变量的每个可能值，H关联P中H变量的所有可能值。因此H（X）=VH×XL，其中VH=T，是（VH）的顶元素。现在Joshi-Leino定义可以用下面的方式重写[10]，其中P）是P的具体指称语义。HP）H=HP）（1）例如，设h1，h2∈ {0， 1}，l∈ {0， 1}。 则VH={ 0， 1} × { 0， 1}，VL={ 0，1}。考虑任何X;例如，令X={ 0， 0， 1}，即，X表示其中h1= 0，h2= 0，l= 1的状态。则H（X）=VH× { 1}。设P为l：=h1，使得<$P）（X）={<$0， 0，0 <$}且H（<$P）（X））=VH× { 0}. 另一方面，在一项研究中，<$P）（H（X））={<$0， 0， 0 <$，<$0， 1， 0<$，<$1， 0， 1<$，< $1，1， 1 <$}因此我们有H（<$P）（H（X））=VH×{0， 1};因此H（<$P）（H（X））<$H（<$P）（X））。由于H（P）（H（X））包含三元组H（P）（X））中不存在的三元组H（P）（X））和H（P）（X））中不存在的三元组H（P）（X）），从而揭示了l对h1因此P是不安全的：对于H（P）（H（X））中h1的任何两个不同的值0和1，l的两个不同的值0和1可以相关联。宣布非军事化。对于l：=h1，如果安全策略允许h1的去类化，程序将是安全的。方程（1）自然必须通过解类器φ：（V H）→（V H）对H进行“滤波”来修改“过滤后的 我们要平等对待。Hφ=Hφ（2）也就是说，将<$P）应用于具体输入x，将<$P）应用于x的抽象，其中x的H分量已被φ去类化，两者都抽象为相同的值。如前所述，设P为l：= h1且X={x 0，0，1}。我们对φ我们有，φ（{<$0，0<$}）={<$0，0 <$，<$0，1 <$}：φ是关于必须被解密的东西的恒等式--我们正在释放h 1的精确值--但是φ是关于必须被保护的东西的T，这解释了为什么<$0，0 <$和<$0，1 <$都出现。现在Hφ（X）= φ{<$0，0 $>} × XL={<$0，0，1$>，<$0，1，1 $>}，因此<$P）（Hφ（X））={<$0，0，0 $>，<$0，1，0 $>}和H（<$P）（Hφ（X）= VH×{0}。这等于H（P）（X））。 我们可以证明对任何X∈H都有等式（2）;因此l：= h1是安全的。注意φ是如何将φ（）划分为50A. Banerjee等人理论计算机科学电子笔记173（2007）47块{100，0100，100， 1100}（100，0 100和100，1100的范围）和{101，0 100，101，1100}（100，0 100和 100，1 100的范围）。1，0直观地说，φ允许在公共输出处暴露块之间的区别，例如，在φ0， 0和φ1，0之间;在标准NI中，φ3评论：摘要解释抽象解释通常使用伽罗瓦连接（GC）[5]来制定，但我们在本文中使用的等效框架[6]使用上闭包算子3。 例如，在第2节中，H：H（X）→H（X）定义为H（X）=VH×XL，是H（X）上的上闭包算子，因为H是单调的、幂等的和扩张的。我们通常把闭包算子称为抽象域。特别地，H被称为输出（即，观察到的）抽象域，忽略私有信息。Hφ在Sect.2也是一个UCO。基于静态分析的抽象解释的完整性起源于Cousot的工作，例如，[5，6]，这意味着分析尽可能具有表达性。下面的例子是从施密特的优秀调查[ 26 ]完整为了验证Hoare三元组，{？}y：=−y;x：=y+1{isP_positive（x）}，一个可靠的分析可以计算出前提条件isN_negative（y）。但是如果能够表示像isN onN negative和isN onPpositive这样的性质，则完整的分析将计算出最弱的先决条件性质isN onP positive（y）。一个抽象域对于一个具体函数f是完备的，如果“ 存在两个完备性概念--向后（B）和向前（F）--取决于具体和抽象计算是在抽象域中比较还是在具体域中比较[ 11 ]。形式上，设C是一个完备格，f是具体的状态转移函数，f：C→C。抽象整环ρ是f的一个可靠的抽象，条件是ρ <$f <$ρ ± ρ <$f。例如，在Sect.2，H（P）（H（X））→ H（P）（X）），所以H是P）的一个可靠的抽象。完备性是通过要求相等性来获得的：ρ是B（分别为F）-完全抽象fi <$ρ <$f= ρ $>f<$ρ（resp. f<$ρ= ρ <$f <$ρ）。完备性可推广到抽象域对（ρ，η）：当ρ ∈ f ∈η = ρ ∈ f时，（ρ，η）的B-完备性成立; F-完备性成立对于（ρ，η），当ρ<$f<$η=f<$η时（详见[12]）。例如，在第2节中，去分类示例断言等式（2）成立，即，（H，Hφ）是B-完全的，（P）。存在完成抽象域的算法基本上，F-完备性是通过将f的所有正像加到输出抽象域上来获得的;B-完备性是通过将函数的所有最大逆像加到输入域上来获得的（详见附录A）。3偏序集C上的上闭包算子（uco）ρ：C→C是单调的、幂等的和广延的，即，x ∈ C。 x ≤Cρ（x）。C上所有上闭包算子的集合记为uco（C）。A. Banerjee等人理论计算机科学电子笔记173（2007）4751Q⎣4F-保密 政策的完整性和满足性等式（1）和（2）给了我们一种动态检查程序是否满足保密策略的方法：事实上，这两个等式都使用了进程中程序的指称语义但是我们可以静态地做这个检查我们现在将看到，静态检查涉及F-完备性，而不是B-完备性，并使用最弱的自由前提，而不是指称语义。在最弱的自由主义前提下，（WlpP写作），方程（1）具有以下等效的重新表述：HWlpPH=WlpPH（3）等式（3）表明H对于WlpP是F-完全的。换句话说：考虑通过H抽象具体的输入状态X;这产生一组状态，其中私有信息被抽象为“任何可能的值”。该等式断言WlpP（H（X））是H的定点，这意味着WlpP（H（X））产生一组状态，其中每个公共输入与任何可能的私有输入相关联：定点的进一步抽象（参见，等式（3）的LHS）没有产生新的结果。因为私有输入之间没有区别，所以公共输出独立于私有输入。因此，等式（3）断言标准NI。下面的定理断言用B-和F-完备性描述不干涉的两种方法是等价的。定理4.1 HP）H = H P）i H WlpP H = WlpP H。证据由[11，12]我们知道，如果f是可加的，则对于任何ρ，我们有ρ <$f<$ρ= ρ<$fi <$ρ <$f+<$ρ= f+<$ρ。[4]我们有（P）+= WlpP。分别取H，P）为ρ，f，我们结束了例4.2考虑规划P，令VH={ 0， 1} × { 0， 1}，VL={ 0， 1}。如果h h，则l：=h+h<$P）：nh1，h2，ln n → nh1，h2，ln n1212 13 14 15 16 17 18 19P=⎨⎧⟨h1,h2,1⟩→{⟨h1,h2⟩}×VLelsel：=h1−h2+1;WlpP：h1，h2，ll →l= 1公共输出l总是1，因此P是安全的，如以下计算所示。给定VH×{l} ∈ H，我们可以证明对于<$P）的B-完备性成立：H（P）（VH× {l}））=H（VH× {1}）=VH× { 1} =H（H1，h2，1<$）=H（P）（H1，h2，1<$））WlpP的F-完备性也成立H（WlpP（VH× {1}））=H（VH× VL）=VH× VL=WlpP（VH× {1}）H（WlpP（VH× {l/= 1}））=H（H）=H=WlpP（VH× {l/= 1}）52A. Banerjee等人理论计算机科学电子笔记173（2007）4712L5完整性和已宣布的NI（DNI）当一个程序P满足由φ表示的无干扰性时，它是什么？考虑任意两个状态为s1，s2∈n的游程。假设s1=Ls2。设sH和sH表示秘密1 2s1，s2中的值被φ去分类，并假设在P的两次运行中，未分类的值不暴露，即φ（sH）=φ（sH）。然后1 2P满足由φ表示的无干扰性，条件是<$P）（s1）=L<$P）（s2）。形式上：s1=Ls2<$φ（sH）=φ（sH）<$P）（s1）=L<$P）（s2）注意，通过设置φ（sH）=T=φ（sH），可以获得普通的不干涉1 25.1建模非分类上一节的讨论并没有激发我们为什么需要WlpP这就是我们在去阶级化的背景下所要做的。考虑秘密h1，h2∈ {0， 1}，并且去分类策略策略释放了h1和h2之间的关系，但没有def他们的确切价值。程序P=l：=h1+h2满足策略吗？这里，VH={ 0， 1} × { 0， 1}，并且解类器φ被定义为：φ（）=φ;φ{ 0， 0}=φ{ 0， 1} =φ{ 1， 0} ={ 0，0，0， 1， 1， 0}（即，我们将所有具有相同非经典性质的元素集合在一起），并且φ{1，1}= VH; φ（X）=x∈X（φ（{x}））.遵守上述策略的程序不应在公共输出中暴露输入0， 0、0， 1和1， 0之间 但允许暴露分区块{{0， 0}，{0， 1}，{ 1， 1}}和任何对之间的区别，因为策略支持后一种区别P是否暴露了它不应该暴露的区别？为了回答这个问题，我们考虑WlpP（l=a），其中a是某个通用输出值。为什么WLP？因为这样我们就可以静态地模拟攻击者为获得秘密信息的初始值（或初始关系）而进行的分析为什么l=a？ 因为这给了我们最一般的Wlp，输出值上的参数。def现在，注意WlpP（l=a）=（h1+h2=a）;令Ha=（h1+h2=a）。因为defa∈ {0， 1}，我们有H0=（h1+h2= 0）.这允许攻击者求解h1，h2：h1= 0，h2 = 0. 因此，当l= 0时，在分区块中的区别{000，0}{0， 0， 0， 1，1， 0}被暴露。因此，该方案不符合政策。所以，考虑一个去分类的保密政策，并在以下模型中对去分类进行建模：通过抽象φ，私人输入的形成，收集到-将所有具有相同属性的元素聚集在一起，由策略取消分类。 设Hφ：H（φ）→H（φ）为相应的抽象函数。 相应地，设X∈N（N）是一个具体的状态集，设XL是X的L切片。 考虑def任意l∈XL. 定义集HL={h ∈ VH|l∈ X};即，给定一个l，H包含所有与X中的l相关的H值。然后是与X相对应的Hφ（X）定义为Hφ（X）=L∈XLφ（HL）×{l}。注意，对于普通无干扰，域H是Hφ的实例化，其中φA. Banerjee等人理论计算机科学电子笔记173（2007）4753将任何集合映射到T。 等式（2）Hφ<$WlpP<$H=WlpP<$H（4）证明了（Hφ，H）对WlpP是F-完全的.例如，对于程序P，F-完全性失败。当X=10， 0， 0时，我们有H（X）=VH× { 0}和WlpP（H（X））={0， 0， 0}。但Hφ（WlpP（H（X）={<$0，0， 0 <$，<$0， 1， 0<$，<$1， 0， 0<$}<$WlpP（H（X））.我们现在可以通过下面的定理5.1将Hφ连接到NI：唯一的警告是φ必须划分输入抽象域，即，你好φ（x）={y|φ（x）= φ（y）}。划分背后的直觉是，φ定理5.1考虑一个分割φ。则P满足无干扰性，由φ i <$Hφ（P）<$Hφ= H φ（P）表示。与定理4.1一起，我们得到推论5.2考虑一个划分φ。则P满足非干扰性，可通过φ i <$H φ <$WlpP<$H =Wlp P<$H来降低，即，（Hφ，H）对Wlp P是F-完全的.推论中的等式断言，Wlp所释放的东西，除了φ已经释放的东西之外，再没有什么了。如果F-完全性不成立，但（Hφ，H）仅仅是可靠的，则Hφ<$WlpP<$H±WlpP<$H。在这种情况下，Wlp（即，RHS）释放的信息（在技术上：更具体）比未分类的信息（即，LHS）。我们的目标不仅是检查一个程序是否满足特定的保密政策，而且要找到可能违反保密政策的公共观察，以及每个公开观察所揭示的相关秘密例如，考虑下面的程序[7]，其中l，h∈Nats。defP=while（h >0）do（h：=h− 1;l：=h）endw如果我们在输出处观察到l= 0，那么我们对输入h所能说的就是h≥0。 但是通过输出观察l/= 0，我们可以推断出输入中的h= 0：循环一定没有被执行。由于Wlp将观察到的（公开的）输出与私人（秘密的）输入相关联，因此，从最终的观察中，我们可以通过以下方式导出该观察所释放的确切秘密：（a）计算wlpwrt。每个观测获得关于输入状态的最一般的谓词（b）检查wlp所描述的状态是否不允许私人投入的区别超过政策允许的范围如果是这样，就没有违约。例5.3考虑下面的代码[22]defP=h：=hmod2;ifh= 0then（h：=0;l：=0）else（h：= 1;l：= 1）;令VH=Nats=VL。假设我们想解密这个测试，h= 0。然后φ（{0}）={ 0}和φ（{h}）=Natsz{ 0}。 因此{h|H0}，{ 0}是分区由φ在VH上诱导，我们得到Hφ={λ，T}<${{h|h = 0}× VL}<${{0}× VL}。54A. Banerjee等人理论计算机科学电子笔记173（2007）47设Had=efVH×{a}。请将此文档的最新版本写入Wlp（l=a），其中a∈ VL。{（a=0hmod 2 = 0）（a=1hmod 2 = 1）}h：=hmod 2;{（a= 0h = 0）（a=1h= 1）}if（h=0）then（h：=0;l：=0）else（h：= 1;l：= 1）{l=a}因此，Wlp将输出状态集H0映射到输入状态{H1，H2，H3，H4，H5，H6，H7，H8，H9，H10，H|hmod 2 = 0，l∈VL}.但是这个状态并不比状态更抽象，{h|h/= 0}× VL，用Hφ表示：它区分，例如，（8， 1）从（7， 1）-保单不允许的区别。实际上，考虑两次P的运行，h的初始值为8和7，l的初始值为1;φ（8）=φ（7）;但我们得到了l的两个不同的输出值。def例5.4考虑P=if（h≥k）then（h：=h-k;l：=l+k）else skip[22]，及其Wlp语义。 考虑H甲乙丙d=ef{h，l，k|h∈VH，l=a，k=b}. Supose取消分类策略是T，即，什么都不需要释放。{（h≥b<$l=a−b<$k=b）<$（h b<$l=a<$k=b）}if（h≥k）then（h：=h−k;l：=l+k）else skip{l=ak=b}WlpP：Ha，b<$→{\displaystyle\mathbb {a}，a−b，b}}|h≥b} ∪ {h，a，b|h（C）和f：<$（C）−→<$（C），如果X<$f（Y）或X<$f（Y）=<$，则元素X∈<$f对于f关于Y∈ <$是稳定的;否则X是不稳定的。根据稳定性对完备性的理解保证了，如果一个抽象域不完备，那么至少存在两个不稳定的元素。在我们的上下文中，f是Wlp;我们想要检查稳定性的元素是由去类器φ诱导的VH划分中的一组私有输入;以及我们检查稳定性的元素（Y在定义中）是特定的输出观察（例如，l=a）。命题5.6 H φ的不稳定元提供了φ的反例。[4]我们把对“几乎没有”的概率分析留爱丽丝Hid：r;d;c∈{0，1};m鲍勃m0;m1;r0;r1可见：m0;m1;r0;r1;f0;f1;e c;m;f0;f1;e;d;rA. Banerjee等人理论计算机科学电子笔记173（2007）4757定义⎢⎣我的律师。Supposethhatl∈VLsuchat（thein tatttesdescribedy）Wlp（HL）∈/Hφ。当x∈Wlp（HL），且h∈φ（xH）时，x∈L∈/Wlp（H1）.Notethatφ（xH）×{xL}<$Wlp（HL）=/其中，φ（xH）×{xL}/φWlp（HL）∈ φ（xH）× {xL}，xL∈φ（xH）×{xL}，xL∈/Wlp（HL）. 因此，平衡作用域Hφ是不稳定的。 为了找到一个反例，考虑h1∈ φ（xH）z {k|{k，xL<$∈ Wlp（HL）}和h2∈ {k| {k，xL∈ Wlp（HL）}. 后一个集合由wlp针对输出观测l获得，因此其任何元素，例如，h2，导致观察L，而集合之外的所有元素，例如，h1，不能导致l。Q例5.7考虑下面的程序，h 我们可以def计算WlpPwrt。 l = a∈ Z，且Ha={\displaystyle\alpha\，l\alpha}|h∈VH，l = a}.{（h= 0<$l =a）<$（h >0<$a = 0）}while（h >0）do（h：=h− 1;l：=h）endw{l=a}⎧⎨H0› →{⟨h,l⟩|h>0， l∈VL} <${<$0，0 <$}Wlp： Ha→ {因此，Wlp（H0）=（VH×{0}）<${H，l<$}| h> 0，l/= 0}。因此，所有l = 0的输入状态都不是去分类策略的反例。相反，对于输入l/= 0的任何两个游程，只要h1= 0且h2∈Evensz{0}，我们就观察到不同的输出。因此，我们可以区分比去分类划分{Evens，Odds}更多的东西。下面的例子[16]表明，这种方法提供了一种对应于放松不干涉的不干涉的弱化。这两种方法都提供了一种方法来表征所显示的信息和必须去分类的信息，事实上，它们都给出了相同的结果，因为它们是由特定的输出观察（参数）驱动的。然而，让我们强调，基于抽象解释的方法也允许从观察到的公共输出中独立地导出最大信息。例5.8考虑程序P[16]，sec，x，y：H，in，out：L，其中hash是一个函数：x：=hash（sec）;y：=xmod 264;P=ify=inthenout：= 1elseout：=0;z：=xmod 3;58A. Banerjee等人理论计算机科学电子笔记173（2007）47考虑其Wlp语义，其中out，in和z分别是a，b，c∈ Z：{（a= 1，out =a，hash（sec）mod264 =b，hash（sec）mod3 =c）（a= 0，out =a，hash（sec）mod264x：=hash（sec）;y：=xmod 264;b，hash（sec）mod3 =c）}{（a= 1，out =a，y=b，xmod3 =c）<$（a= 0，out =a，y/=b，xmod3=c）}ify=inthenout：= 1elseout：=0;{out=a，in=b，xmod3 =c}z：=xmod 3;{out=a，in=b，z=c}让我们首先考虑P，而不考虑z的最后一个赋值，并考虑域由集合Hdef64和Hdefin，1={1sec，in，out，x，y}|in = hash（sec）mod 264，out= 1}in，0 ={1sec，in，out，x，y}|在hash（sec）mod2，out= 0}。 一组所有这些域体现了去分类策略，因为它将所有元组收集在一起，使得SEC对于散列（SEC）mod264具有相同的值。在这一点上，请注意，WlpP语义进行以下关联：Wlp：Hin，a›→Hin，a，这清楚地意味着域是完整的，即，取消分类政策是足以保护该计划。让我们现在考虑最后一个赋值，然后我们有一个变量，我们重新定义H，a为也包含z但对z没有任何条件的元组集合，因为它不在去分类策略中考虑。在这种情况下，Wlp语义执行以下关联：⎧⎪⎨Hin,1›→Hin,1∩，⟨sec，in，out，x，y，z⟩. hash（sec）mod3=z，Wlp：⎪⎩ Hin，0<$→Hin，0<$，1秒，进，出，x，y，z，hash（sec）mod 3 =z，添加到域中的新元素在私有变量sec上还有一个条件，它可以通过观察公共输出来进一步区分私有输入这使得最初的取消分类政策不令人满意。5.3完善保密政策前面描述的方法的自然使用是用于保密策略的语义驱动的细化。我们的想法是从一个保密策略开始，说明什么可以用抽象域（或等价关系）来发布在极端的情况下，该政策可以规定任何关于私人信息的内容都不得发布。A. Banerjee等人理论计算机科学电子笔记173（2007）4759推论5.2的一个结果是，只要Hφ对于WlpP不是前向完备的，那么释放的信息就比去分类φ所允许的要多。因此60A. Banerjee等人理论计算机科学电子笔记173（2007）47私有域为πL=X∈Hφ πL（X）;（d）令π=L∈VLL由φ在私有域上引起的划分必须由完成过程来细化为了得到细化的策略φJ，我们执行以下步骤：考虑定义域HφJ，由Hφ的完备化得到;（b）对于每个Y∈ HφJ计算集合，πL（Y），在一个固定的公共值l∈ VL上是参数的，其中：π（Y）d=ef{h∈VH|（c）对于一个ch l，把partitin，π，inducedondefJdefLπ。 的declassi fica-操作策略，φJ，现在可以定义为φ的细化，R（φ），通过计算对应于π[14]的划分闭包，即， 选言补全，形成分区的集合：φJdef=R（φ）=（π）。例如，在例5.4中，每个输出观测k=b都导致划分πb={{h|h≥b}，{h|h< b}}，这是单次观测所释放的信息。如果我们考虑所有可能观测的集合，那么我们得到π=bπb=id，即我们有φ=id。命题5.9让φ对被分解的信息建模。如果Hφ<$WlpP<$H<$WlpP <$H，则R（φ）<$φ，即，R（φ）是φ的一个加细，它最接近φ5例5.10考虑程序P[22]，其中VH=VL=Z及其Wlp语义defP=h1：= h1; h2：= h1;... hn：= h1; avg：=解密（（h1 + h2 +. +hn）/n）{h1=a}h1：=h1;h2：=h1;.. . hn：=h1;<$iX<$$> →<$if<$a∈VL. XHa{（h1+h2+.. . +hn）/n=a}Wlp：。 i。hi∈Z平均值：=（h1 + h2 +.+hn）/n{avg=a}Ha›→H2，.，hn，a好吧avg=a其中Hdef={h，...，h ，平均值|H∈ Z，（h+ h +... +H）/n=avg=a∈ Z}。什么...a1n i1 2n假设输入去分类策略释放私有值的平均值，即，定义J J J Jφ（φh1，.，hn nn）={nh1，.，hn|（h1 +.. . + hn）/n =（h1 +.. . +hn）/n};策略列-选择所有可能的私有输入，平均值相同因此，平均值是这种状态划分允许观察的唯一属性。显然，该计划释放更多。 考虑n = 4，hi∈ {1，.，8}，且X= H4。 Hφ（X）在avg = 4的态上诱导的分离为{φ 5，2，3，6，4 <$，1，7，3，1，5，4<$，. . . }。但WlpP（H4）={14，3，7，2，4 1，14，8，3，1，4 1，. . }。因此，我们需要重新定义原...最终策略，完成Hφ（X）wrt. WlpP：我们对所有a∈ Z添加元素WlpP（Ha）。φJ在每个这样的元素中，h1具有特定的值a。形式上，域H（X），包含所有的集合{h1，h2，...，hn，平均值|h1 = avg = a，ni > 1。hi∈ Z}; HφJ（X）区分所有在第一个私有输入中不同的元组，其中φJ是作为计算分区的析取完成获得的，并对h1的值进行declassi。⎪LA. Banerjee等人理论计算机科学电子笔记173（2007）4761[5]在理论上，这个细化也可以计算为策略φ和未分类策略T的细化之间的交集。这两种方法之间的效率比较留给我们工作的实现阶段。62A. Banerjee等人理论计算机科学电子笔记173（2007）47⎢这是最接近φ的域，因为如果我们在所得域中添加任何其他元素，我们将区分更多的东西，即，大于h1值的差异。实际上，仍然抽象元素的平均值，我们可以添加具有相同平均值的其他元组集合，但是我们可以添加的唯一元组（即，尚未在域中的元组）必须添加一些新的区别。例如，如果我们添加像{104，6，1，5，4}，{104，6，3，3，4}，... . }，其中h2也是固定的，那么我们也允许区分h2的值，它不是由程序释放的。5.4抽象的不干涉政策所描述的用于检查和完善安全策略的方法是基于公共观察的参数，但是可以对属性执行相同的过程。如果存在关于程序执行上下文的一些信息，那么我们可以限制（抽象）可能的观察结果。这些限制可以建模为抽象域，因此通过抽象的不干涉政策。特别是，已经证明[10]，我们对公共信息观察得越多，私人信息可以保密的就越少。这意味着，如果我们考虑对公共输出的较弱观测，则在一般上下文中不安全的安全策略可以变得安全。例如，考虑下面的程序P，它有两个私有输入x，y和两个公共输出xL，yL。d、dx、dy是常数公共输入，其中dx> d且dy> d：如果（d≤x+y≤d+dx+dy<$−dy≤x−y≤dx），则def如果（x≥0<$x≤d）则xL：=d;如果（x> d<$x≤dx）则xL：=x;如果（x> d <$x≤d+ d）则x：=d;P=x x L x⎢如果（y≥0），则yL：=d;如果（y>d≠y≤dy）则yL：=y;如果（y>dy≠y≤dy+d）则yL：=dy;我们可能希望跟踪属性，而不是具体的输入和输出，例如，一个特定的变量位于什么区间。上图以图形形式表示程序的输入和输出：程序将输入属性，即八边形（在私有变量x，y中，由±x±y≤c形式的约束集表示）转换为输出属性，即矩形（在变量x，y中，由± x ± y ≤c形式的xL，yL）：因此，如果我们取WlpPwrt。区间属性-⎢A. Banerjee等人理论计算机科学电子笔记173（2007）4763η˜˜˜˜抽象域[18]，即，我们推导出两个私有输入之间的八边形关系。因此，安全策略必须至少解密八角形域，以使程序安全。此外，为了使算法可计算，抽象的不干扰策略可能是有用的。事实上，通过抽象公共域，我们可以使攻击者的可能观察数量有限;在实践中，这意味着当我们计算Wlp（ρ（l）=A）时，只要抽象域是有限的，我们就可以保证将有无限多的Wlp计算。这个例子表明，我们可以结合（狭义）抽象不干涉def[9]在下面的完备性方程中进行了非经典化：设Hρ= λX。VH×Lφdef defJ Jρ（XHη= λX.φ（Hη（L））×η（l），其中Hη（L）={h|η（l）= η（l），l∈ X}Hφ<$WlpP<$Hρ=WlpP <$Hρ6抽象模型检验与信息流在前面的部分中，我们已经看到了如何验证和改进允许某些私人信息泄漏的保密策略。整个研究是通过考虑I/O语义（指称和wlp）和建模DNI作为一个完整性问题。另一方面，在抽象模型检验（AMC）框架中存在的完备性和稳定性（在Paige-Tarjan意义上）之间的强关系已经被研究[20，11]：所讨论的完备性是由状态域上的等价关系诱导的后函数的B-完备性由于指称语义是一个过渡系统的职位，其中所有的痕迹是两个状态长因此，两条迹是L不可区分的，即，=L，如果它们具有相同的公共投影。定理6.1设|P|给出了P（deterministic program）的标准跟踪语义。迹线上的不干扰，即， σ1，σ2∈|P |σ 1 = L|P|（σ2），保持i H postP H = H postP，其中postP是与过渡系统建模P相关联的后函数。这个定理意味着，当我们必须保护整个迹语义不受恶意观察时，我们也可以表征状态的私有信息此外，完备性方程（通过定理4.1改写为H<$pre<$H=pre<$ H）断言（在AMC的上下文中）不存在虚假的反例。在国家情报局的情况下，这意味着没有信息泄露。特别是，对于解密，如果Hφ=prePH成立，则不需要通过细化进一步解密私人信息，即使如果我们假设攻击者可以观察到计算的每一个中间步骤在下面的简单示例中，我们通过提供它与Zdancewic和Myers [28]定义的等价关系Transformer的关系来展示这种方法是如何工作的，以表征私人信息的泄漏首先，我们重写64A. Banerjee等人理论计算机科学电子笔记173（2007）47Transformer如下：设σ i是一个等价关系，我们定义σ1S（σ i）σ2当且仅当σi >0。[posti（[σ1]）]= [posti（[σ2]）]。（posti是post与自身i次的合成。）这个新的等价关系，如果与X不同，有东西被释放了。通过我们的方法，我们可以准确地描述释放的内容。当我们处理等价关系时，post的向
我的内容管理
展开
