通过验证的共享能力模型：seL4微内核的高层访问控制模型

理论计算机科学电子笔记254（2009）25-44www.elsevier.com/locate/entcs一个验证的共享能力模型安德鲁·博伊顿悉尼研究实验室，澳大利亚计算机科学与工程学院，新南威尔士大学，澳大利亚andrew. nicta.com.au摘要本文提出了一个高层访问控制模型的seL4微内核。 我们扩展了早期的形式化Elkaduwe等人的非确定性，明确共享的能力存储，和实体的删除操作。 我们正式证明了这个新模型可以强制执行系统- 全球安全政策以及权威确认。通过在抽象访问控制模型中显式地处理共享，我们大大简化了对seL4实现的细化证明。据我们所知，这是第一个机器检查的访问控制模型，具有显式的权限共享。关键词：共享能力，交互式定理证明1介绍本文提出了对seL4的机器检查，高级安全分析[8]的扩展。 seL4内核[4，6]是L4内核的演化 系列[11]。seL4内核旨在专门支持安全的嵌入式设备。Elkaduwe等人[8]现有的正式访问控制模型基于经典的获取-授予模型[12]，并且部分地从EROS能力模型[16]中获得灵感。seL4安全模型最初的重点是证明关于该模型的安全性定理，这表明它是合适的1NICTA由澳大利亚政府资助，由宽带、通信和数字经济发展局和澳大利亚研究委员会通过信息通信技术卓越中心计划提供资金。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.05826A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）25用于强制执行强制性的系统全局访问控制策略和权限确认。隔离特性已在最近的工作中得到证实[5]。最终目的是展示Elkaduwe等人的模型与seL4内核的C实现之间的关系。这种关系分三个步骤显示。我们的重点是第一：安全模型和抽象操作规范之间的细化，在L4验证项目中定义[3]。该项目旨在展示另外两个步骤：操作规范和可执行规范之间的细化，以及从后者到C实现[10]。我们试图证明访问控制模型和操作规范之间的关系，结果表明，seL4的特征也存在于其他能力系统中，这使得证明特别复杂。按照复杂性的递增顺序，这些特性是：非确定性、删除实体（不仅仅是功能）和共享功能存储。第一种是非决定论，主要是技术性的，容易处理。第二种是实体的定义，概念上很简单，但在安全规范中出现的实体和实现中存在的实体之间引入了不匹配;稍后将给出一个示例。第三，共享能力存储，引入了一个概念问题。此外，如果一个人天真地将经典方法形式化，那么在精化证明中，抽象状态和具体本文的贡献是直接在安全模型中处理所有这些特性，扩展了现有的形式化和安全性证明。特别是• 我们扩展了现有的模型，包括非确定性的准确细化故障条件，• 我们扩展了模型，包括删除实体，这引入了对安全定理假设的改变，• 我们提供了共享能力存储的第一个正式模型和安全分析。共享能力存储改变了分析的基本谓词，并为传输权限和信息引入了额外的可能性。我们展示了如何调整分析以考虑共享权限，并证明了调整后的系统仍然适用。能够强制执行强制性的系统全局访问控制策略以及权限确认和隔离。本文中的所有形式定义和定理都在定理证明器Isabelle/HOL [14]中进行了机器检查。由此产生的安全模型支持一种细化关系，该关系将安全模型中的实体和功能与内核几乎一一A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）2527⇒操作模型中的对象。这使得证券分析稍微困难一些，但它大大减少了显示细化的难度。后者是比安全分析大得多的活动虽然改进证明尚未完成，但已经取得了足够的进展，以暴露操作规范的早期版本中的安全问题：即使在启动时显式检查将权限从线程A转移到另一个线程B的授权操作，也可能发生中断，并且在恢复操作时不进行另一次检查，即使在该中断期间权限可能已经从A撤销。因此，操作的完成将是未经授权的，并且不会细化所有此类操作都是原子的安全模型这个问题在此期间已经得到了解决，并展示了如何使用细化来暴露像这样的细微缺陷。虽然我们的工作是出于对seL4进行改进证明的愿望，但我们相信共享能力存储的模型本身是共享是一种常见的性能优化，在资源受限的设备中可能很重要。我们认为，明确地对待它可以提高设计的清晰度和相应分析的精度，而不是将其扫到地毯下在介绍了符号之后，我们将继续简要概述seL4内核，并准确说明共享功能存储的含义。我们研究如何共享能力存储的传统论点导致不必要的复杂性，然后提出我们的扩展的正式访问控制模型和相关的安全定理的细节。2符号我们的元语言Isabelle/HOL在很大程度上符合正常的数学符号。本节介绍一些异常，以及一些基本数据类型和对它们的原语操作全函数空间表示为. 类型变量被写入符号t：：τ表示HOL项t具有HOL类型τ。集合（类型Jaset）遵循通常的数学约定。 我们将选项类型datatypeJa option = None|一些Ja将一个新元素None邻接到一个类型Ja。我们使用J选项来建模部分函数。函数更新写为f（x：=y），其中f：： Ja<$Jb，x：： Ja和y：： Jb，f（x<$→y）代表f（x：=Somey）。28A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）25→⇒ ⇒ ⇒⇒Isabelle支持具有命名组件的元组。例如，我们写记录点={x：：nat，y：：nat}为类型点与两个组件的类型nat。如果p是一个点，则表示p的可能值（|x= 5，y = 2|）. xp代表p的x分量. 从当前值更新p（|x= 5，y =2|），更新符号p（|x：= 4|），gives（|x= 4，y = 2|）.关键字types引入了一个类型缩写。证明规则和定理中的蕴涵表示为[[A1;.. . ;An]] = A表示A1= （...）= （An= A）. ）. 意蕴在对象内部编写公式。这种区别是Isabelle/HOL的技术人工制品。3seL4和共享功能存储正如在介绍中提到的，seL4是L4家族中的一个微内核。它包含8，700行C代码，并提供以下基本服务：进程间通信（IPC），线程，虚拟内存，中断和基于能力的访问控制。访问控制管理所有内核服务;为了执行任何系统调用，用户进程必须提供对所请求的服务具有足够访问权限的功能。作为两个例子，考虑线程通信和创建。线程之间并不直接寻址，而是通过内核中维护的通信端点进行寻址。一个端点需要两种能力来发送消息，发送线程需要写能力，接收线程需要读能力。创建线程涉及到分配线程控制块和访问该块的新功能。因此，对于一个线程创建另一个线程，它必须拥有两个不同的访问内核内存的能力：一个具有足够的空间来存储线程控制块，另一个具有足够的空间来存储新的能力。为了支持高度动态和可配置的系统，内核允许复制和撤销功能，并删除内核对象，如上面提到的端点和线程控制块。所需的数据结构是seL4实现中最复杂的部分[3]。当线程通过IPC向其他线程授予权限时，就会发生复制如果一个能力后来被撤销，内核必须暂时撤销所有从它制作的副本，这简化了从整个子系统中删除对资源的访问，但需要在内核中仔细记账一个对象只有在不能从系统的其他部分访问时才能被删除，因为相应的内存可能随后被重新用于不相关的目的。功能存储在称为CNodes的内核对象中。当然，访问A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）2529CNode对象本身由另一种类型的能力控制。但是，由于安全模型从功能类型中抽象出来，因此我们将使用特殊的存储权限来标记提供对CNode存储访问的功能。每个线程控制块都包含一个CNode的存储能力，然后它可以包含其他CNode的存储能力，等等，从而使相关线程访问能力存储的有向图-称为CSpace。在实践中，CSpace通常是树或无环图，但在我们的模型中没有限制。就本文而言，最有趣的观察是，一个CNode，以及从它可到达的其他CNode，可以链接到多个CSpaces：线程之间可以共享功能。能力模型必须解决共享问题，这样才能使从中得出的结论有效。在传统的能力模型中，CNodes的共享可能会导致远距离的幽灵行动。考虑三个线程A、B和C，其中A具有对B的授权能力，但不具有对C的授权能力，并且其中B和 C共享所有能力存储。如果A将一个能力授予B，它将出现在B的存储器中，并且，由于共享，也出现在C的存储器中-即使A没有被授权授予C！类似地，如果从B中删除了某个能力，那么它也将从C中消失。忽略通过共享存储的间接通道进行传输的可能性的高级安全分析是不正确的。传统上，共享是通过围绕它进行争论来解决的：B和C共享能力存储相当于在它们之间双向授予权限，应该这样建模。对B的能力采取的任何行动都必须立即反映在C的能力上这个论点在概念上没有错，但是随着共享结构变得越来越复杂，抽象模型和实现细节之间的关系也变得安全模型必须同时表示正常的授予权限和用于共享的附加权限它和实现模型之间的关系的形式化是复杂的，证明它是繁琐的。此外，在两个模型中执行的操作之间不再存在简单的对应关系：安全模型中的操作取决于实现模型的状态。我们认为，在本文中，这是更容易和更方便的模型共享明确，并考虑它直接在安全分析。此外，任何根据模型的主要定理运行的安全监视器都必须考虑共享。因此，一个明确的共享模型也有利于安全监视器的实现30A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）254共享能力存储的形式化模型本节介绍seL4中访问控制的扩展模型。在必要时，我们重复Elkaduwe等人的定义[8]。这些扩展包括非确定性、删除实体（不仅仅是能力）和共享能力存储。该模型分为几个部分，因为我们的工作目标是陈述和证明所有可能的系统行为的安全性定理。我们首先在4.1节中定义能力和全局状态。然后，我们在4.2节中定义了权威泄漏的含义，并在4.3节中定义了各种操作如何改变模型的状态。 安全证明的主要引理在第4.4节中陈述，并在第4.4节中推广到子系统。四点五4.1能力和全球状态遵循Elkaduwe模型，我们不区分主动（例如线程）和被动（例如内存）对象，而是将所有内核对象称为实体。从形式上讲，实体只是一组功能，这是该级别上唯一感兴趣的属性。类型实体=帽集Elkaduwe等人[8]用一个总函数和一个单独的显式域来建模安全模型的全局状态。相反，我们使用了一个从entity-ids到entities的部分函数，以便稍后更容易包含delete命令。typesstate=entity-id实体选项Testing forNone用于确定某个实体是否是状态的一部分is-entity：：state实体idboolis-entityse/=无能力同样被定义为具有两个字段的记录：（a）指定目标实体的标识符和（b）定义持有者被授权执行的操作的一组访问权限。记录上限={实体：：实体ID，权限：：权限集}其中数据类型权限=读取|写|格兰特|创建|店数据类型权限定义了我们模型中的五种原始访问权限。读和写意味着读和写信息的能力。拥有创建权限允许实体创建新实体。的实体A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）2531授予另一个实体的权限能够将其能力授予该另一个实体。Store权限模拟了共享功能的概念。如果一个实体拥有另一个实体的Store权限，那么它可以直接访问该实体中存储的所有功能。由于多个实体可以将存储功能存储到单个实体，因此这允许共享功能。我们使用术语all-rights来表示所有访问权限的集合;形式上all-rights={Read，Write，Grant，创建、存储}。我们说实体拥有直接能力（实体本身拥有的能力）和间接能力（存储连接的实体拥有的能力）。因此，为了获得实体的完整能力集，我们获取存储连接到e的所有实体的直接大写字母，其中store-connected被定义为store-connected-direct的传递、响应闭包，如下所示。direct-caps-of：：state实体ID验证caps集direct-caps-of s sref如果s sref为None则为{}|一些e ecaps-with-store：：state重复实体ID重复capsetcaps-with-store se {c J∈ direct-caps-of s e. 存储∈权利cJ}store-connected-direct：：state集合（实体ID×实体ID）store-connected-directs{（e x，e y）. e y∈实体' caps-with-store s e x}store-connected：：state（entity-id×entity-id）setstore-connecteds（store-connected-directs）caps-of：：state重复实体-id重复capset塞萨洛尼基例如为了更好地理解上述定义，让我们考虑一个小例子，其中状态s由以下定义：s idi=某个ei，i=0，1，2其中3个实体的定义如下：0|entity=id1，rights={Storre}| ） }e1{ （ |enti ty=id2 ， 权 限={Grant}|）}e2{}然后，我们可以检查这些实体的各种能力direct-caps-ofs' { E J. （e，eJ）∈store-connecteds}32A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）25e0级存储cce1e21赠款cc20= 0=0={ （|enti ty=id1 ， rights ={St orr e}|） }direct-caps-ofsid1={ （|enti ty=id2 ， 权 限={Grant}|）}direct-caps-ofs id2={}然后，我们可以计算出哪些实体是相互存储连接的。根据定义，任何实体都与自身存在商店关联，也与通过一系列商店权利关联的实体存在商店关联。因此，在本发明中，存储连接的s={（id0，id0），（id1，id1），（id2，id2），（id0，id1）}由此，我们可以确定每个实体的能力，这些能力是由实体本身直接拥有的，以及由存储连接的实体拥有的。inti={（|enti t y =id1，rights={Storre}|），（|enti t y =id2，权限={Grant}|）}1={（|enti t y =id2，权限={Grant}|）}caps-ofs id2={}虽然可以使用正式定义来理解这个模型，但使用图表可以提供很大的帮助。遵循Lipton [12]的符号，我们将模型表示为一个图，其中实体作为节点，能力作为顶点。因此，我们将使用下图来表示上述状态1.一、注意，边标签，例如Store∈c1，意味着权利，这里是Store，是c1的权利组件的成员，其中c1是e0中的能力，其实体组件是e1。Fig. 1. 示例的图表表示因为我们通常对实体的能力（而不仅仅是直接能力）感兴趣，所以我们引入虚线箭头来表示这些能力。直观地说，虚线箭头表示一系列零个或多个Store功能，后面跟着一个特定类型的功能，如图2所示。二、4.2泄漏正如在埃尔卡杜维模型中一样，安全分析的中心引理预测了给定当前状态的未来权威分布。 这就归结为这样一个问题：权威（即能力）是否会在实体之间泄漏A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）2533►→►↔►→ ∨►→e0级赠款cc2e2图二. 示例的替代图表表示这反过来又使我们能够确定系统中集体权威没有增加的分区我们现在定义了从一个子系统泄漏的能力意味着什么到另当我们证明一个能力只能从一个实体转移到另一个实体时，如果这些实体已经是传递连接的，则需要这些定义。 我们写s x y来表示实体x有能力将权限泄露给状态为s的实体y，如果x对y有授权能力，如果其中一个对另一个有存储访问权，或者如果它们都对一个公共实体有存储访问权，leak：：state安全实体-id安全实体-id安全boolsx→ygrant-capy：caps-ofs xshares-capss x y<其中，grant-cap xxx（|enti ty=x，权限={Gran t}|）萨雷斯-卡普岛 （x，e i）∈存储连通s ∈（y，e i）∈存储连通S且c：，并用它来表示子系统不能增加其图8：两个隔离子系统的示例。他们可以沟通，但他们之间的能力不能-不增加。40A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）25∈对特定实体的权力。 为此，我们还需要使用subsys-caps函数收集子系统的所有实体：subsys-capss xsubsys-caps-ofsc：> C c J∈C. 实体c J=实体c −→权利c J→权利c定义与Elkaduwe等人的定义相同。subsys-caps函数获取子系统中的实体集，然后获取它们所有能力的并集。这里，这些是实体可传递地访问的所有功能。如果C至多提供与能力c对实体c所指向的权限一样多的权限，则能力c支配能力集C（c：> C）。由于实体的能力是那些直接存储在存储连接的实体中的能力，而且这些实体也是同一个子系统的一部分，因此我们可以证明子系统能力的等价定义。这更容易使用，因为它删除了一个传递闭包级别subsys-capss x=direct-caps-ofs等式允许我们忽略共享能力对子系统之间能力转移的影响，但SysDelete操作仍然需要添加先决条件，即所讨论的实体持续存在。按照与[8]基本相同的逻辑，我们可以证明结果：定理4.5（权威的确认）。给定一个正常的状态s，一个在s中由x跨越的非空子系统，以及一个在s中具有目标身份y的能力c，如果子系统的权限在s中没有超过c，那么只要x和y都存在，它在系统的任何未来状态中都不会超过c[[sanes;sJexecutecmds s;entityc=y;is-always-entitycmds s x;is-always-entitycmds s y;c：>subsys-capsx]]=blogc：>subsys-capssJx5隔离到目前为止，安全分析涉及法律上的权利，即能力直接赋予的权利。如果我们对信息通过系统的传播感兴趣，那么我们需要考虑事实上的权利。如前所述，事实上的权限对可能试图通过间接授权渠道合作传输信息的实体进行建模。如果如果A对B有读访问权，而C对B有写访问权，那么事实上，A对C有读访问权，即使在法律上，从A到C的读操作将永远不会发生。A. Boyton/Electronic Notes in Theoretical Computer Science 254（2009）2541内核授权在上一节中，实体被划分为子系统，我们可以在这个意义上考察子系统之间的信息流。我们 不检查子系统内的信息流，因为能力可以通过定义在子系统内的实体之间传输。Bishop在4.5节中，我们考察了泄漏关系的对称闭包，与此不同的是，信息流是一个有向关系。Elkaduwe由于我们知道子系统之间的能力不能增加，我们可以得出结论，信息流的路径不能随着时间的推移在子系统之间增加。这就引出了下面的定义。我们说信息可以从一个实体集合X流到另一个实体集合Y，如果X中的一个实体对Y中的一个实体具有写能力，或者如果Y中的一个实体对X中的一个实体具有读能力，我们写为（X，Y）∈set-how s。形式上：（（X，Y）∈set-ow s）=（x ∈X. y ∈Y。 read-cap x：

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