依赖性核心演算在计算lambda演算和分布式系统中的应用

理论计算机科学电子笔记172（2007）5-31www.elsevier.com/locate/entcs一个核心依赖马蒂恩·阿巴迪加州大学圣克鲁兹分校计算机科学系硅谷微软研究院摘要依赖性核心演算（英语：Dependency Core Calculus，DCC）是计算lambda演算的扩展，其设计目的是为了捕捉在信息流控制、部分求值和其他编程语言设置中出现的依赖性概念。 我们表明，出乎意料的是，DCC也可以用作分布式系统中的访问控制演算。从这个角度开始研究DCC，我们探索了它的一些吸引人的属性。关键词：授权，类型1介绍依赖核心演算（DCC）[3]是Moggi的计算lambda演算[ 22 ]的一个小扩展DCC的设计目的是为了捕捉在信息流控制、部分评估、呼叫跟踪和其他编程语言设置中出现的常见的中心依赖概念。介绍DCC的论文包括从基于类型的依赖分析到DCC的六种翻译正如那里所解释的，在描述依赖性时使用计算lambda演算有点令人惊讶。通常，计算lambda演算描述了带有副作用的语言[22]，或者形成了向纯函数式语言添加副作用（如I/O）的基础[14]。相反，依赖性分析不会从根本上改变计算的值。尽管如此，在计算lambda演算的两种用途下都有一个共同的想法。在Haskell的情况下，没有办法使用I/O类型构造函数计算值并将该值传递给非I/O类型的表达式。类似地，在信息流系统中，对“if-then-else”中的高安全性布尔值1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.0026M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5条件返回高安全性值。在这两种情况下，计算lambda演算的类型规则强制执行必要的限制。在本文中，我们表明，也出乎意料的是，DCC可以用作分布式系统中的访问控制演算。在本申请中，DCC施加的限制意味着没有办法取得当事人A已经作出陈述s的证据，并将其非平凡地用作无关当事人B已经作出陈述t的证据。访问控制基本上包括确定发出请求的主体是否相应地，访问控制的逻辑支持对主体、其请求和其他语句的推理[4，16，19，9，6]。(See[1]以进一步讨论其中的几个逻辑和其他参考。通常，逻辑包括诸如Asayss的公式，其中A表示princi-pal，s表示语句（请求，授权或其他话语），并且says是运算符。said的使用从认证和授权的细节中抽象出来。我们可以说，即使A没有说，A也说直接说出S。 例如，当A是一个用户，它的一个程序包括s时，在消息中，陈述A说s可能是方便和适当的。在这种情况下，A说s意味着A已经导致s被说，s已经代表ADCC可以被看作是访问控制的那些先前逻辑的核心的替代方案DCC承诺在这方面的一些吸引人的功能：简单的规则与有用的后果，一个精确的语义，和良好的基本属性。• 这些规则暗示了这个公理基本上断言，对于两个主体A和B，如果A说B代表A说话，那么B确实代表A说话。它通常被视为一个附加组件，而不是更基本的规则或语义定义的结果其次，这些规则还意味着，如果s为真，那么对于每个主体A和陈述s，A说s。这种推断可能是可取的，但它可能会产生意想不到的结论，如A说s→（s（A说sJ））对于所有s和sJ[1]。在这里，这些结论是由使用的重复推理。(Garg和Pfenning[11]在不同的形式系统的背景下发现了构造性的这种好处;见第2节。当然，建设性是有代价的，而且很难激励。为什么人们要放弃排中律呢？例如，主体A说“删除文件”或没有说“删除文件”，这不是真的吗？DCC在某种意义上解决了这个难题。它不是用来推理经典真理的，而是作为证据的类型系统，因此，它是建构性的不应该太令人惊讶，因为一个人并不总是有证据证明一个命题或其否定。• 语义学是理论对微积分的解释M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）57（与模态逻辑的经典可能世界语义相反[4]）。语义学并不直接解释诸如责任和权威之类的概念，至少在目前的形式上是这样。在语义学中，一个陈述的意义可以被粗略地看作是一组可以导致陈述结论的论证这些论点可能代表数字证书和其他种类的证据，用逻辑推理拼凑在一起• 基本性质包括一些传统上证明类型系统。特别是，可以制定各种一致性，类型健全性，参数化，和非干扰的结果。这些结果有时会有新的形式和新的应用。例如，探索不干涉，我们证明了一个定理（定理7.6），限制了一个主体对其他主体的陈述的可能的不干涉。DCC的一些性质已经在以前的工作中考虑过[3，27]。虽然我们不试图全面发展的元理论的DCC，我们提出了一些简单的，但重要的证明理论的结果。虽然这些功能可能不是DCC独有的，但我们认为DCC提供了一个相当有吸引力的软件包，值得研究。此外，DCC不是纯粹为了推理访问控制而发明的特别演算，这似乎既除了具体的技术成果之外，本文的主要贡献是重新考虑DCC作为访问控制系统，更广泛地说，在访问控制中使用Curry-Howard同构（Curry-Howard同构似乎还没有在这种情况下被利用，它似乎有很大的潜力。在整个过程中，我们专注于DCC的规则及其解释。我们留下几个机会，进一步工作的扩展和相关的理论。下一节（第2节）讨论了这项工作的一些来源第3节回顾了DCC，特别是定义了一个我们称之为简单类型DCC的系统。这是DCC的终止片段，因为它以前被定义过，只有符号的表面变化。第4节考虑如何使用简单类型的DCC进行访问控制。更进一步，第5节以Girard的System F [ 13，7 ]的风格添加了多态类型第6节展示了这种扩展如何实现对“代言”关系的新处理第七节是关于多态DCC的元理论。第8节介绍了一个有吸引力的多态DCC片段第9节最后简要讨论了DCC的前景。本文是一篇会议论文的修订版[2]。2相关工作当然，这项工作的主要来源包括关于访问控制演算和DCC的原始论文（例如，[1，3]）。通过DCC和计算lambda演算，这项工作也与大量关于编程语言和逻辑的研究有关（例如，[24，10]）。8M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5另一个重要的和更直接的在这方面的工作是一个有见地的建议，从Langworthy[18]和一个有趣的手稿由Garg和Pfenning [11]。在那份手稿中，他们开发了一种新的访问控制逻辑。这种逻辑是先前逻辑的直觉主义变体，具有明显令人愉快的证明理论。它让人想起信息流类型的系统，我们发现它与DCC有相似之处（Garg和Pfenning并不知道）。另一方面，与DCC不同的是，这种逻辑并没有被定义为编程语言的类型系统。此外，它缺乏与手操作属性的DCC，正如我们在这里使用的那样，并不像它最初定义的那样。从技术上讲，这些变化是重要的，但例行的。具体地说，我们去掉了非终止程序和相应的“指向类型”的概念;非终止在通用类型系统中很有吸引力，但在证明系统中并不常见。另一方面，我们以系统F的风格引入类型量化。这种类型的量化使我们能够对“代言”关系进行建模最后，我们改变符号，例如写A表示s而不是Tl（s），用A代替l。奇怪的是，这种表面的语法变化可能被认为是比删除非终止程序和添加类型量化更深刻的影响3简单类型的DCC在本节中，我们定义了简单类型的DCC，并指出如何用逻辑术语阅读它。3.1微积分Simply Typed DCC与标准计算lambda演算有三个区别[22]。首先，Simply TypedDCC包括sum类型。第二，不是让一个类型构造函数T与一个monad语义关联，演算合并了多个类型构造函数T A（这里写的A表示... . ），对格L的每个元素A∈ L都有一个.（Wadler [28]也考虑了这个想法。 在我们使用这个格时，L的元素将表示主体，较小的元素表示更可信的主体，较大的元素表示不太可信的主体。三是一元操作3.1.1类型简单类型DCC的类型由语法给出s：：= true|（s）|（s）|（s→s）|A说S其中A是格L的元素的范围，具有偏序±。因此，我们从原始的DCC符号出发：我们写• true而不是unit，• s1=s2而不是s1+s2，M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）59表1Simply Typed DCC：Typing Rules.[Var] Γ，x：s，ΓJx：s[Unit] Γ（）：true[林][对]r，x：s1，e：s2r（λx：s1. e）：（s1→s2）Γ e1：s1Γe2：s2Γe1，e2：（s1s2）[应用程序]Γe：（s1→s2）ΓeJ：s1Γ（e eJ）：s2e：（s1[项目1]项目（proj1e）：s1Γ►e:s1[进样1]（注射1e）：（s1s2）e：（s1[项目2]Γ（proj2e）：s2Γ►e:s2[注射2]Γ► (inj2e) : (s1∨s2)re：（s1s2）r，x：s1e1：sr，x：s2e2：s[案例]（inj1（x）的情况e）。e1|注射2（X）。e2）：s中文（简体）[单位M][绑定]Γ（ηA e）：A表示sre：Asayssr，x：seJ：t在eJ：t中，r_n约束x=et被保护在A• s1×s2，而不是s1×s2，• A表示s而不是TA（s）。对于每个A∈ L，says操作导出一个类型子集，称为在级别A保护的类型：• 如果A±B，则B表示s在A级受到保护;• true在A级保护;• 如果s和t在A级被保护，则（st）在A级被保护;• 如果t在A级受保护，则B表示t在A级受保护;以及• 如果t在A级被保护，则（s→t）在A级被保护。(Tse和Zdancewic [27]已经提出了这个定义的推广，这在将来可能会有所帮助。说10M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5true在A级受保护的子句来自它们。）M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5113.1.2方面Simply Typed DCC的术语和类型规则见表1。这些规则用于证明形式为Γe：s的类型判断（读作这里，类型化环境Γ表示具有类型的不同变量的列表。单位、函数、乘积和和类型的规则都是标准的，一元单位运算的规则也是如此。一元绑定操作的规则是非标准的，它对绑定表达式体使用了“protected at level A“的概念3.1.3语义介绍DCC的论文为Simply Typed演算提供了操作语义和指称语义（包括这里没有考虑的构造，特别是术语递归）。操作语义是按名称调用的语义。项（ηA e）简化为e，并且（bindx=eineJ）简化为eJ[e/x]，其中e[eJ/x]表示eJ对e中x的无捕获替换的结果。Simply Typed DCC的其余操作语义是标准的。这种操作语义与类型系统并不完全一致。特别地，项（ηA e）简化为e，尽管这两项具有不同的类型，项（bindx=eineJ）简化为eJ[e/x]，尽管e和x不具有相同的类型。然而，这种差异是有限的。（约简保留了第7节函数（·）F的模应用类型。）一个alter- native操作语义[27]更适合类型系统。在这个语义中，除了lambda演算的标准规则外，我们还得到了eJ中的bindx=（ηA e）简化为eJ[e/x]。Zdancewic最近使用Bidelf证明工具检查了这种语义的进展和主语归约属性[31]。对于我们目前的目的，任何一种操作语义都是令人满意的。Simply Typed DCC的指称语义更加复杂。 我们在这里省略它。然而，它可能是有用的，在进一步的工作，特别是因为它捕获的非干涉性质。3.2逻辑阅读我们在表2中以逻辑形式重申了简单类型DCC的规则。在这里，环境Γ表示类型的列表。我们只是省略了所有的术语。这种从类型系统到逻辑的转变是Curry-Howard同构的一个实例。为了清楚起见，我们在表2中显示了结果规则根据这些规则，如果类型t在A级受到保护，那么t和A说t在逻辑上是等价的。因此，直到逻辑等价，在A级保护的类型是那些形式为Asaystfor somet的类型。我们把s写成s，并说s是一个定理，当s可由表2的规则导出时。等式，s是一个定理，当存在一个项e使得等式e：s可由表1的规则导出时。在这种情况下，我们说e存在于s中，并且e表示s的一个证明。12M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5表2简单输入DCC：逻辑阅读。[Var] Γ，s， Γjs[Unit] ΓtrueΓ，s1<$s2[林]Γπ（s1→s2）联系我们[对]Γ► (s1∧s2)Γ► (s1∧s2)[项目1]第一章第一章[进样1]Γ► (s1∨s2)（s1→s2）[应用程序]第二章Γ► (s1∧s2)[项目2]第二章第二章[注射2]Γ► (s1∨s2)Γ（s1<$s2）Γ，s1<$sΓ，s2<$s[案例]Γ ►s[单位M]Γ ►sA说，ΓAsayssΓ，st[绑定]伊特t被保护在A在实践中，这个证明可以作为访问资源的请求中的s的证据来传输[30，5]。为此，用附加的类型信息来修饰术语可能是有用的，这样验证就可以像可能特别地，这样的类型信息可能有助于向后应用规则[BindM]-对于当前形式的规则，我们必须猜测A和s，以便找出产生结论的假设。我们抵制这种诱惑和其他诱惑，修改语言的证明，以尽量减少对DCC的变化，并强调其令人惊讶的适用性访问控制。Simply Typed DCC具有每个类型都被占用的属性，因此Simply Typed DCC可能不会被视为非常有用的逻辑。幸运的是，用表示基本命题的原子类型来丰富SimplyTyped DCC是很容易的;这些原子类型在应用程序中很方便，而且它们提供了无人居住的类型。不过，为了尽量减少与DCC最初定义的偏差，并且因为多态DCC包括可以表示基本命题的类型变量（见第5节），我们在这里不介绍它们。M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5134简单类型DCC接下来，我们建议如何使用Simply Typed DCC进行访问控制。我们从一个基本的，一般性的讨论使用逻辑访问控制，然后集中在简单类型的DCC的一些功能。4.1基础知识在访问控制的逻辑方法中，决定是否应该授予操作的问题例如，逻辑公式s可以表示应当执行特定操作o在这种情况下，s可以写成Do（o）（或Ok（o）[29]）形式的命题负责为o做出访问控制决策的引用监视器可以具有特定主体A被授权执行o的策略。该策略可以由以下公式表示（A说Do（o））→Do（o）类似地，来自主体B的对操作o的请求可以由以下公式表示：B说Do（o）引用监视器可能会尝试证明这两个公式隐含Do（o），如果成功，则授予访问权限一般来说，证明可以利用A和B之间的关系以及参考监视器已知的其他事实。或者，参考监控器可以简单地检查B提供的证明。因此，当证明是DCC项时，引用监视器可以简单地进行类型检查。4.2says属性在Simply Typed DCC中，运算符、和→遵循标准的直觉命题规则。另外我们有► s→A表示s带证明项和λx：s。（ηA x）J J► （A说（s→s））→（（A说s）→（A说s））带证明项J J J JJλx：A表示（s→s）。在λy中绑定x = x：A表示s。bindy=yin（ηA（x y））这些定理对应的主要公理和规则，通过在以前的calculi（尽管切换到直觉推理）。因此，我们有足够的时间来执行关于访问控制的许多典型的、基本的推理14M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5事实上，定理s→A说s甚至比我们通常拥有的更强通常，我们只有模态逻辑中的必然性规则，它只说如果s，那么s是s。必然性规则避免了在经典逻辑语境中s→A说s的意外后果[1]。定理“s→Asayss”表明Asayss并不意味着A实际上说出了s或暗示了它的东西，相反，我们应该从负责做出访问控制决策的引用监视器的角度来看待所有推理。非正式地说，我们有A说s，当参考监控器相信的陈述与A贡献的陈述相结合时，参考监控器可以得出s的结论。因此，引用监控器的参与是隐式的您因前述► （A说A说s）→（A说s）带证明项λx：A说A说S。绑定y=xiny（参见[4]第3.4节，以及►（A说B说S）→（B说A说S）带证明项λx：A说B说S。bindy=xin bindz=yin（ηB（ηA z））这些性质有时会简化关于话语链的推理：它们意味着，当A1说A2... 说An说S主体A1，.. .，An以及它们在链中出现的频率并不重要。在这方面，saying很像旨在保证数据完整性的系统中的污染：污染的顺序和它们发生的频率通常不会影响结果的完整性级别。然而，交换性性质（AsaysBsayss）→（BsaysAsayss）并不是我们方法的核心，在第8节中我们将展示如何省略它。4.3使用偏序及其与“代言”的联系在我们的DCC应用程序中，级别网格中最小的元素代表最受信任的主体，较大的元素代表不太受信任的主体，如第3节所示。相反的顺序通常用于获得信息流类型系统的安全保证，特别是DCC（例如，[3]）。目前的排序在模型中是相当普遍的完整性。这种巧合应该是意料之中的，因为可靠的访问控制需要请求和策略的完整性.我们有以下定理：► （A说s）→（B说s），对于A±BM. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）515因此，我们可以把±看作是“speaks for”关系的表征。事实上，通过这种解读，我们得到，如果A代表B说话，A说s，那么对于每一个s，B都说s。这一性质是“代言”关系的特征然而，Simply Typed DCC并不是一个丰富的推理“代言”关系的设置。特别是，我们不能在诸如A说（B±A）这样的表达式中使用符号±：这个表达式甚至不是句法上合法的公式。 一个可能的解决方案可能是扩展语法，使（B±A）是一个类型，从而将±内部化。虽然这种方法可能是可行的，但它有点临时性。下面我们将开发一种更有原则的方法，它依赖于多态性。4.4使用Meets和Joins组合主体和组格结构还提供了算子H和H，分别是格L的交算子和连接算子。由于AHB±A和AHB±B，我们得到：(1)（AHBsayss）→（Asayss）每一个S然而，反过来并不是对每个s都自动成立。1直觉上，AHB可能比A和B更值得信赖，即使A和B碰巧意见一致。在这个意义上，声明的联合签名可能比同一声明的两个单独签名更有分量同样，由于A±AHB和B±AHB，我们得到：(2)（A说s）对于每个s，但不是相反。直觉上，AHB可能比单独的A和B中的每一个更不可信。因为说在逻辑推论下是封闭的，所以AHB的陈述可以从A和B的单独陈述中导出，其结果是A和B都不会单独产生的。这些性质表明我们可以把格元解释为群，H解释为群交，H解释为群并，±解释为群包含。因此，格L的单个元素可能不（总是）对应于原子主体，而是对应于一组主体。因此，AHB的陈述可能比A和B的陈述更可信，这似乎是相当合理的。例如，安全策略可能涉及两个群体，“ 俱 乐 部 成 员 ” 和 “ 成 年 人 ” ， 并需 要 成 年 俱 乐 部 成 员 的 某 种 授 权 ; 成 年 俱 乐 部 成 员 的 声 明 不 能 被 任意 俱 乐 部 成 员 和 任 意 成 年 人 的 相 同 声 明 所 取 代 。可替代地，格L可以是抽象安全级别的格，其类型可以用于多级安全（例如，[8，12]）。在这样的格中，（1）和（2）的逆可能具有强的、可疑的结果。例如，让我们考虑一个五元素晶格，它有一个底部，一个顶部，以及三个彼此无关的元素A，B和C在这个晶格中，AHB是底部元素，AHB[1]更确切地说，一旦我们引入基本命题，就不能导出逆命题，例如，以类型变量的形式。只要每一种类型都有人居住，当然可以推导出相反的结果，但不是出于有趣的原因。类似的注意事项适用于第4节其余部分对其他一些公式的讨论。16M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5表3多态DCC：附加的类型规则。Γ，Xe：s[TLAM]Γ（Λ X.（e）：SΓ► e：∀X. S[TApp]r（et）：s[t/X]（t在Γ中良构）表4多态DCC：附加类型规则的逻辑形式。Γ ►s[TLAM]X. SX. S（X在Γ中不是自由的）[TApp]rs[t/X]是顶部元素，因此AHB±C±AHB。如果A说s，B说s暗示了AHB说s，那么它也会得出C说s。同样，如果AHBsayss暗示Asayss或Bsayss，那么Csayss也会暗示Asayss或Bsayss。在许多这样的场景中，特别是当L是群的格时，格L是分配的。一般来说，格L不需要是分配的，但增加这个条件并不矛盾; DCC的规则不变地适用。4.5关于主词尽管存在重要的差异，但操作符H和H可能会让人想起过去应用于主体的操作符和我们可以将这些操作符作为缩写引入：A说B说S代表（A说S）说（B说S）A说B说S代表（A说S）说（B说S）虽然这些缩写是方便的，但值得注意的是，AB和AB不需要完全像晶格元素一样表现。例如，不应想当然地认为，（AB说（s→sJ））→（（ABsayss）→（ABsayssJ））对每个s和SJ成立：当A说s，B说（s→SJ），我们有A→B说sA→B说（s→sJ），但不一定是A说sJ或B说sJ。M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5174.6附加操作更进一步，我们可以在格子上添加其他缩写和其他运算符，以表示有用的复合主体。在先前的工作中已经探索了这样的扩展（例如，[4，16]）。在那里，接线员|（“引用”）起着核心作用，因此我们在本节中简要地重新讨论它。我们留下进一步的工作更系统的研究额外的运营商。当A和B是两个主体时，A|B是代表A引用B的主体。A的一个基本性质|B（有时被视为其定义）是A的等价物|B说s，A说B说s，对每一个s。在简单类型DCC的上下文中，4.2节中列出的say的性质暗示了运算符的强公理|.具体来说，我们可以采取|是结合的、交换的和幂等的。此外，定理J► （A说s）→（A说s）对于A±A(see第4.3节）表明，|在第一个参数中关于±可以是单调的，并且在第二个参数中也可以是交换性的。它遵循（A）|B）±（（A H B）|（A H B））=（A H B）相反，对于所有s，如果A说s或B说s，则A|B说S。因此，令（AHB）±（A|B），因为人们可能认为AHB是说A或B所说的一切的最小的原则。这一属性需要对Simply Typed DCC进行实质性的强化，因为它意味着（AHB）sayss→AsaysBsayss这种强化可以通过放松类型系统来实现，以这样一种方式，A说B说s在AHB级受到保护。总之，在Simply Typed DCC的上下文中，很容易将引号运算符等同于|连接操作符H。虽然这个等式看起来是合理的，并且避免了为|，它可能会导致简单类型DCC的重大变化。5多态DCC我们以System F的方式对DCC进行了多态性扩展。我们依赖于System F，因为它的简洁和强大;像往常一样，人们也可以考虑更多限制形式的多态性。这个扩展解决了4.3节中描述的缺点：在第6节中，我们展示了我们可以使用多态来表示和推理当然，我们也可以以其他方式使用多态性。特别是，我们考虑如何使用多态性编码说。多态类型的一个常见的实际批评是，它们在类型推理中引入了我们注意到，这种批评并不适用于J18M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5本申请。多态类型的另一个实际批评是，它们可能很难编写和理解。这种批评是适用的。我们不建议使用许多量化器编写安全策略。在实践中，安全策略通常可以用一些习惯用法来编写，这些习惯用法的定义可能依赖于量化器，但没有明确的量化器。 在这个方向上，探索用于编写安全策略的语言的开发是很有吸引力的，也许是逻辑编程风格（如SD3 [15]，Binder [9]和RT [20]）。5.1微积分对多态DCC的扩展只依赖于多态的标准规则我们在本节中回顾这些规则。5.1.1类型对于多态性，DCC的类型由语法给出s：：= true|（s）|（s）|（s→s）|A说S|X|第十章S其中，A的范围是格L的元素，X的范围是一组类型变量。变量X被绑定在XNUMX中。s，并可重命名。同样，says操作会导出一个类型子集，称为A级保护的类型。我们在第3.1.1节的定义中增加一条：• 如果测试在A级保护，则为X。t被保护在A级。这个简单的从句的动机是直接类比“”和“”。5.1.2方面表3中列出了多态DCC的附加术语形式和附加类型规则。这些是对表1的补充。这里，类型化环境Γ表示列表，其中每个元素是不同类型变量或具有类型的不同变量。我们要求，如果变量的类型提到了类型变量X，那么X出现在更左边。 因此，例如，x：X和x：X，X不是格式良好的类型化环境，而X，x：X和X，Y，x：X，y：A说（X→Y）是格式良好的类型化环境。在规则[TApp]中，我们要求t是Γ中的良构类型。这个条件意味着t中的任何类型变量都应该在Γ中声明。同样在规则[TApp]中，表达式s[t/X]表示在s中用t替换X的无捕获替换的结果。5.1.3语义沿着标准线（例如，[21]）。ZdancewicM. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）519一也适用于此扩展扩展指称语义有点更具挑战性。我们把这个扩展留给进一步的工作。5.2逻辑阅读在3.2节中概述的简单类型DCC的逻辑阅读，可以推广到多态DCC。表4以逻辑形式给出了附加规则。这里，类型化环境Γ表示类型的列表;类型变量可以在这些类型中自由出现。我们只是省略了所有的术语，以及类型变量的声明。例如，键入环境X，Y，x：Y→X，y：A表示Y产生的环境和打字判断Y→X，A说YX，Y，x：Y→X，y：A说Y在（η（xyJ））中绑定yJ=y：A说X收益率Y→X，A说Y，A说X在这样的判断中，没有量化的类型变量可以被读取并用作基本命题。在表4的规则[TLam]中，我们明确指出X不应该在Γ中自由出现。在表3中，相应的要求是由以下事实暗示的：Γ，X是一个格式良好的类型化环境。和3.2节一样，我们写了s，并说s是一个定理，当s可由表2和表4的规则导出时。等式，s是一个定理，当有一个类型变量列表X1，.，Xn和项e，使得X1，.，Xn=e：s可由表1和表3的规则导出。特别是，我们立即获得：►（A说是X。 s）→（λX. A说s）带证明项λx：（A表示λX。 s）。 Λ X。 bind y = x in（η A（yX））而不是相反的含义--这可能是无害的，但我们似乎并不需要。5.3将访问控制转换为参数化Tse和Zdancewic [27]已经展示了简单类型化DCC到系统F中的编码。至关重要的是，他们将一种形式A表示s映射到αA→s，其中αA20M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5是一个独特的类型变量。其他DCC结构的翻译大多很简单。Tse和Zdancewic并不涉及非终止性和相关概念，幸运的是，我们目前的目的并不需要这些概念似乎有可能将它们的编码扩展到多态DCC。最终的结果将是一个纯粹在系统F中的访问控制的内部表示。我们把对这种表示的研究留到进一步的工作中去。可能需要比Tse和Zdancewic的那些定理更大的定理来证明他们的技术的这种使用。特别是，虽然它们的编码是类型保持的，但在System F中的键入比在DCC中更自由，并且人们希望确保System F的可扩展性不会产生访问控制的意外结果此外，虽然编码到系统F中可以提供有用的指导和语义，但用系统F取代DCC还为时过早。在这一点上，在DCC中推理访问控制似乎比在System F中更方便不像系统F，简单类型的DCC提供了一个简单的符号和设置，在其中研究逻辑问题，开发示例和应用程序，并尝试替代概念和规则。虽然多态DCC包括了系统F的所有复杂性，但从我们的角度来看，它仍然具有简单类型DCC的许多优点，特别是因为我们在这个初步探索中只有限地、有纪律地使用量化器。6多态DCC继续第4节，在本节中，我们建议如何使用多态DCC进行访问控制。6.1“Speaks我们通过多态性来编码“代言”。为了与以前的论文保持一致，我们将“A为B说话”写为然而，在这里，我们写AB作为一个焦点，第十章（A说X→B说X）我们立即得到“代言”关系的一个基本性质► （AB）→（（A说s）→（B说s））对于每个s，有证明项λx：A≤B。XS值得注意的是，我们还得到了“手-o-公理”作为定理（而不是作为附加公理）：► （A说（B<$A））→（B<$A）这个定理可以推导出来，因为定义意味着BA在A级受到保护。它的证明是术语：λx：A表示（B<$A）。绑定y=xinyM. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）521显然，A±B意味着A<$B：► A B代表A±B然而，反过来则不成立：A<$B并不意味着A±B。 事实上，我们甚至可以有A<$B和B<$A，而A和B是不同的晶格能级。 在这方面，逻辑在底层晶格和底层晶格之间保持一定的分离。“代言”关系的偏序。这种分离是一种特征还是一种不幸的冗余可能会引起争论。它似乎没有明显的缺点，它的优点是允许我们在有一个“代言”关系之前开发简单类型的演算它还允许使用格运算H和H，否则将难以定义。然而，在第8节中，我们考虑了一个不需要主体格的多态DCC片段“代言”的限制，类似于以前考虑的限制（例如，[17]可以很容易地定义和研究。特别地，给定一个带有自由类型变量X的类型C（X），我们可以这样写第十章（C（X）→A说X→B说X）为了表示A在满足C（X）的陈述X上代表B说话。例如，当C（X）对于某些s是s→X时，这种类型意味着A在s的后果上代表B说话。6.2示例使用“代言”的编码，我们勾勒出一些使用的小例子多形态DCC用于访问控制。对于这些示例，为了方便起见，我们假设标准数据类型（如int）以及授权的基本命题。我们还推测对DCC进行更实质性的扩展由于DCC是一种编程语言，因此考虑在语言级别将传统编程与基于DCC的访问控制集成的方法是有吸引力的。这些例子部分是为了建议在这个方向上的研究途径。更进一步，考虑基于DCC的访问控制与用于编程语言的信息流系统（例如，[23，25，26]），特别是因为DCC可以捕获信息流的概念。6.2.1使用简单的Hand-o工具我们的第一个例子相当基本。它可以在各种其他逻辑中重现，一旦适当的实例22M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5∧假设我们有以下公式：(3)A说（BA）B说做（o）（A说Do（o））→Do（o）第一个代表从A到B的手。和4. 1节一样，第二个公式表示B的权威支持的语句Do（o）结合这些公式，我们可以导出Do（o）。形式上，我们有：⎛A说（BA）⎜⎜⎜⎜► ⎜⎞⎟⎟⎟⎟→Do（o）B说Do（o）⎜ ⎟⎜ ⎟⎜ ⎟⎝ ⎠（A说Do（o））→Do（o）与4.1节一样，结论Do（o）的意思是操作o应该被允许。我们假设第6节的其余部分使用公式（3），因为我们是在这个例子的基础上建立的6.2.2证明携带呼叫接下来，我们考虑为操作o定义安全感知接口的情况。此接口应反映o例如，如果o需要一个整数参数并产生一个整数结果，那么o的类型可能是：Do（o）→（int →int）其中我们明确了要求Do（o）。因此，当一个主体C- vokeso时，它应该通过Do（o）的证明。为此，我们期望调用者C将获得并组合公式B说Do（o）、（A说Do（o））→Do（o）和A说（B<$A）的证明。如果我们采用这样一个合理的原则，即一个可以用主体的公钥检验的数字签名的语句构成了主体说了这个语句的证明，那么A说（BA）和B说Do（o）的证明 （AsaysDo（o））→Do（o）的证明可以由下式导出：o上信任的权威机构的数字签名声明。我们将标准DCC和数字签名世界之间的接口细节留给进一步的工作。从根本上说，这个例子需要将命题视为类型，将证明视为语言级表达式。因此，尽管它很简单，但它似乎超出了其他访问控制逻辑的范围。∧M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5236.2.3校对完成和评估当（AsaysDo（o））→Do（o）表示由o上信任的权威指定的o的访问策略时，引用监视器可能愿意采用此公式，但调用者C可能没有（AsaysDo（o））→Do（o）的证明。 在这种情况下，o的更宽松的类型可能是合适的。类型可能是：或者简单地说：（AsaysDo（o））→Do（o））→Do（o））→（int→int）（A说Do（o））→（int→int）根据这种类型，C应该提供证明，A说做（o）然后，参考监视器可以通过应用（A说Do（o））→Do（o）类似地，在某些情况下，B说Do（o）的证据不能被具体化为一个证明，调用者C可以提出并与其他证明结合例如，当C实际上是B时，调用o的动作可以包括断言Do（o）。引用监视器可能知道B说了什么，但所讨论的证据不是可以传输的位串或表达式。同样，o的更宽松类型可能是合适的。类型可能是：（（B说Do（o））→Do（o））→（int→int）根据这种类型，C应该提供证明，（B说Do（o））→Do（o）然后，参考监视器可以尝试为自己建立Do（o），在这种情况下，通过证明B说Do（o）。 特别地，如果引用监控器已经将调用者认证为B，则引用监控器可以简单地假设B说Do（o）。对于其他调用者，引用监视器在运行时可能无法证明B，即Do（o）。一个更丰富的类型系统可能会表示，如果调用者代表B说话，那么引用监视器保证授予访问权。这样的变化导致这样的想法，即有时应该允许调用者C仅提供Do（o）的不完整证明。不完全证明可以包含指示引用监视器被期望在哪里进行定理证明、咨询其本地策略、或者从C或从其他源请求附加证据的这些命令超出了我们在本文中正式研究的范围;例如，它们可能包括输入、输出和递归。他们不能保证一定会成功。例如，递归可以允许循环推理，并且对输入的请求可能不会被应答。因此，应评估证据，24M. Abadi/Electronic Notes in Theoretical Computer Science 172（2007）5F FF评估过程应该把不完整的证明变成完整的证明。结果系统利用了证明是可以执行的程序的想法，从而进一步利用了Curry-Howard同构。7元理论在本节中，我们开始探索多态DCC的元理论7.1基本结果多态DCC的元理论应该包括传统的一致性、类型可靠性和参数性结果，这些结果在系统F的研究中很常见在本文中，我们开始考虑这些性质，依赖于系统F的元理论。更广泛地说，