信息流类型系统下的安全保护转换研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）75-94www.elsevier.com/locate/entcs一种流敏感到安全保护转换的Agda形式化流量不敏感的安全类型塞西莉亚·曼齐诺1Dep artamentodeCienciasdelaComputaci'on罗萨里奥国立大学阿根廷阿尔贝托·帕尔多2乌拉圭蒙得维的亚大学计算机学院摘要信息流分析是确保数据机密性的一种流行技术。正是在这种背景下，保密政策出现了，以保证私人数据不能通过对公共数据的检查来推断。其中一个策略是不干涉，这是一个语义条件，通过不允许区分两个计算的结果，当它们只在其机密输入中变化时，确保在程序执行期间不存在非法信息流。无干扰的一个显著特征是，它可以通过信息流类型系统的定义静态地实施。 在这些类型系统中，如果程序进行了类型检查，则意味着它满足安全策略。在本文中，我们专注于通过程序翻译的非干涉性的保存。具体地说，我们形式化的证明Hunt和Sands的翻译，转换高级别的，而程序类型在一个低敏感类型系统到等价的高级别程序类型在一个低不敏感类型系统的安全保护我们的形式化是在依赖类型的语言Agda。我们利用Agda类型系统的表达能力在类型级别上对安全类型系统进行编码。我们的形式化的一个特别的方面是，它遵循一个完全内在的方法，我们装饰的类型的抽象语法与安全类型信息，以获得良好类型的表示（即安全）的程序。这种方法的一个好处是，它允许我们在转换关系的类型中直接表达安全保护的属性。在这种方式下，除了固有地表达程序的转换之外，翻译关系还代表了安全保护的归纳证明。关键词：无干扰，信息流类型系统，依赖类型编程，Agda，类型安全1电子邮件地址：ceciliam@fceia.unr.edu.ar2电子邮件：pardo@fing.edu.uyhttps://doi.org/10.1016/j.entcs.2020.08.0051571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。76C. Manzino，A.Pardo/Electronic Notes in Theoretical Computer Science 351（2020）751引言信息流分析是确保数据保密性的一种流行技术。正是在这种背景下，保密政策出现了，以保证私人数据不能通过对公共数据的检查来推断。不干涉[3]是安全策略的一个例子。它是一种语义条件，通过不允许区分两个计算的结果，确保在程序执行期间不存在非法信息流，当它们只在其机密输入中变化时。无干扰的一个显著特征是，它可以通过定义信息流类型系统来静态地实施[2，16，14，8]。因此，当一个程序在这样的类型系统中进行类型检查时，这意味着它满足了安全策略。在这种设置中，程序变量根据它们可以存储的信息类型（例如，公共或机密数据）。根据类型对安全属性进行建模的优点是可以在编译时检查它们，从而部分减少甚至消除了在运行时检查属性的开销大多数安全类型系统都是对数据流不敏感的[14]。这些类型系统中程序变量的安全级别保持不变。这与对带宽敏感的安全类型系统形成对比[4，13]。在这些类型系统中，每个变量在程序的不同点上可以有不同的安全级别。流敏感类型系统比流不敏感类型系统更宽松，因为它们接受更大的安全程序集在本文中，我们专注于通过程序翻译的非干涉性的保存具体地说，我们形式化了Hunt和Sands的翻译[ 4 ]的安全性保护证明我们的形式化是在依赖类型的函数语言Agda[9，1]中进行的。我们利用Agda类型系统的表达能力我们的形式化的一个特殊方面是，它遵循完全内在的方法[10，7，12]，其中我们用安全类型信息装饰抽象语法的类型，以获得良好类型（即安全）程序的表示这些术语同时表示形式类型系统中的AST和（它们相关的）类型规则[15，11]。这种表示的一个有趣的结果是，它限制了可表示的对象语言术语。事实上，并不是每个AST都是可表示的，只有那些根据对象语言的类型系统是良好类型的但更有趣的是这种表示对类型化术语之间的函数的影响：只有保留那些类型不变量的函数才被接受。这个事实的积极方面是它的验证简化为类型检查。本文的结构如下。在第2节中，我们介绍了作为翻译的源和目标的高级语言以及它的对行不敏感的类型系统。第3节讨论了Hunt和Sands定义的语言的对行不敏感的类型系统。第四节给出了程序的转换和证明C. Manzino，A.Pardo/Electronic Notes in Theoretical Computer Science 351（2020）7577J它保留了安全类型。 第五节是论文的结论。完整的Agda代码可在https://www.fceia.unr.edu.ar/~ {}ceciliam/codes/.2类型不敏感性我们首先简要描述作为翻译源和目标的语言。在此之后，我们提出了一个类型系统，强制执行安全的信息流的语言的程序。本节中所示的系统是一个对波纹不敏感的类型系统，对应于用于输入翻译的目标程序。我们决定从描述翻译的端点开始，因为系统更自然，更容易理解。这也是一个适当的背景，在此背景下，我们可以采用内部主义方法来执行《农业发展议程》。除了实现细节上的分歧，本节中要展示的对线程不敏感的类型系统已经在[7]中介绍过了，在那里我们开发了一个Haskell实现的安全保护编译器，也使用了内部主义方法。2.1语言翻译中使用的语言是标准的While语言，其表达式和语句由以下抽象语法定义e：：=不存在|X|e1+ e2S：：= x：= e |skip |S1; S2|如果e则S1否则S2|while e do S其中e∈Exp（表达式），S∈Stm（语句），x∈Var（变量），n∈n（整数文字）。语义是完全标准的。表达式和语句的含义都是相对于状态s∈State=Var→Var给出的，其中包含每个变量的当前值我们假设表达式的语义是由一个评价函数E：Exp→State→Est给出的，这个评价函数是由表达式结构的归纳法定义的。 对于语句，我们定义了一个大步语义，它的转换关系写为S，s，s，J，这意味着在初始状态s中对语句S的求值以最终状态s终止。转换关系的定义如图1所示。注意，为了简单起见，该语言不包含布尔表达式。相反，if或while语句的条件由算术表达式给出，当表达式计算为零时，条件为true，否则为false。78C. Manzino，A.Pardo/Electronic Notes in Theoretical Computer Science 351（2020）75≈x：=e，sS1，sS1;S2，ss sS JE[[e]]s=0sJ如果e，则S1，否则S2，s，则sJE[[e]]s/=0sJ如果e，则S1，否则S2，s，则sJE[[e]]s=0sJwhileedoS，sJsJJ当e做S的时候，E[[e]]s/= 0当你做S的时候，图1. 语句的大步语义2.2安全类型系统假设我们要对一个安全场景建模，其中每个程序变量都关联了一个安全级别，说明它存储的值的保密程度在这种情况下，实现某种安全机制以保护机密数据是很自然的。我们将通过实施一个信息流类型的系统来做到这一点[16，14，8]。本节中定义的类型系统是对线程不敏感的，因为它认为变量的安全级别在程序执行期间保持不变。具有此属性的变量称为固定类型变量.这与所谓的加密类型变量形成对比，加密类型变量的安全级别可能随程序执行而变化。我们将在第3节中介绍的对指针敏感的类型系统中处理指针类型的变量。我们假设一个有界格的安全水平（L，≤）满足（）和连接 （T）操作，以及顶部（T）和底部（T）值。底部的值表示最低安全级别（公共数据），而顶部的值表示最高安全级别（机密数据）。我们还假设晶格在能级之间具有相等关系。表达式llJ表示安全级别l比lJ的可信度低。不干涉是程序的一个属性，它保证在程序执行期间不出现当信息从安全级别较高的变量流向安全级别较低的变量时，就会发生非法泄漏。 当任何安全级别为l的变量的最终值不受变量初始值变化的影响时，程序满足此安全属性更高的安全级别。这个属性可以用程序语义来表示。我们写xl来引用安全级别为l的变量。 让我们说两个状态s和SJ是l-等价的，记为sj=LSJ，当每个状态都与l-等价时，securitylevelthan 1在两个状态下具有相同的值;即， s（xl′）=SJ（xl′）对于每个xl′，其中lJ0：LL<$r{w：=y;z：=x+ 1}r'0'Γ'1=Γ'0'HΓ=Γ[w→N]r>0：NNr'{w：=y}r'N<$Γ'{z：=x+1}Γ'[z <$→H]1Γ“=Γ"”HΓ = Γ[w<$→N] =Γ“1 1 1 1N<$r'1{w：=y;z：=x+ 1}r'1[z<$→H]图4.类型化迭代的示例点态：Γ H Γ J= λx。Γ（x）x。Γ（x）≤ΓJ（x）。半格有一个由环境给出的顶元素，所有变量都是顶安全类型（T）。根据规则ASSIGN，在赋值之后，变量x的类型可以：（i）如果赋值在上下文pc中执行并且被赋值的表达式是类型t，则改变为更高的值pc_t，其中，Γ（x） pc_t，则改变为更低的值;或者（iii）否则保持不变。像往常一样，IF和WHILE的规则旨在防止隐式溢出。（条件的）分支或（while的）主体必须在上下文中是可类型的，该上下文是上下文pc和条件类型t的最小上限。例如，考虑以下安全类型的网格：图4显示了代码的输入迭代步骤：whilex>dow：=y;z：=x+ 1，从环境Γ ={w：L，x：M，y：N，z：H}开始。请注意，在WHILE规则中，后环境是迭代构造的结果，迭代直到获得固定点。循环体重复键入，直到后期环境相对于最后一次迭代没有更改。然后，该规则可以用最小不动点算子来重新表述：W HILE-FIXΓ f= fix（λ r. 设Γe：tpctr {S} r Jin r JH r 0）pc<$r0{whileedoS}rf这个固定点构造保证会终止，因为它是在单调函数（根据类型规则定义）上计算的，并且环境集是有限的这个规则的收敛性证明在[4]中给出，作为下面定理证明的一部分，该定理陈述了类型系统的正确性。我们称AS为计算最小ΓJ的函数，使得pc<$Γ{S} ΓJ。定理3.1（[4]）对于所有的S，pc，Γ，存在唯一的 ΓJ使得pc≠Γ{S} Γ J，并且，相应的函数AS（pc，Γ）<$→ Γ J是单调的。为了在Agda中实现这个类型系统，我们需要定义一个函数来计算WHILE-FIX规则的固定点。 不动点的构造基于以下定理的Agda形式化（定理3.2），84C. Manzino，A.Pardo/Electronic Notes in Theoretical Computer Science 351（2020）75n≤±陈述了在任意偏序集上满足某些要求的任何单调函数的不动点的存在性。在公式化的定理中，我们捕捉到了我们的环境半格所具有的相关特征。考虑到环境是有限映射，只包含分析程序中出现的变量，结果证明半格是有限的。由此，与我们相关的是，半格中的每一个严格升链都有有限长;特别是，每一个终止于顶环境的链。这将通过假设存在一个函数来反映在定理中，该函数称为界，它将自然数与偏序集的每个元素相关联，并且相对于严格顺序严格减少：xиy约束y约束x.bound值背后的直觉是，它表示从元素到top（T）的最长严格递增链的长度 在T处的边界值为当然是零。我们不要求偏序集有一个顶元素，并且在T处的bound的值为零，而是等价地要求bound有一个唯一的极小元素：boundx = 0 boundy = 0 boundx = y。定理3.2设（S，±）是偏序集，x∈S是元素，g：S→S是±上的单调函数，有界：S→ N是关于严格阶（i）的严格减函数，且有唯一极小元.如果存在一个元素x ∈ S使得x ± gx且对某个k有界x ≤ k，则存在n ≤ k使得gx是g的一个不动点。证明证明是通过对k的归纳。• k = 0：假设边界x ≤0，因此边界x = 0。 由于bounds是一个递减函数，且x ±gx，我们有bounds（gx）≤ bounds x。因此，bound（g x）= 0。通过界的极小元的唯一性，我们得出gx = x，因此x是g的不动点。• k= KJ+1：通过假设我们知道界x ≤ KJ+1和x ± gx。那么我们有两种情况：casex=g x：则x是g的不动点。casex<$g x：由于bound是严格递减的，我们有bound（g x）

下载后可阅读完整内容，剩余1页未读，立即下载