Cerberus：一种安全高效的飞地内存共享的正式方法

1871→地狱犬：一正式方法安全高效的飞地内存共享DayeolLee加州大学伯克利dayeol@berkeley.edu卢嘉玲加州大学伯克利cathylu@berkeley.edu莫娜·维杰英特尔实验室mona. intel.comKevinCheang加州大学伯克利kcheang@berkeley.edu普拉纳夫·加达马杜古加州大学伯克利pranavsaig@berkeley.eduDawn Song加州大学伯克利dawnsong@berkeley.edu克里斯特·阿萨诺维奇加州大学伯克利krste@berkeley.edu亚历山大·托马斯加州大学伯克利alexthomas@berkeley.edu安乔·瓦尔迪克-奥伯瓦格纳英特尔实验anjovahldiek@gmail.com桑吉特河塞希亚加州大学伯克利sseshia@berkeley.edu摘要硬件安全区依赖于不相交内存模型，该模型将每个物理地址映射到安全区以实现强大的内存隔离。然而，这严重限制了飞地程序的性能和可编程性虽然一些先前的工作提出了飞地存储器共享 ， 但 它 没 有 提 供 其 设 计 的 正 式 模 型 或 验 证 本 文 介 绍 了Cerberus，一种安全有效的飞地内存共享的正式方法 为了减少形式化验证的负担，我们比较了不同的共享模型，并选择了一个简单而强大的共享模型。基于共享模型，Cerberus扩展了一个安全区平台，使得安全区内存可以通过额外的操作在多个安全区之间变得不可变和可共享。我们使用增量验证开始与现有的正式模型称为可信的抽象平台（TAP）。 使用我们的扩展TAP模型，我们正式验证Cerberus不打破或削弱安全保证的飞地，尽管允许内存共享。更具体地说，我们证明了安全远程执行（SRE）的财产，我们的形式模型。最后，本文通过在现有的飞地平台RISC-V Keystone中实现Cerberus来展示其可行性CCS概念• 形式化安全模型;信任框架;可信计算.关键词安全性;形式化方法;安全性;编程语言;安全远程执行;安全性;安全远程执行;两位作者对本文的贡献相当。本作品采用知识共享署名国际4.0许可协议进行许可。CCS©2022版权归所有者/作者所有。ACM ISBN978-1-4503-9450-5/22/11。https://doi.org/10.1145/3548606.3560595ACM参考格式：Dayeol Lee ， Kevin Cheang ， Alexander Thomas ， Catherine Lu ，Pranav Gad- damadugu ， Anjo Vahldiek-Oberwagner ， Mona Vij ，Dawn Song ， Sanjit A. 塞 希 亚 和 克 里 斯 特 ·阿 萨 诺 维 奇 . 2022 年 。Cerberus：一种安全有效的飞地内存共享的形式化方法 在2022年ACMSIGSAC计算机和通信安全会议（CCS '22）的会议记录中，2022年11月7日至11日，美国加利福尼亚州洛杉矶。ACM，纽约州纽约市，美国，15页。https://doi.org/10.1145/3548606.35605951引言硬件飞地[6，23，25，28，29，36，41]是通过分配一组只能从程序访问的物理地址来保护程序[18，45，47，48]硬件飞地的核心思想是通过使用除了典型的内存管理单元（MMU）之外的硬件机制来隔离物理内存的一部分。 隔离是基于不相交的存储器假设，其将隔离的物理存储器区域中的每一个约束为由特定飞地拥有。硬件平台通过使用额外的内存元数据和硬件原语来强制隔离例如，英特尔SGX维护称为Enclave Page CacheMap（EPCM）条目的每物理页面元数据，其中包含所有者的Enclave ID [22]。硬件查找每个内存访问的条目，以确保只有当当前安全区是所有者时才能访问页面。然而，不相交的内存假设也显着限制飞地的性能和可编程性方面首先，enclave在启动时需要进行昂贵的初始化，因为enclave程序不能使用系统中的共享库，也不能从现有进程克隆[38]。每次初始化都包括将安全区程序复制到安全区内存中，并执行测量以标记程序的初始状态。初始化延迟根据程序和初始数据的大小成比例地增加。其次，程序员需要意识到关于内存的非传统假设。例如，像fork或clone这样的系统调用不再依赖于有效的写时复制内存，导致了显着的性能下降[18，47]。CCSDayeol Lee etal.1872一些研究已经提出了平台扩展，以允许安全区的机密共享Yu等人 [65]提出了Elasticlave，它修改了平台，使得每个飞地可以拥有多个物理内存区域，飞地可以选择性地与其他飞地共享。飞地可以通过发出请求，然后由所有者授予访问权限，将其他飞地Elasticlave提高了依赖于大量进程间通信（IPC）的安全区程序的性能 Li等人 [38]提出了Plug-In Enclave（PIE），这是英特尔SGX的扩展。PIE通过引入共享飞地区域来实现更快的飞地创建，该共享飞地区域可以通过新的SGX指令EMAP映射到另一个飞地。EMAP映射预初始化的插件安全区的整个虚拟地址空间。 PIE提高了具有大初始代码和只读数据的飞地程序的性能（例如，无服务器工作负载）。虽然先前的工作表明，内存共享可以大大提高性能，他们不提供正式的安全保证毫不奇怪，飞地的不相交内存假设对于飞地平台的安全性至关重要。以前的研究[25，44，51，57]正式证明了飞地平台的高级安全保证，例如基于不相交内存假设的非干扰属性，完整性和机密性。然而，据我们所知，没有模型在被削弱的假设下正式验证安全保证，即飞地可以分享记忆实际的形式验证需要选择正确的抽象级别来建模和应用自动推理。对符合低级实现[44]或源代码[11，20，30，54，56]的模型的验证通常是特定于平台的，因为它只为这些实现提供安全保证，因此不适用于一般情况。如果有人试图验证在一系列飞地平台上的内存共享方法是安全的，那么将验证工作重用于特定实现并不容易。 我们寻求一种渐进的方法，也适用于现有的平台。此外，有许多方法可以设计内存共享模型，每种方法的复杂性和灵活性都不同。复杂的模型可以提供更大的灵活性来优化应用程序的性能，但这通常是以增加形式验证的复杂性为代价的。但是，如果内存共享限制太多，程序员也很难利用它来提高性能因此，我们寻求一种简单的分享模式，在灵活性和易于核查之间取得平衡为此，本文提出了Cerberus，一个正式的方法来安全和有效的飞地内存共享。 Cerberus选择了只读共享内存的单共享模型，允许每个安全区只能访问一个只读共享内存。 我们表明，这种设计决策通过简化不变量显著降低了验证成本，但仍然为重要用例提供了很大的性能提升。我们形式化了一个飞地平台模型，该模型可以准确地捕获扩展的高级语义，并形式化验证了一个称为安全远程执行（SRE）的属性[57]。我们从一个名为可信抽象平台（TAP）[57]的现有正式模型开始执行增量验证，其中SRE属性已经建立。最后，本文通过在现有平台RISC-V Keystone中实现Cerberus来展示其可行性[36]。地狱犬可以基本上减少了初始化等待时间，而不会引起显著的计算开销。概括而言，我们的贡献如下：提供一个通用的正式飞地平台模型，该模型具有可削弱不相交内存假设并捕获飞地平台族的存储共享通过自动化形式验证正式验证修改后的飞地平台模型是否满足SRE属性提供可与现有系统调用在现有安全区平台上实施扩展，并证明Cerberus可降低安全区创建延迟2动机和背景2.1在飞地中共享内存的使用案例现在许多程序都利用与其他程序共享内存的优势。例如，共享库允许程序使用比静态库更少的物理内存更快地初始化，因为操作系统可以为多个进程重用内存中的共享库。类似地，共享大的内存中对象（例如，存储器内键值存储）可以在多个进程之间共享由于不相交内存假设，在安全区内运行程序将禁用内存共享。本节介绍了一些在飞地中共享内存的潜在用例，以激励Cerberus。内存共享可以显著提高需要具有共享初始代码和数据的多个隔离执行上下文的飞地程序的性能。无服务器工作负载。无服务器计算是一种程序执行模型，其中云提供商按需分配和管理用于功能执行的资源。在模型中，程序开发人员只需要编写一个在语言运行时（如特定版本的Python）上运行的函数。许多无服务器框架[2，4]通过预初始化包含语言运行时的工作线程来减少执行的冷启动延迟 如Li et al. [38]，工作者将遭受极长的初始化等待时间（例如，几秒），因为语言运行时通常是几兆字节（例如，Python是4MB）。因为工人记忆之间的差异（例如，堆、堆栈和函数代码）可以小到几个字节，通过共享存储器可以节省大量的初始化延迟和存储器使用推理API。 机器学习模型服务框架[1，3，5]允许用户发送他们的输入并返回模型的推理结果。随着模型大小的增加，使用单独的安全区为不同的用户提供服务将具有更长的延迟到目前为止，Huggingface [3]中最流行的五个模型的参数从几亿到几千亿不等，这至少会占用数百兆的内存。共享内存将大大减少飞地中此类推理API的延迟和内存使用Web服务器。多处理Web服务器处理具有不同执行上下文的请求，同时共享相同的代码和大型对象。例如，提供对大对象的读访问的web服务器或API服务器（例如，前端数据或数据库）将····一种形式化的飞地内存共享方法CCS1873遭受在飞地中运行长等待时间和内存使用如果安全区可以共享内存，它们可以以更低的延迟和更小的内存使用来响应。2.2安全远程执行属性不共享任意共享上限共享第一季第二集第三1234单个共享如前所述，许多先前的工作将完整性和机密性确定为飞地平台的关键安全属性。因此，我们的目标是证明一个至少与这两个性质一样强的性质，即SRE性质。为了提供属性背后的直观性，飞地用户的典型设置是用户希望在远程飞地平台上安全地执行他们的飞地程序。 远程平台在很大程度上是不受信任的，其操作系统、一组应用程序和其他可能是恶意的飞地。 因此，期望在飞地程序和用户之间创建安全通道，以便安全地设置飞地程序。因此，为了实现端到端的安全性，我们需要确保安全区平台以以下三种方式运行：在远程平台上对安全区的测量可以保证安全区被正确地设置并且以确定性的方式运行每个飞地程序受到完整性保护以免受不可信实体的影响，因此确定性地执行每个安全区程序都受到保密保护，以避免向不受信任的实体泄露机密。这三种行为表现为第5节中定义的安全度量、完整性和机密性属性，并且最终是我们用Cerberus扩展的平台模型的保证。2.3飞地平台的形式化模型先前的工作已经正式建模和验证了飞地平台模型的功能正确性和遵守类似于SRE属性的安全属性 而在源代码级的验证（例如， Komodo [25]）提供了软件安全监视器管理的飞地的功能正确性和不干扰性的证明，现有的验证工作通常与实现密切相关，因此很难将现有的工作应用于我们的扩展。二进制或双精度级验证（例如，Serval [44]）则侧重于实现的自动化验证。使用二进制级别的模型通常是困难和乏味的，因为二进制通常缺乏高级程序上下文（例如，变量名）。本文的目的是验证一般飞地平台上的飞地内存共享因此，二进制级别的验证是本文的非目标，虽然它可以通过验证给定的实现在二进制级别上改进我们的模型来补充该方法。可信抽象平台模型[57]是一种抽象，与SRE属性一起引入的飞地平台。SRE属性声明远程平台上的飞地执行遵循其预期的语义，并且受到机密保护以免受与TAP模型一起定义的一类对手的攻击。此属性为在远程平台上运行的安全区提供完整性和机密性它也已被正式证明，最先进的飞地平台，如英特尔图1：具有不同灵活性的内存共享模型。灰色（和白色）框表示可共享（和不可共享）的物理内存区域，圆圈表示飞地.从飞地到物理存储器的边是声明飞地可以访问其所指向的存储器的访问关系该图仅描绘了存储器区域的数量与飞地的数量相同的情况，但是��� 可能比实际上更大���。TAP模型，从而满足SRE对各种对手模型。据我们所知，TAP是唯一一种用于以一般方式捕获飞地平台的正式验证模型抽象的层次也使它易于扩展。基于这些原因，本文对TAP模型进行了扩展。3设计决策在我们的方法中做出了几个设计决策，以符合我们的设计目标。内存共享模型和接口设计是建模、验证和实现的关键。本节将详细讨论我们如何选择设计内存共享模型和接口。3.1可复制共享内存某些程序使用共享内存实现高效的进程间通信（IPC），这要求对共享内存的任何写入对其他进程可见Elasticlave [65]允许一个安全区将一个内存区域的写权限授予其他安全区，这样它们就可以在不加密或复制数据的情况下进行通信。然而，作者还示出了这样的可写共享存储器需要动态地改变写入许可以防止飞地之间的干扰。 作为正式推理的内存与动态权限将引入一个不平凡的复杂性，我们离开这个方向作为未来的工作。因此，Cerberus不支持基于IPC或其他可变共享数据的用例类似地，PIE [38]也只允许在飞地之间共享只读内存。3.2内存共享模型图1显示了四种不同的内存共享模型，具有不同的灵活性。我们讨论了实现的影响和形式化验证的可行性，为每个模型。对于这个讨论，我们使用的数量之间的访问关系圈和内存区域作为一个度量的复杂性验证和实现。禁止共享。我们将假设不相交内存假设的模型称为非共享模型，该模型在最先进的飞地中实现[25，36，41]。无共享模型严格禁止共享内存，并将每个物理地址给一个安全区。因此，访问关系的数量为���������������������������（第一季第二集第三1234第一季第二集第三第一季第二集第三··1234·1234CCSDayeol Lee etal.1874（）下一页（+）飞地1飞地2飞地3独立区10飞地11飞地12objZ立白libX飞地1独立区10飞地11飞地2飞地12objZ立白立白libX上限共享单一共享图 2 ： 用 例 中 capped 和single-sharing 模 型 之 间 的 差 异 。libX、libY和objZ是安全区想要共享的大型对象。Enclave 10和11依赖于libX和libY，而Enclave 12依赖于libY和objZ。regions，而numbers是飞地的数量因此，不共享的实现将需要元数据缩放���，以保持访问关系。例如，每个SGX EPC页面在EPCM中具有对应的条目，其包含页面的所有者ID无共享模型已在不同级别得到正式验证[25，44，57]。任意分享。可以完全放松共享模型，允许任意数量的飞地共享内存（如Elasticlave）。 我们将这种共享模型称为任意共享模型。在这种情况下，飞地之间的访问关系的数量为���（������）。因此，任意共享需要使用���（������）进行元数据缩放。分享分享分享 为了实现访问关系的数量的可伸缩性，可以约束共享策略，使得每个飞地只能访问有限数量的共享物理存储器区域。我们将这种共享模式称为封顶共享模式。图在图1中，封顶共享示出了每个飞地仅被允许访问最多两个附加共享物理存储器区域的示例例如，PIE [38]引入了一种称为插件飞地的新型飞地，它可以映射到普通飞地的虚拟地址空间。这将关系的数量减少到了100个，其中100个是允许由飞地访问的共享物理内存区域单身共享单一共享模型是上限共享的一个特例，其中���= 1。因此，该模型仅允许飞地访问特定飞地的共享存储器区域。 单一共享将复杂度降低到���（���）。3.3共享模型的形式化验证由于模型的灵活性，形式化验证任意或有上限的共享模型是一项挑战。SRE等安全属性的根据我们的经验，对任意数量的共享内存进行建模会增加这种复杂性。例如，证明TAP上的SRE所需的一个归纳不变量是，如果存储器区域可由飞地访问，则该区域由飞地拥有。为了允许共享任意数量的内存区域，不变量应该被扩展，使得它在所有关系上存在量化，例如，声明内存的所有者是与飞地共享其内存的飞地之一（参见§5和等式（8）详情）。TAP中不变量的编码使用一阶逻辑和数组理论，并且通常是不可判定的[15]。因此，这个量词的引入进一步使不变量复杂化。 尽管在上限共享中存在限制性约束，但捕获任何任意限制���的正式模型仍然需要对任意数量的共享内存进行建模，就像在任意共享方案中一样，并且面临相同的复杂性。相比之下，单共享模型大大减少了形式化推理和实现的工作量首先，形式化推理不再需要复杂不变量，因为飞地可访问的内存要么属于飞地本身，要么只属于共享内存的另一个飞地第二，实现变得简单得多，因为它仅需要一个每飞地元数据来存储对共享存储器的引用。 平台修改也变得最小化，因为它在每次内存访问时只检查一个元数据。尽管它很简单，但单一共享模型仍然可以通过使所有共享内容（例如，共享库、初始代码和初始数据）。图2描述了封顶共享模式和单一共享模式之间的差异。 利用加帽共享模型，每个可共享内容可以用单独的飞地来初始化，从而允许每个飞地映射到���不同的飞地存储器区域（即，PIE中的插件包体）。单一共享模型仅允许每个飞地映射一个其他飞地，当异构工作负载具有共享代码时，在存储器中留下潜在的重复（例如，libY）。我们声称，该模型的简单性的好处超过了限制，因为单一共享没有显着的缺点，超过封顶共享时，异构工作负载之间没有共同的内存。3.4接口飞地程序需要接口函数来基于共享模型共享内存Elasticlave和PIE引入了显式操作来将可共享的物理内存区域映射或取消映射到安全区的虚拟地址空间。例如，Elasticlave需要一个enclave程序显式调用map操作来请求访问该区域，这将由所有者通过共享操作批准。类似地，PIE允许飞地使用EMAP和EUNMAP指令来将整个插件飞地存储器映射和解除映射到飞地的虚拟地址。Elasticlave和PIE允许飞地程序将可共享的物理内存区域映射到其虚拟地址空间。然而，这些方法也有一些缺点。首先，程序员必须手动指定应用程序的哪一部分应该是可共享的。在大多数情况下，程序员必须完全重写程序，使得程序的可共享部分被划分到单独的飞地存储器中。其次，动态映射或取消映射需要本地证明，其验证新映射的存储器处于预期的初始状态。因此，程序的测量属性依赖于多个物理存储器区域的测量属性。Cerberus采用了一种类似于传统优化技术的方法，即通过写时复制（copy-on-write）来克隆地址空间，就像在clone和fork这样的系统调用中一样。这种方法适合Cerberus的使用情况，其中可共享的区域包括文本段、静态数据一种形式化的飞地内存共享方法CCS1875片段，和动态对象（例如，机器学习模型）。一般来说，程序员希望这样的系统调用将进程的整个虚拟地址空间（无论它包含什么）复制到新创建的进程。类似的接口将允许程序员编写具有相同期望的飞地程序而且，这样的接口将不需要关于多个飞地的测量的附加属性或假设。由于飞地的初始代码已经包含何时共享其整个地址空间，因此初始测量隐式地包括要共享的所有存储器内容。为此，Cerberus引入了两种飞地操作，即快照和克隆。 快照冻结安全区的整个内存状态，克隆创建安全区的逻辑副本。我们使快照只能从安全区本身调用，允许安全区决定何时共享其内存。对手可以随时调用克隆，这不会破坏安全性，因为它可以被视为启动安全区的特殊方式（请参见§4.4.1）。 当攻击者在现有安全区上调用克隆时，将创建一个新的安全区，并使用快照的写时复制（CoW）内存恢复。因此，在克隆之后对每个安全区的任何更改彼此不可见下面的部分将正式讨论Cerberus的共享模型和接口。4形式化模型我们首先在第4.1节中介绍了一种威胁模型，它与这些目标和当前最先进的飞地威胁模型相一致。然后，我们在第4.2节中列出并证明了我们的假设，在第4.3节中介绍了基于这些假设的平台和对手的正式模型，然后在第4.4节中介绍了两个新的操作快照和Cerberus的克隆。在第5节中，我们使用这些形式化模型来定义SRE [57]属性，这是一个关键的安全属性，用于证明在远程平台上执行的飞地正在按预期和机密地运行。这些属性，然后正式验证使用增量验证TAP。换句话说，我们的正式模型扩展了由Subramanyan等人介绍的TAP模型。 [57 ]第50段。虽然SRE已经在扩展的TAP模型上得到了证明，但Cerberus设计削弱了不相交的内存假设以允许内存共享。此外，目前还不清楚这两个额外的操作是否明确保留了SRE。因此，我们证明SRE仍然成立在我们的扩展模型下进行操作。对于其余的文献，我们参考由以下定义的原始正式平台模型：远程飞地平台Ence其他应用用户I/OEnclave平台/可信平台扩展软件（操作系统/虚拟机管理程序）其他飞地图3：用户在与不受信任的软件隔离的远程安全区平台中配置其（受保护的）安全区扩展绿色/红色框表示可信/不可信组件。不应该被操作系统或其他安全区和应用程序观察到 我们确保安全区仍然是写隔离的，这意味着对来自一个安全区的数据的任何修改都不能被其他安全区观察到，甚至不能被它所克隆的安全区观察到。因此，任何秘密数据都需要在飞地被克隆之后被安全区程序员有责任确保父安全区不包含任何可能通过子安全我们不认为在安全区中运行的程序本身是脆弱的或恶意的。例如，程序可以在共享存储器中生成密钥，并使用该密钥加密孩子的机密数据。这将破坏彼此写隔离的子飞地之间的机密性，因为子飞地将访问共享存储器中的密钥我们不考虑这种情况，但这可以很容易地解决，让程序在创建了不信任的孩子之后将秘密加载到它们的内存中。由于我们的主要目标是设计一个通用的扩展，我们也不考虑任何类型的侧信道攻击或特定于架构的攻击[16，17，31，35，39，40，43，52，59，60，62，64]。 我们离开侧通道弹性接口设计作为未来的工作。我们注意到，由于基本TAP模型也被用于证明某些飞地平台上的侧通道弹性[23，36]，因此将我们的证明扩展到此类攻击模型并非不可能否认Subramanyan等人[57]作为TAP和我们的扩展模型TAP���。4.1威胁模型我们的扩展遵循典型的飞地威胁模型，其中用户���的飞地程序在飞地状态（例如，区域程序所拥有的寄存器值和数据存储器）对抗在远程区域平台中运行的任何软件对手。安全区的软件对手包括不受信任的操作系统、用户程序和其他安全区，如图3所示。在Cerberus中，飞地可以共享在引入克隆之前在飞地之间共享的数据或代码。我们假设内存在这些具有共享内存的飞地然而，每个飞地对飞地的服务也超出了本文的范围这与现有技术的飞地平台的威胁模型一致。第§4.3.5节在正式定义平台之后，对威胁模型的正式模型进行了更详细的描述4.2TAP模型假设下面，我们总结了一系列关于TAP执行模型���的假设，这些假设是为了简化和抽象建模。这些假设与上述对手模型一致：TAP安全性继承了TAP [57]的假设和限制，包括假设每个平台和安全区操作相对于彼此是原子的，假设·CCSDayeol Lee etal.1876O∈→[客户端]MOSM[][·]MM []M������→ × × {}（）CubeOSE ∪ {OS} ∪ {}E������������∈⟨⟩×（）∈M[]M[]M[]M[客户端]������（）下一页∈M[ ] M[]M[]∈（M [ ][][M [ ]]<$）⊥→������→DRAM是可信的，不支持按需分页，假设一个单核和单进程模型，并假设用于测量的加密功能的属性。如果安全区操作返回错误代码，我们假设平台的状态完全恢复到执行该操作之前的状态。飞地的状态连续性超出了我们模型的范围，与之前的工作TAP [57]一致，并且可以使用替代方法[27，46]来解决。内存分配算法（例如，用于写时复制）是确定性的，假定未分配内存的集合是相同的。这意味着给定平台的任何两个执行序列，只要页表状态相同，分配算法将返回相同的空闲内存位置进行分配。接下来，我们介绍我们的正式模型描述的平台，扩展现有的TAP模型与快照和克隆在这些假设下。4.3正式TAP平台模型概述如上所述，飞地平台的用户通常具有他们想要在远程服务器中安全运行的程序和数据，与所有其他进程隔离，如图3所示。这样的程序可以作为飞地运行���。 远程服务器使用其硬件原语和用于管理飞地的软件来提供隔离，其中软件组件通常是固件或安全监视器。 该软件组件通过一组操作（由表示）为飞地用户提供界面，以进行管理���。我们的目标是确保这块飞地的安全受到保护对一组单词的理解。我们写来表示给定物理地址PA处的内存值。��� 页表抽象定义了虚拟地址到物理地址的映射PA和访问权限perm：���������������，其中���������是读、写和执行权限的集合。���������可以定义为产品������������������������������������������，whhe re������������=.������������，���������������值对应于给定虚拟地址索引的读、写和执行许可。ecurr：execute表示正在执行的当前安全区。������������������ 是 由 自然 数和特殊标识符表示的安全区ID的集合表示不受信任的操作系统。我们保留标识符������������来引用无效的安全区ID，可以将其视为不引用任何有效安全区的默认值。为了便于参考安全区是否有效和启动，我们定义一个特定的词���������������������=. ���������≠���������������������≠这又反过来，无论ID是否是有效的飞地ID。���每当飞地被启动或克隆并且在状态中尚未被销毁时，活动谓词都为飞地返回true���。 o是描述物理地址的所有权的映射，每个物理地址可以由安全区（具有对应的安全区ID）或不受信任的操作系统拥有。最后，每个飞地���都有一组飞地元数据，这是表2中描述的变量的记录。 我们滥用记法，写���������来表示���������元数据映射中存储的记录中的程序计数器。对于表2中定义的其他元数据字段，我们类似地使用飞地索引操作符来引用特定飞地安全区启动是安全区的入口点，安全区启动在Launch之后和Enter之前开始。M[���]是的虚拟地址映射，从平台上的所有其他进程并按预期运行飞地计划M[���]是地址权限映射为了理解证明的目的，我们将我们想要保护的飞地称为受保护的飞地���。 我们这样做是为了将其与对手控制的飞地区分开来。4.3.1平台和飞地国家。平台可以被看作是一个过渡系统���=���，���������，或者，也可以将其看作是对一组状态变量的赋值。平台在集合���中的初始状态中开始，并且在由转换关系定义的状态之间转换。���我们写���，���“ a”表示平台从到的有效过渡������。 执行所述因此，平台发出一个（可能是无限的）状态序列每个虚拟地址。������安全区是从虚拟地址到布尔值的映射，表示地址是否分配给安全区。���������安全区的当前程序计数器。安全区寄存器文件是安全区的保存寄存器文件。安全区暂停是一个布尔值，表示安全区是否已暂停，启动时初始值为false。���这些变量被引入到基本TAP模型中，在TAP模型中没有修改。我们在§4.4节介绍了Cerberus所需的其余四个元数据TAP模型中未在基本TAP模型中定义的状态变量状态变量（state）是平台状态到���的飞地状态���，包括M ������[���]、M������[���]、M������[���]，��� = ���100，���1，. 其中，对于n∈N，（ n，n���+1）∈N。���我们写=���������������������������可互换，但通常在引用特定跟踪时写入“跟踪当一个enclave最初启动时，它处于enclave执行之前的初始状态，我们使用谓词（）���表示：→。������������������ 我们在下面的§4.3.2节中描述了TAP的变量���集和飞地状态������（���）���。4.3.2TAP���状态变量。TAP中的每个变量������都是包块，包块记忆的投射������������ ���������你好������ITE������ ������ ，���������。在最后一个表达式中，���������是虚拟地址集合上的常用lambda运算符，表达式体是ifthen else运算符，如果条件为真，则返回条件1，否则返回条件2。������������������������是恒定的底部值，可以认为是不关心或不可观察的这种记忆的投射如表1所示。 pc：������p是p图计数器的抽象其值是来自所述虚拟地址���集合的虚拟地址���。Δ������：N���是寄存器文件，其是从（自然数的）寄存器索引集合N到字集合���的映射。中文（简体）是内存的抽象，它映射物理地址集表示可由飞地存储器访问的所有存储器，包括共享存储器和由虚拟地址映射M_Enclave所拥有的存储器。���我 们可以这样写：到平均变量∈的类型为���������类型为→的†，其中索引类型为，值类型为。���我们使用=。 这意味着通过定义来区分最佳质量符号。···一种形式化的飞地内存共享方法CCS1877→→→→→ EOOS1111MM222E†（）下一页（）下一页一（）（）（）（）操作系统O {}（）OO--（）（）（）（）（）下一页O（）下一页（）下一页（）（）∈（[][ ]）0州变量类型说明PC������程序计数器。���������通用寄存器。物理内存。一个PA虚拟表页面表抽象;虚拟到物理，���cal地址映射。一个perm���虚拟表页面抽象;虚拟到他们的权限.ecurr当前执行的enclave ID（或ecurr=������当对手不执行而不被对手观察时，采取任何数量的步骤传统上，我们定义了一个对手的观察和篡改功能，描述了对手可以观察和改变在其执行过程中的平台状态，以打破完整性和机密性。处决对手是如果OS正在执行）。o从物理地址映射到en-������ ������拥有它的克拉夫中的操作AdversaryExecute������������攻击者可以使用篡改或观察功能的攻击过程ME������→ E���飞地ID到飞地元数据的映射。emd[OS]存储OS的检查点图4描述了我们模型的这两个函数。表1：TAP状态变量州变量每个字段的类型描述M������������飞地入口。���0������0. . .������A级���+1日本语+1中国���+2. . .��������������������������������� ���������Enclave的虚拟地址映射。��� ��� → ���������Enclave的地址权限。���2������0. . .������A级���+1日本语+1中国���+2. . .M������������→������������私有虚拟地址的集合。保存������������程序计数器。M ������������N →���保存的寄存器。M������������������������������飞地是否暂停。M������†飞地������������是否是快照。图4：说明了平台在安全度量、完整性和机密性证明中的两个轨迹的执行。检查每个属性的证明义务儿童������飞地的数目。M������†E ������Enclave的根快照。所指示���L和相等的初始条件表示为M���������†������→������������自由物理地址的映射。我的天op 指示从O表2：TAP记录������ 飞地元数据。指示为支持快照&克隆而添加的其他状态变量。4.3.3飞地输入和输出。对于���给定的状态，飞地和外部进程���之间的通信通过的输入和输出来控制���������������������。������包括���管理飞地的操作的自变量���、飞地可以访问的飞地外部的存储器区域以及不受信任的攻击者可以写入的存储器区域，以及来自平台的随机性。���������包含安全区的输出������，攻击者和用户可以对其进行写入和访问。4.3.4平台和飞地执行。enclave的执行���由其中，操作的执行直到其输入���������和当前状态���������都是确定性的。这意味着，给定相同的输入���������和飞地状态���������，对飞地状态的改变���������被取消。术语。基本TAP模型的操作集为������������=.启动，销毁，进入，退出，删除，恢复，敌对执行。TA P���用两个额外的操作扩展基本集合：下载快照，克隆。我们使用谓词=来������������������指示可能受对手控制飞地正在状态“0”处执行，且������������“0”指示操作���������系统正在执行。4.3.5正式的粘附模型。在我们的模型中，不受信任的实体（如OS和不受信任的飞地）由对手表示，该对手可以对受保护的飞地之外的状态进行任意修改���，表示为���������。 与基本TAP模型一致，不受信任的实体和受保护的飞地���轮流在我们的正式TAP���模型中的交错语义下执行，如图4所示。 在这些语义下，当飞地不执行时，允许对手采取任意数量的步骤。同样，允许受保护的安全区A表示对手执行。防篡改功能。篡改函数用于对攻击者对平台状态这些恶意修改进行建模，并且在���包括不被受保护的飞地存储器和页表映射所拥有的任何存储器位置的加密器���模型的语义允许对手在执行时进行这些更改我们允许所有被篡改的状态在我们的模型中不受约束，这意味着它们可以取任何值。这种类型的攻击者篡改功能过度近似威胁模型可以改变的内容，通常被称为攻击者[19，57]。观察功能。 对手���������������的观察功能表示。在我们的模型中，我们允许攻击者观察不属于受保护飞地的内存位置���，用集合���������������=来描述。 ���������=. ������PA. ������ ������. 奥���里你，你。你���好，直觉，������������是平台状态的投影，可由对手观察到，其差异应被属性排除。例如，如果在不同秘密上操作的同一个飞地程序通过输出揭示了秘密，那就是飞地程序中的错误，我们不对此进行保护。攻击者可以尝试在飞地的生命周期期间修改或读取飞地在这种威胁模型下，我们证明了TAP���模型仍然满足第5节中描述的SRE属性。4.4扩大飞地行动Cerberus是安全区平台的扩展，具有两个新的操作快照和克隆，以促进安全区之间的内存共享。直观地，快照将执行操作的安全区转换为只读安全区，克隆从正在克隆的父安全区创建子安全区，以便子安全区可以在克隆时读取和执行与父安全区相同的内存内容。LLLL≈CCSDayeol Lee etal.1878������[] M [ ] []������M[]M[]M[]M[客户端]→ E →M[][] ∈������（（））（）���（）下一页（）（）（）（）M[]∧推出克隆(a) 克隆推出快照克隆(b) 快照（c）快照+克隆如果条件满足，则Clone将把MySQL虚拟地址空间中的所有数据复制到MySQL，以确保写隔离。���对于每个由服务器映射的虚拟地址，克隆首先选择服务器拥有的物理地址，将内容从服务器[M���]复制到服务器，并更新服务器的页表，使得������������������������������ ������ =���.这可以在平台本身中实现（即，e���.安全，安全图5：克隆、快照和快照后克隆.虚线箭头表示克隆新创建的飞地。这个扩展需要四个新的元数据状态变量，在表2中用符号表示。���是������一个布尔值变量，指示是否已在安全区上调用快照���。������clone是clone拥有的子节点数，换句话说，是clone在安全区clone上被调用的次数，其中clone是Clone的父节点。���������如果存在根快照，则根快照是对根快照的引用，而根快照是已分配给根快照但尚未分配内存的���我们现在