动态信息流控制的新方向：广义多方面及其优化和终止敏感版本

跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂731动态信息流控制的一个更好的方面明娥法国INRIAminh.ngo @ inria.frTamaraRezkINRIA，法国tamara.rezk@inria.frNataliiaBielovaINRIA，法国nataliia.bielova@inria.fr亚历杭德罗·鲁索查尔姆斯理工大学瑞典russo@chalmers.se科马克·弗拉纳根UCSC，美国cormac@ucsc.edu托马斯·施密茨UCSC，美国tschmitz@ucsc.edu摘要Multiple Facets（MF）是一种动态的实施机制，它被证明是实现JavaScript信息流安全的一个很好的选择它依赖于多次执行程序，每个安全级别或视图执行一次，以实现可靠性。 通过查看程序内部，MF对视图进行编码，以减少所需的多次执行次数。在这项工作中，我们在三个方向上扩展多个方面首先，我们提出了一个新版本的MF任意格，称为广义多方面，或GMF。 GMF严格推广MF，这是最初提出的一个特定的格的校长。其次，我们提出了一个新的优化GMF，进一步减少了执行的数量第三，我们提出了一个终止敏感的版本，消除了隐蔽通道，由于termina-tion，加强了多方面提供的安全guar-antees。ACM参考格式：Minh Ngo ， Nataliia Bielova ， Cormac Flanagan ， Tamara Rezk ，Alejandro Russo，and Thomas Schmitz.2018年。动态信息流控制的一个更好的方面 在WWW '18伴侣：2018年网络会议伴侣，2018年4月23日至27日，法国里昂。ACM，New York，NY，USA，9页。https：//doi.org/10.1145/3184558.31863481介绍JavaScript已经成为Web事实上的编程语言Web浏览器每天执行数千行JavaScript代码，这些代码通常可以访问机密信息，例如标记Web会话中的用户已通过身份验证的cookie。JavaScript成为攻击的常见目标并不奇怪虽然浏览器以访问控制的形式部署安全措施（例如，SOP和CSP），它们不足以[12，17，30]保护数据的机密性。信息流控制（IFC）是一种很有前途的技术，它提供了一种系统的解决方案来处理无意或恶意的机密信息泄漏。最近，动态IFC分析受到了很多关注[1-3，5，7，9，10，14，26，33]，部分原因是它适用于JavaScript，而静态分析是相当尴尬的[29]。本文在知识共享署名4.0国际（CC BY 4.0）许可下发布。作者保留在其个人和公司网站上以适当的归属方式传播作品的权利WWW©2018 IW3C2（国际万维网会议委员会），在知识共享CC BY 4.0许可下发布。ACM ISBN 978-1-4503-5640-4/18/04。https://doi.org/10.1145/3184558.3186348为了扩展，适合Web的IFC技术不仅需要是动态的，而且还需要将对现有JavaScript代码的修改减少到最鉴于此，满足这两个要求的有趣的动态IFC技术包括执行程序的几个副本：每个安全级别或视图执行一次。以这种方式，程序（视图）的每个副本仅取决于可观察到对应安全级别的信息，其中因此不可能有泄漏安全多执行（SME）[14]和多方面（MF）[3]是基于这个想法的两种技术。这两种技术已被证明是一个很好的适合信息流的安全在网络上，因为他们已经成功地实现了Firefox浏览器的扩展[13，33]。虽然SME和MF都基于多执行，但它们存在重要差异[7]。一方面，SME是黑盒[24]，即，它是一种不查看程序内部而是改变输入和输出的语义以确保安全性的机制。暂时，我们假设安全级别只是主体集合的场景（例如，web源），其表示对数据具有保密性关注的那些机构 在这样的场景中，SME需要为任何可能的主体集合生成一个执行，其中执行的数量相对于主体的数量呈指数级增长！相反，MF [3]旨在减少SME的多执行次数和内存占用。它通过检查程序代码和多执行指令以及仅在需要时多路复用存储器来实现这一点。虽然MF比SME更加资源友好，但当涉及到通过异常终止的泄漏时，SME提供了更强的安全保证[7]。我们的主要目标是提高效率的技术基础上MF和中小企业的一般情况下。特别是，我们发现MF有时可能比SME产生更多的多执行-当考虑MF的目的时，这是违反直觉的（请参见第2节）。我们的第一个贡献包括一种新的技术，以进一步减少多执行（和内存占用）的MF的数量。我们的第二个贡献是将MF推广到任意有限格（见第3节），而不是像最初的建议[ 3 ]那样仅限于主体的安全格。例如，当一个程序依赖于5个安全级别时，这就变得很有用。在这种情况下，如最初所述，MF将需要通过使用（至少）3个主体（2 3> 5）来对它们进行编码，并且因此执行程序2 3 = 8次，而SME将仅执行它5次（每个安全级别一次）。最后，我们将MF和SME组合成单个新的动态IFC机制，以便提供与SME一样强大的安全保证（即，终端敏感跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂732（⊙）（⊙）（）（）⊕̸⊑−（）（）（）（）⟨⟩（）[›→]（）（）（）（）（）下一页⊤对于一个程序h=l µ（l）⊤⊤⟨⟩⟨⊤⟩⊤（）（）[›→ ›→]（）（）（）（）斯克伊普（skip，µ）µAssI gnv=µ（e）（x：=e，µ）µ[x›→v]SME-TINI（P，H（µ））µ1（P，L（µ））µ2如果μ（e）=v（Pv，μ）μ′（ifethenPttelsePff，µ）µ′seQ（P1，µ）µ′（P2，µ′）µ′′（P1;P2，µ）µ′′（P，µ）SME−T I NIµ1⊙µ2其中⊙将两个正常存储器组合成SME存储器，什么（如果e然后P;而e做Pelseskip，µ）µ′（whileedoP，µ）µ′图1：语言语义这样，H µ1µ2=µ1，L µ1µ2=µ2。SME机制将盲目地执行程序，尽可能多地存在视图（或阵列的位置考虑程序h：= l，其中变量l和h的初始视图由下式给出：µh= 1：0和µ l= 1：1。在SME中，使用SME-TINI规则，分配将被执行两次：一次是H（µ）=[h›→1，l›→ 1]用于高视图，另一次是H（µ）=[ h ›→ 1，l›→ 1 ]用于高视图。非干扰），同时尽可能避免多执行，因为我们的MF优化版本允许它。所有的证据都可以在[23]中找到。2中小企业和小额信贷在本节中，我们将讨论MF中的基础机制如何一方面减少与SME相比的执行次数，另一方面由于基于主体的安全网格，可能会比SME运行更多的多执行。我们在这里的目标部分是教学，部分是为了激励和提供第4节中提出的优化的直觉。语言和语义为了研究多方面的基础，我们使用一个简单的，确定性的while语言。 它的语法包括程序P、变量x、表达式e和值v。我们将符号用于二元表达式运算符。值可以是整数值或布尔值。（节目）P：：=skip|x：=e|如果e则P1否则P2|而e做P |P1; P2（表达式）e：：= v|X|埃埃图1展示了该语言的标准大步语义存储器µ将变量映射为值;我们重载存储器的符号，并使用µ e作为存储器µ中表达式e的求值函数，其中µ v = v且µ e1 e2 = µ e1µ e2. 我们写P，µ µ′表示程序P在内存µ上的求值以内存µ’终止。 我们使用µ x v作为内存µ ′其中，如果y ≠ x，则μ ′ y = μ y;如果y= x，则μ ′ y = v。MF可以使用比SMESME [14]多执行程序更少的资源，以黑盒方式，与网格中的安全级别 让我们将SME内存定义为一个函数，该函数将每个变量映射到一个值数组，每个安全级别一个值。 为了简单起见，让我们首先考虑仅具有两个元素H和L的安全格，其中H L是唯一被禁止的流。因此，SME内存μ将变量映射到2个（可能不同）值的数组：一个对应于H视图，一个对应于L视图。让我们将这样的值数组表示为v1：v2，其中v1是私有视图H，v2是公共视图L。假设H（resp.L µ（）是标准语义中的记忆体，通过µ（）的投影获得，将变量映射到高视图的单个值（分别为低视图）。然后，用于这样的语言的SME监视规则1可以由如下的关系SME T I N I给出：1我们在这里给出SME的终端不敏感版本其中Lµ=h 0，l 1用于低视图。在执行之后，最终SME存储器将h映射到1：1。减少执行次数的一种方式是利用变量l的高视图和低视图相等的知识Hµl=L µl。由于语义是确定性的，因此不需要执行程序两次。 我们可以通过在命令的粒度上专门化SME来使用此知识，并包括以下分配规则：SME-optI mH（µ）（e）=L（µ）（e）（x：=e，L（µ））µ（x：=e，µ）SMEµ[x›→ µ（x），µ（x）]请注意，此SME优化需要查看程序的内部形状，以评估赋值的表达式e是否满足假设。一般来说，为了使用SME-TINI的多执行技术减少执行的数目，足以（i）在SME存储器中识别值阵列中的哪些值相等及（ii）记住哪些值对应于哪些视图。MF使用多执行技术，实现了（i）和（ii），因此减少了执行次数。 MF将SME存储器（具有与晶格元素一样多的位置的阵列）中的值编码为有序二叉树，其中顺序由晶格的元素给出。例如，对于SME存储器，其中对于具有顶部元素的4个元素的晶格，μµh= 1：0：0：0，等效MF存储器将该阵列编码为？1：0，意味着1是视图，0是其余视图。每个依赖于该值的执行将执行两次，而不是像SME中那样执行4次。此外，MF还使用由编码提供的视图信息，以便在分支命令的情况下更少地执行。例如，对于具有SME存储器的SME-TINI，µ（h）=1：0：0：0>程序：1：如果h=0，则2：h：=h+1执行4次（其中第2行的赋值执行3次）。使用MF存储器编码µh =？1：0，MF记住在第2行，视图没有可能的观察（因为对于视图，h的值是1，所以它因此，赋值h：= h +1只在h为0的内存中执行一次（变量h的视图对应于3个不是的级别）。：，其中在SME中Φ是1：1，MF仅保留值1：单个值表示所有视图都可以观察到相同值的事实。因此赋值h：=l执行一次(and也将减少依赖于h的所有未来执行跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂733B2⟨⟩⟨ ⟩∈L（）下一页（）下一页⟨⟩⊥⊤∉∀ ∉⊑（≤）（≤）\⊖（（））（9{∈| }关于我们99⟨ ⟩ ⟨⟩L（）下一页（）下一页因此，当编码SME内存可以有效地减少，多个执行是典型的相应地减少如B1B3所示以下章节，保存-MF存储器编码方法通过执行需要：简单值或多面值。分面值的形式为l？其中，l是安全级别，并且Vi可以是分面值或简单值。第一刻面V1的l？V1：V2被称为私有的，并且对于在网格中的安全级别1或更高级别处的观察者可见;第二方面V2被称为公共的，并且对于比1更低或不可比的安全级别可见。我们使用V作为分面值或简单值的元变量。每将值的数组表示为称为分面值的树，并对图2：格点LB，在转基因食品中的评价（见图6）标有一组安全级别pc，当前的计算是可见的。根据分面值评估表达式。特别地，关于分面值的表达式的评估的定义高度依赖于表达式的形状及其根据不同视图的值，并且因此与监视器的黑盒属性相矛盾。MF可以比SME运行更多的多执行。原始MF在SME方面有一个限制：它仅被设计用于主体的安全格：对于n个主体，这样的格包括3.1表达式计算用pcewe表示e值-H分面式表达式e的表示存储器µ，具有一组安全级别埃尔斯角pce的定义是M1M2示于图四、比如说，考虑x的求值，当保持2n个安全级别。以下广告交换平台[35]示例表明，MF在以下方面可能不如SME有效内存μ中的分面值x为L实践中，当安全网格不是基于主体时。实施例2.1. 广告交换平台需要在发布商的网站上投放广告。为此，它实现了一个实时我？我？V1：V2。为了定义在给定pc的情况下哪个方面是有用的，我们考虑以下情况：图3：晶格L竞价（RTB）系统[36]，广告商可以在发布商的网站上该系统接收来自投标人的所有投标报价作为输入，并对它们进行排序。根据RTB算法，第二好的报价获胜。我们在图中给出了这个例子的5个元素的晶格二、 为了简单起见，我们只考虑3个投标人，称为B1，B2和B3，一个广告交换（级别），它能够看到所有的出价，和一个公共视图。因为MF是针对主晶格设计的，所以为了编码5安全级别，它使用3个主体k1、k2和k3，并创建一个格pc中的所有水平都大于或等于l，表示为l”pc（即l’pc）。l l’）：评估可以使用私有方面V1，因为公共方面V2无论如何都不适用于该pc中的每个级别。pc中的所有水平都低于或不能与1相比，表示为1 l ′ pc.l l ′）：评估只能使用公共分面V2，因为V2是对任何低于或不能与l相比的视图可见的分面。• 否则，我们说l和pc不可比较，并表示8= 23级，因此有可能运行它通过L PC（即，l ′，l ′′ ∈ pc. l l ′ ∧ l l ′′）：我们首先评估程序执行8次，而SME总是执行程序5次。我们考虑一个测试，天真地检查出价的- fers的顺序，并决定赢家。点阵的编码是：{k1，k2，k3}，B1 ={k1}，并且1：winner：= 0;第二章： 测试：=x1x2和x2x3;3：如果测试，则获胜者：=2，否则跳过投标人的出价值为x1=其他方面Gpc（e）= V1：V2∠pc1={l′∈pc|ll′}V1⊕pcViflpc2=pc\pc1µ1=µ（y›→V1）µ2=µ（y›→V2）是吗Vpc1V ：Vpc2V否则Gif-SG Gˆpc其中pc1={l′∈pc|ll′}和pc2=pc\pc1。图4：表达式求值GWhI le（ifethenP;whileedoPelseskip，µ）↓pcµ′（whileedoP，µ）↓pcµ′µ↑def（x）=μ（x）如果Γ（x）=glb（L），（x）？否则为μ（x）：def（x）>。其中，µ 1l µ 2（x）=[l？1（x）：图6：任意安全网格联系我们|Γ（x）=l（μ）（x）当rel=Γ（x）图5：分面记忆和普通记忆的函数使用对M1可见的公共方面。并在公共方面中添加默认值（由def函数定义）在一个特殊的情况下，当x的级别是格子中的最小级别时，我们只保留一个对所有安全级别可见的简单值µ x然后我们用构造的分面记忆来评估程序pcpcpcpc且pc=L。由此产生的分面内存被转换回µ（x+y）=µ（x）+ µ（y）通过使用预处理功能生成正常备忘录|Γ。=pc（M1？10：0∠）+pcpc（∠M2？5：0）skip，sequence和while循环的语义规则是直接的-10PC？五比零？10个5：10{M}0for rwa rd. GAssign规则使用分面ede赋值µpc（e）定义=+ ∠M2=+1第3.1节。=M2？15：103.2语义我们滥用符号并使用l作为简单值、分面值和分面记忆的投影函数。对于任何V，I V返回V中的值，其对于级别I处的用户可见。对于任何μ，l μ返回μ中的内存，该内存对级别l的用户可见。在描述if指令的语义之前，我们首先定义了几个辅助函数。设dom μ是µ的定义域，y是一个新变量，即ygdom）.我们用yV表示一个新的mem y yyy，使得domyy=domyyy，μy=V且对于所有xdomµ，µ′x=µx。通过y，我们从的域中移动y，也就是说，y构造了一个新的memory′，其中域′ =domy，且对所有x≠y，μx=μ′x。考虑if指令的求值ifethenP1elseP2l（v）=v l（∠l1？V1：V2）=l（μ）（x）=l（μ（x））l（V1）如果l1l，l（V2），否则。与PC。如果e被评估为常数值（tt或ff），则仅评估Ptt或Pff（参见规则GIf-C）。当e被评估为一个分面值l？V1：V2，我们构造一个new programifythenP1elseP2，其中y是新变量。从投影函数l用于定义将分面存储器转换为简单存储器的函数（见图1）。（五）。GMF的语义定义在图1中6作为大步评估关系ΓP，μGMFμ’，其中程序P在存储器μ和安全环境Γ中执行，该安全环境Γ将变量映射到给定安全网格中的安全级别。主要规则GMF首先从以下构造分面存储器使用图1中的转换µdef的标准存储器5，其中GLB是的最大下界。结果分面存储器将每个变量x的原始值保持在私有方面中，vpcV2ifl“l？V1：V2pcV=）>。跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂735⊗\{∈| }9和\不是空的。在本例中，我们运行新的引理3.1，我们有l pc，因此pc1 ={l ′ ∈ pc |l l ′}pc2=pc pc1编程ifythenP1elseP2两次：一次具有比1“更高的视图”，即，其中pc1=1′pc1 1′，并且y被设置为私有面V1，并且另一次具有比1“更低或不可比较的视图”，即，其中pc2=pc1，并且y被设置为公共面V2。然后，我们使用l运算符组合所得到的记忆。分面存储器的组合基于以下事实：当在GIf-S规则中将pc拆分成pc1和pc2时，pc1中的所有级别都大于或等于1，并且pc2中的所有级别都小于或不可比于1。跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂736（）--L⟨l?[V1]：[V2]>其他人也是。⊑⟨ ⟨ ⟩ ⟩ ⟨⟩转→⊙→→→ [（）]L9（）↑2（）\\（）下一页{}（›→）{}（›→）G[[]][v]=v[V]如果V1=V2，[l？V11：V22∠]elseifl1l，ll2，V1= ∠l1？V11：V12∠，按照GMF规则，程序的求值条件为pc==H，M1，M2，L.对于赋值指令，x的值被更新为µpcx1>x2=M1？H？H？ tt：ff：tt。其余的在示例3.4中描述了评估，并且得到的分面[l？V1：V2]=V2=x2的程序图P。假设Γ（x1）=M1，Γ（x2）=H，Γ（z）=H，μ（x1）= 10，μ（x2）= 5，则x1和x的默认值分别为100和20 2。设µ=μdef。它遵循μ（x1）=M1？ 10：100∠且μ（x2）=∠H？ 五点二十分。Γ1：x：=x1>x22：如果x，则z：=10，否则z：=52选择x1和x2的值和默认值，使得赋值指令求值后x的值其中列表S是来自集合S的安全级别的列表，使得如果l出现在列表S中的l’之 前 ，则l l’。 如果一个给定的安全格中的关系不是全序，我们可以将它转化为全序T，只要它是有限的偏序。然后我们可以将列表S看作一个列表，使得对于这个列表中的任何l和l′，如果l出现在l′之前，则l′Tl。FV1，V2，pc1，pc2的定义使用以下运算符基于安全性的有序列表创建分面值（P，µ↑Γ ）↓OdefL ′Γ（P，μ）OGMFμ′|Γ跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂738‖l（V2）如果L=l，l∈pc2，（1）（）下一页{}{}（∪）⊤ ⊥⟨L ⊑⟩{}（1）（1）（1）①（1）（1）（）下一页联系我们联系我们9（）9 ∠（）∠（）下一页（）下一页•（）下一页（）（）（）⊥̸⊑{}（）⊑ ⊥{}() ⊥ ()LO？：′′glb′被简化为（）下一页水平L，两个分面值，pc1和pc2：l(V1) ifL=l,l∈pc1,L，V1，V2，pc1，pc2 l（V1）：﹥T，V1，V2，pc1，pc2﹥﹥新分面值中存在的所有级别也存在于PC中。因此，我们的例子中减少的分面值是？v：L（V′），{，L}.最后，如果上述条件都不成立，那么我们递归地减少小平面，其中V′是一个简单值或一个分面值3。=∠B1？0：∠B2？0：∠B3？2：2，{B2，B3，}==∠B1？0：∠B2？0：∠B3？2：2，{B3，}= B1？0：∠B2？0：2实施例4.5（0GMF比GMF更资源友好 反函数V，pc在图1B中定义。9.第九条。如果V的形式l？v：v′∠，则优化是直接的。现在我们考虑V的形式为二、从例4.1开始。 为了显示OGMF的优化，我们用pc ={，B1，B2，B3，}和µ进行评估，其中µ（x1）=B1？ 10：0，μ（x2）=B2？ 5：0>，且μ（x3）=>B3？ 7：0。如果分面值V的形式为？v：∠B？v：V′（for-在执行第2行处的指令之后，分面存储器100被配置为执行第2行处的指令。马利报和 v=v’），则可以简化为1第一个B1 vV，pc）isµ′=µ[winner›→0，test›→V]，wheee1、2、3个（formally，¢l′？v′：V′，pc′）），其中pc′=pc\{}。′⟨ ⟨⟩⟩V=∠B？B？ff：ff ∠：∠B2？ff：∠B？tt：tt ﹥。如果分面值V的形式为B1？v：B2？v：V′，（l和l是不可比的，并且v=v′），并且此外对于我们考虑if指令的执行对于水平pc1={B3，}，测试的e赋值为tt：B3（µpc（test））=（µpc（test））=对于B1或B2可见的pc，可以保证它们观察到