摘要
现实的安全处理器，包括为学术和商业目的而构建的处理器，通常实现“证明执行”抽象。尽管是现代安全处理器的事实上的标准，但“证明执行”抽象还没有得到足够的正式处理。我们为“证明执行”的安全处理器提供正式的抽象，并严格探索其表达能力。我们的探索既展示了预期，也展示了令人惊讶的结果。
一方面，我们表明，就像普遍的看法一样，证明执行非常强大，并且允许人们实现强大的加密抽象，例如有状态的反映，即使在假设虚拟黑盒混淆和无状态硬件令牌时，其存在也是不可能的。另一方面，我们惊讶地发现，使用经过验证的执行处理器实现可用的双方计算并不像人们预期的那样简单。具体来说，只有当双方都配备了安全处理器时，我们才能实现可组合的双方计算。如果其中一方没有安全处理器，我们就表明无法进行可组合的双方计算。然而，在实践中，期望允许多个传统客户端（没有安全处理器）利用服务器的安全处理器来执行多方计算任务。我们将展示如何引入最少的额外设置假设来实现这一点。最后，我们表明，如果安全处理器没有可信时钟，那么一般功能的公平多方计算是不可能的。当安全处理器具有可信时钟时，如果双方都配备了安全处理器，我们就可以实现公平的双方计算。但如果只有一方拥有安全的处理器（带有可信时钟），那么对于一般功能来说，公平性仍然是不可能的。
1.介绍
网络安全科学建立在一个基本的指导原则之上，即最小化系统的可信计算基础（TCB）[78]。由于在实践中特别是在遗留系统存在的情况下拥有“完美”软件是非常困难的，因此架构社区提出了一种新的范例来从可信硬件（以下也称为安全处理器）引导系统的安全性。粗略地说，安全处理器旨在将敏感应用程序的可信计算基础仅减少到处理器本身（可能与最小软件TCB（例如安全管理程序）结合）。特别是，除了自身之外，敏感应用程序（例如，银行应用程序）不应该信任任何其他软件堆栈（包括操作系统，驱动程序和其他应用程序）来维护任务的机密性或完整性 - 关键数据（例如，密码或信用卡号）。即使软件堆栈可能受到危害，安全性也会保留（只要敏感应用程序本身完好无损）。除了软件对手之外，一些安全的处理器也使其成为防御物理攻击者的目标。特别是，即使对手（例如，云服务提供商的流氓员工或系统管理员）具有对计算平台的物理访问权并且可能能够窥探或篡改内存或系统总线，他也不应该收获秘密信息或破坏程序的执行。
通常认为可信硬件为构建安全系统提供了非常强大的抽象。潜在的应用很多，从云计算[13,35,59,69,70]，移动安全[68]，网络安全到加密货币[82]。在过去的三十年中，学术界和工业界已经提出并证明了许多安全处理器[7,28,34,39,40,57,58,60,74,81];其中一些已经商业化，包括众所周知的可信平台模块（TPM）[2]，Arm's TrustZone [6,8]等。值得注意的是，英特尔最近发布了名为SGX [7,33,60]的新型x86安全扩展，引发了广泛的兴趣，以构建利用新兴可信硬件产品的新型防弹系统。
1.1证明执行安全处理器
虽然有许多关于可信硬件设计的建议，但这些设计在架构选择，指令集，实现细节，加密套件以及它们承诺防御的对抗模型方面差别很大 - 令人惊讶的是，它看起来不知何故大多数这些处理器已经融合在一起提供了一个通用的抽象，从此被称为证明的执行抽象[2,7,34,60,74,77]。粗略地说，一个经过证实的执行抽象实现了以下功能：
•配备有经过验证的执行处理器的平台可以将程序和输入（此后表示为（prog，inp））发送到其本地安全处理器。安全处理器将通过输入执行程序，并计算outp：= prog（inp）。然后，安全处理器将使用秘密签名密钥对元组（prog，outp）进行签名以获得数字签名σ - 实际上，在签名之前应用散列函数。特别地，该签名σ通常被称为“证明”，因此该整个执行被称为“证明执行”。
•上述程序的执行是在沙盒环境中进行的（因此称为飞地），因为软件对手或物理对手不能篡改执行，或检查生活在其中的数据。飞地。这对于实现隐私保护应用程序非常重要。例如，知道安全处理器的公钥的远程客户端可以与驻留在远程服务器S上的安全处理器建立安全信道。然后，客户端可以将加密和认证的数据（和/或程序）发送到安全处理器 - 同时消息通过中介S传递，S不能窃听内容，也不能篡改通信。
•最后，各种安全处理器在如何实现上述安全沙盒机制方面做出了不同的具体选择 - 这些选择与安全处理器试图防范的对抗能力密切相关。例如，粗略地说，英特尔的SGX技术[7,60]针对的是受限制的软件对手，它不会测量时序或其他可能的侧通道，也不会观察到飞地应用程序的页面交换行为（例如，飞地应用程序）使用小内存或设计数据 - 遗忘）;它还可以防御能够窃听内存的受限物理攻击者，但无法点击内存总线上的地址或测量侧信道信息（如时序和功耗）。
我们将读者推荐给Shi等人。 [72]用于可信硬件的通用介绍，以及各种安全处理器所做出的不同选择的综合比较。
架构社区已经融合到“证明执行”抽象的事实是有趣的。究竟如何成为事实上的抽象超出了本文的范围，但有助于观察证明的执行抽象在实践中具有成本效益，具体如下：
•通用：经过证实的执行抽象支持在安全区域内计算通用的，用户定义的程序，因此可以实现广泛的应用程序;
•可重用性：它允许单个可信硬件令牌被多个应用程序和世界上的每个人重用 - 有趣的是，事实证明这种可重用性实际上产生了许多技术问题，将在本文后面讨论;
•诚信和隐私：它提供完整性和隐私保障。特别地，尽管配备有可信硬件的平台P在与可信硬件的每次交互中服务于中介，但是可以通过使远程用户与安全处理器建立安全信道来引导隐私保证。
在本文的其余部分，每当我们使用术语“安全处理器”或“可信硬件”时，除非另有说明，否则我们特别指的是证明执行安全处理器。
1.2为什么安全处理器的正式抽象？
虽然证明执行已被社区接受为事实上的标准，但据我们所知，没有人探讨过以下基本问题：
1.准确而正式地，证明的执行抽象是什么？
2.什么可以证明执行表达，什么不能表达？
如果我们能够正式而准确地阐明这些问题的答案，那么这些好处就可以广泛传播。它至少可以通过以下方式帮助生产者和可信硬件的消费者：
•了解抽象的变化是否会导致表达能力的差异。首先，各种安全处理器可能提供类似但略有不同的抽象 - 这些差异是否与可信硬件的表现力有关？如果我们希望为安全处理器添加特定功能（例如，时序），此功能是否会增加其表现力？
•正式使用可信硬件。许多工作已经证明了如何使用可信硬件来构建各种安全系统[13,14,29,35,59,64,67,69-71]。不幸的是，由于可信硬件提供的精确抽象甚至不清楚，大多数现有工作采用的方法范围从启发式安全到半正式推理。
此外，大多数已知的安全处理器暴露与密码相关的指令（例如，涉及哈希链或数字签名[2,7,33,60]），这使可信硬件的编程变得混淆 - 特别是，程序员基本上必须设计加密协议以利用可信硬件。很明显，用户友好的高级编程抽象隐藏了加密细节将是非常需要的，并且可能是可信硬件编程民主化的关键（事实上，通常是安全工程） - 然而，如果没有准确地表达可信硬件提供的正式抽象，显然不可能在顶部构建正式的正确的高级编程抽象。
•迈向正式安全的可信硬件。最后，了解可信硬件的“良好”抽象是什么，可以为可信硬件的设计者和制造商提供有用的反馈。圣杯将是设计和实施正式安全的处理器。了解要实现的加密级正式抽象是实现这一长期目标的必要的第一步 - 但实现这一目标显然需要额外的，互补的技术和机制，例如在正式方法社区中开发的那些[39， 65,66,81]，这可能使我们能够确保实际的安全处理器实现符合规范。
1.3我们的贡献摘要
据我们所知，我们是第一个为实际的，经过证实的执行安全处理器调查加密声音和可组合的正式抽象的人。我们的研究结果证明了“预期”和（可能）“令人惊讶”。
预期和令人惊讶的。一方面，我们证明了经过验证的执行处理器确实非常强大，正如人们所期望的那样，并且允许我们实现原语，否则即使在采用无状态硬件令牌或虚拟黑盒安全加密混淆时也是不可能的。
另一方面，我们的调查揭示了在没有正式建模的情况下可能容易被忽视的微妙技术细节，我们得出了一些可能最初令人惊讶的结论（当然，事后看来很自然）。例如，
•我们表明，如果一方没有这样一个安全的处理器（而另一方就是这样），那么普遍可以组合的双方计算是不可能的。
这对我们来说最初是令人惊讶的，因为我们通常认为一个经过证实的执行处理器提供了一个可以计算通用的，用户定义的程序的“无所不能”的可信第三方。当存在这样的可信第三方时，似乎可以安全且非交互地评估任何功能，从而隐藏程序和数据。解释我们的发现的一种方法是，这种直觉在技术上是不精确和假设的危险 - 虽然证明执行处理器确实接近提供这种“可信第三方”理想抽象，但有些方面对于这种理想的抽象是“不完美的”，不应该被忽视，并且必须采用严格的方法来正式使用可信硬件。
多方计算的其他结果。我们还显示以下结果：
•普遍适用的双方计算可能会在任何一个配备了经过验证的执行处理器的情况下进行。我们给出了一个明确的结构，并表明其设计和证明中有几个有趣的技术（我们将很快评论）。处理这些技术细节也证明了一个可证明安全的协议候选者在重要细节上与最自然的协议候选者[49,64,70]从业人员会采用（不知道具有可证明的可组合安全性）的区别。这证实了正式建模和可证明安全性的重要性。
•尽管即使单方没有安全的处理器也不可能进行多方计算，但实际上仍然需要构建多方应用程序，其中多个可能的旧客户端将数据和计算外包给配备有单个云服务器的单个云服务器安全的处理器。
我们展示了如何引入最小的全局设置假设 - 更具体地说，通过采用全局扩充公共参考字符串[22]（以下称为Gacrs） - 来规避这种不可能性。尽管即使没有安全处理器[22]，Gacrs也知道通用UC安全MPC的理论可行性，但是现有结构涉及在要安全评估的程序的运行时间中（至少）线性的加密计算。相比之下，我们对仅涉及O（1）量的加密计算的实际构造特别感兴趣，而是在安全处理器内执行所有与程序相关的计算（而不是加密）。
技术。我们的结构中出现了一些有趣的技术问题。首先，组合式校样通常要求模拟器拦截和修改与对手（和环境）之间的通信，以便对手无法区分它是与模拟器或现实世界的诚实方和安全处理器对话。由于模拟器不知道诚实方的输入（超出计算输出所泄露的输入），由于不可分辨性，可以得出结论，对手也不能知道诚实的各方输入。
•等同。我们的模拟器执行此类模拟的能力受到安全处理器签署证据的证据的阻碍 - 因为模拟器不具有秘密签名密钥，它不能修改这些消息并且必须直接将它们转发给对手。要解决这个问题需要新的技术来执行模棱两可，这是标准协议组合证明中出现的技术性问题。为了实现模棱两可，我们提出了在飞地项目中设置特殊后门的新技术。必须精心设计这样的后门，以便它们为模拟器提供更多的动力，而不会给现实世界的对手额外的力量。通过这种方式，我们可以充分利用这两个方面：1）诚实方的安全不会在实际执行中受到伤害; 2）证明中的模拟器可以“编程”飞地应用程序以签署其选择的任何输出，只要它能够展示正确的陷门。在几乎所有的协议中，该技术以不同的形式重复使用。
•提取。提取是协议组合证明中常见的另一个技术问题。这个技术问题最有趣的表现形式是我们的协议，它在全局公共参考字符串（Gacrs）和单个安全处理器（参见第6节）的情况下实现多方计算。在这里，我们再次利用在飞地计划中种植特殊后门的想法来允许这样的提取。具体而言，当提供一方的正确身份密钥时，飞地程序将泄露该方对呼叫者的输入。诚实的参与方安全不会受到这个后门的伤害，因为没有人在现实世界中学习诚实党派的身份证，甚至连诚实党派本身都没有。然而，在模拟中，模拟器学习腐败方的身份密钥，因此它可以提取腐败方的输入。
值得信赖的时钟和公平。最后，我们正式证明了抽象的差异如何导致表达能力的差异。特别是，许多安全处理器提供可信时钟，我们在公平的双方计算环境中探索这种可信时钟的表现力。众所周知，在标准设置中，一般功能的双方计算中不可能存在公平性[32]。然而，最近的一些研究表明，一般功能的不可能性并不意味着每种功能都是不可能的 - 有趣的是，存在一类可以在普通环境中公平计算的功能[9,46,47]。我们在证明的执行处理器的背景下演示了几个有趣的发现：
•首先，甚至比普通环境更公平地执行计算机操作系统功能。具体来说，我们表明如果只有一方配备了经过证实的执行处理器，那么在平原设置中不可能进行公平的双方硬币翻转。
•不幸的是，我们证明单个证明的执行处理器不足以完全计算一般的2方功能;
•从好的方面来说，我们证明如果双方都配备了经过验证的执行处理器，那么确实可以公平地安全地计算任何功能。
变体模型和其他结果。除了可信时钟，我们还探讨了抽象的变化及其含义 - 例如，我们比较非匿名证明和匿名证明，因为各种处理器似乎对此做出了不同的选择。
我们还探索了一个名为“透明飞地”的有趣模型[79]，由于对已知安全处理器的可能的旁道攻击，飞地内的秘密数据可能泄漏给对手，我们展示了如何实现有趣的任务，如UC-在这个较弱的模型中的安全承诺和零知识证明 - 这里我们的协议必须处理与提取和模棱两可有关的有趣技术。
1.4非目标和常见问题
多个社区从不同角度研究了可信硬件，包括如何构建安全处理器[7,28,34,39,40,57,58,60,75,81]，如何在应用程序中应用它们[13， 14,29,35,59,64,67,69-71]，侧通道和其他攻击[44,55,56,76,80,83]并防止此类攻击[40,58,81,83] 。尽管有大量文献，但加密声音的正式抽象似乎是一个重要的缺失部分，这项工作旨在朝着这个方向迈出第一步。然而，鉴于广泛的文献，关于本文的确切范围出现了几个自然但常见的问题，我们在下面讨论这些问题。
首先，虽然我们的建模基于现实的安全处理器旨在提供的内容，但我们并不打算声称任何现有的安全处理器可以实现我们的抽象。我们强调，提出这种性质的任何主张（安全处理器正确地实现任何正式规范）是正式方法和编程语言社区中积极研究的领域[39,65,66,81]，因此仍然具有挑战性开放式问题 - 更不用说一些商业安全处理器设计是封闭源的事实。
其次，一个经常被问到的问题是我们的正式抽象防御的对抗模型。这个问题的答案是特定于处理器的，因此超出了我们论文的范围 - 我们将其留给安全的处理器本身来表达它所保护的精确对抗能力。本文中的形式模型和安全定理假设对手确实局限于特定安全处理器所承担的能力。如前所述，一些处理器仅针对软件对手进行防御[34];其他人还防御物理攻击者[40-42,58];其他人则抵制一类限制类软件和/或不利用某些边线渠道的物理攻击者[2,7,57,60,75]。我们将读者引用到Shi等人的知识论文的全面系统化。 [72]用于各种安全处理器的分类和比较。
最后，我们的目标也不是提出防御侧通道攻击的新技术，或者建议如何更好地构建安全处理器 - 这些问题正在正交但互补的研究领域中探索[34,39-42,58,81,83]。
2技术路线图2.1正式建模
建模选择。为了启用加密声音推理，我们在建模中采用通用组合（UC）范例[21,22,26]。在高层次上，UC框架允许我们将复杂的加密系统抽象为简单的理想功能，从而可以模块化协议组合。 UC框架还提供通常被称为“并发组合”和“环境友好”的内容：实质上，在UC框架中证明安全的协议可以在任何环境中运行，例如1）可能同时执行的任何其他程序或协议不会影响协议π的安全性，2）协议π不会产生影响系统中其他程序和协议的不良副作用（除了那些在理想抽象中明确声明的副作用）。
更直观地说，如果涉及密码术UC的系统实现了一些理想的功能，那么程序员可以简单地对系统进行编程，假装他正在向受信任的第三方进行远程过程调用，而无需了解具体的加密实现。我们将读者引用到附录A，以获得UC框架的更详细概述。在我们开始之前，我们强调加密声音推理的重要性：相比之下，正式方法社区中的早期工作会假设加密和签名等加密原语在没有正式理由的情况下实现“最自然”的理想框 - 并且当理想的盒子实际上用密码学实例化时，已经证明这些方法是有缺陷的[3-5,10,16,24,51,53,62,63]。
正式建模的路线图。我们首先描述了一个理想的功能Gatt，它捕获了一大类经证实的执行处理器打算提供的核心抽象。我们很清楚，各种经过验证的执行处理器都有不同的设计选择 - 大多数都是实现级别的细节，并没有在抽象级别上反映出来，但是一些选择在抽象级别上很重要 - 例如安全处理器是否提供了可信时钟以及它是否实现匿名或非匿名证明。
鉴于这些差异，我们首先描述一种名为Gatt的基本匿名证明抽象，它位于现成的安全处理器的核心，如英特尔SGX [7,60]。我们在状态混淆和多方计算的背景下探索这种基本抽象的表达能力。在本文后面，我们将探讨抽象的变体，例如非匿名证明和可信时钟。因此，总之，我们的结果旨在广泛适用于广泛的安全处理器设计。
Gatt抽象。我们首先描述一个基本的Gatt抽象，捕获提供匿名证明的SGX类安全处理器的本质（参见图1）。在这里，我们简要回顾一下Gatt抽象并解释正式建模中出现的技术问题，但是将更详细的讨论推迟到第3节。
1.登记处。首先，Gatt参与了一个注册表项，该注册表项旨在捕获所有配备了经过验证的执行处理器的平台。为简单起见，我们在本文中考虑静态注册表注册。
2.有状态飞地操作。注册表reg中的平台P可以调用安全区操作，包括
•安装：使用程序prog安装新的飞地，此后称为飞地程序。安装后，Gatt只生成一个新的飞地标识符eid并返回eid。现在可以使用该包围区标识符来唯一地标识包围区实例。
•resume：恢复执行输入inp的现有飞地。在恢复调用时，Gatt在输入inp上执行prog，并获得输出outp。然后Gatt将与outp以及其他元数据一起签署prog，并返回outp和结果证明。
图1：为类似SGX的安全处理器建模的全局功能。 蓝色（和星号*）激活点表示可重入激活点。 绿色激活点最多执行一次。 飞地项目编程可能是概率性的，这对于保护隐私的应用程序非常重要。 Enclave程序输出包含在匿名证明σ中。 对于诚实的各方，该功能验证安装的安全区是否由当前协议实例的会话ID sid参数化。
每个安装的安全区都可以多次恢复，我们强调安全区操作可以跨多个恢复调用存储状态。这个有状态的属性后来证明对我们的一些应用程序很重要。
3.匿名证明。诸如SGX之类的安全处理器依赖于组签名和其他匿名凭证技术[18,19]来提供“匿名证明”。粗略地说，匿名证明允许用户验证证明是由一些经过证实的执行处理器产生的，而不是识别哪一个。为了捕获这样的匿名证明，我们的Gatt功能具有制造商公钥和密钥对（mpk，msk），并且通过签名方案Σ进行参数化。当调用安全区恢复操作时，Gatt使用签名方案Σ对使用msk证明的任何输出进行签名。粗略地说，如果在SGX中采用组签名方案，则可以将Σ视为使用“规范”签名密钥参数化的组签名方案。 Gatt在查询时向任何一方提供制造商公钥mpk - 这模拟了存在分发mpk的安全密钥分发渠道的事实。通过这种方式，任何一方都可以验证由Gatt签署的匿名证明。
全球共享功能。我们的Gatt功能基本上捕获了世界上所有经过验证的执行处理器。此外，我们强调Gatt是由所有用户，所有应用程序和所有协议全局共享的。特别是，不是为每个不同的协议实例生成不同的（mpk，msk）对，而是全局共享相同的（mpk，msk）对。
从技术上讲，我们使用具有全局设置的通用组合（GUC）范例来捕获跨协议的这种共享[22]。正如我们稍后所述，这种加密密钥的全局共享成为“不完美”的来源 - 特别是，由于共享（mpk，msk），msk从一个协议实例（即应用程序）签名的证明可能现在在一个完全不相关的协议实例中带有意义，因此引入了破坏组成的潜在不良副作用。
其他讨论和澄清。我们推迟对我们的建模选择进行更详细的讨论，更重要的是，澄清环境Z如何与Gatt进行互动在第三节中。在本文中，我们假设各方通过安全渠道互相交流。可以通过密钥交换从经过身份验证的通道实现（UC安全）安全通道。在适用的情况下，我们会针对静态损坏的情况说明我们的结果。
2.2证明执行的权力：有状态的混淆
我们证明了经过验证的执行抽象确实非常强大，正如人们所期望的那样。特别是，我们证明了经过证明的执行处理器允许我们实现一种新的抽象，我们将其称为“有状态混淆”。
定理1（非正式）。假设存在安全密钥交换协议。存在Gatt混合协议，其实现非交互式有状态混淆，这在普通设置中是不可能的，即使在假设无状态硬件令牌或虚拟黑盒安全加密混淆时也是如此。
有状态混淆允许（诚实）客户端对程序进行模糊处理并将其发送到服务器，使得服务器可以在多个输入上评估混淆程序，而混淆程序在多个调用中保持（秘密）内部状态。我们考虑有状态混淆的模拟安全概念，其中服务器应该只学习与正在回应服务器查询的有状态oracle（实现混淆程序）交互的信息。例如，有状态混淆在以下应用场景中可以是有用的原语：假设客户端（例如，医院）将敏感数据库（对应于我们希望混淆的程序）外包给配备有可信硬件的云服务器。现在，分析师可以向服务器发送统计查询并获得差异私有答案。由于每个查询都会消耗一些隐私预算，因此我们希望保证在预算耗尽后，对数据库的任何其他查询都将返回⊥。我们正式展示了如何从证明的执行处理器实现有状态的混淆。此外，如上所述，我们证明在普通设置中无法进行有状态混淆，即使假设存在无状态硬件令牌或假设虚拟黑盒安全混淆。
2.3使用单个安全处理器进行可组合的双方计算的不可能性
一个自然要问的问题是，我们是否可以实现普遍可组合（即UC安全）多方计算，这在没有任何设置假设的普通设置中是已知的 - 但是存在公共参考字符串时是可行的[ 21,23]，即为每个协议实例新近独立地以可信赖的方式生成的公共随机字符串。从表面上看，Gatt似乎提供了比普通引用字符串更强大的功能，因此很自然地期望它能够实现UC安全的多方计算。然而，经过仔细研究，我们发现，或许有些令人惊讶的是，这种直觉是微妙的错误，如下面的非正式定理所示。
定理2（非正式）。如果至少有一方未配备经过验证的执行处理器，则在没有额外设置假设的情况下（即使所有其他方都配备了经过证实的执行处理器），也无法实现UC安全多方计算。
在这里，微妙的技术性恰好源于Gatt是一个在所有用户，应用程序和协议实例之间共享的全局功能。这产生了密码学社区众所周知的不可否认性问题。由于制造商签名密钥（mpk，msk）是全局共享的，因此在一个协议实例中生成的证明可以将副作用带入另一个协议实例中。因此，向其他方发送证明的大多数自然协议候选人将允许对手通过向第三方证明证明来暗示参与协议的诚实方。此外，即使安全处理器签署匿名证明，这种不可否认性仍然存在：因为如果并非所有各方都拥有安全的处理器，那么攻击者至少可以证明Gatt注册表中的某些诚实方参与了协议，即使他无法证明哪一个。直观地说，如果所有各方都配备了安全的处理器，那么不可否认性就会消失 - 请注意，这必然意味着对手本身也必须拥有安全的处理器。由于证明是匿名的，因此对手将无法证明证明是由诚实的一方产生的，还是他只是要求他自己的本地处理器签署证明。这基本上允许诚实的一方拒绝参与协议。
提取不可能。我们将上述直觉形式化，并表明不仅发送证明的自然协议候选者遭受不可否认性，事实上，如果并非所有方都拥有安全处理器，则不可能实现UC安全多方计算。不可能性类似于在没有共同参考字符串的情况下，UC安全承诺的不可能性[23]。考虑现实世界的提交者C是否已损坏且接收者是否诚实。在这种情况下，在模拟证明期间，当真实世界C输出一个承诺时，理想世界模拟器Sim必须捕获相应的记录并提取值v commit，并将v发送到承诺理想功能Fcom。然而，如果理想世界模拟器Sim可以执行这样的提取，那么真实世界的接收器也必须能够（因为Sim没有比真实接收器更多的能力） - 这违反了承诺必须隐藏的要求。正如Canetti和Fischlin所展示的[23]，一个共同的引用字符串允许我们通过为模拟器提供更多功能来规避这种不可能性。由于公共参考字符串（CRS）是本地功能，因此在模拟期间，模拟器可以对CRS进行编程并嵌入陷门 - 这个陷门将允许模拟器执行提取。由于现实世界的接收器不具备这样的陷门，因此协议仍然保留了对真实接收器的机密性。
实际上，如果我们的Gatt功能也是本地的，我们的模拟器Sim可以用类似的方式对Gatt进行编程，并且提取很简单。然而，实际上，本地Gatt功能意味着必须为每个协议实例生成新的密钥制造商对（mpk，msk）（即，甚至对于同一用户的多个应用）。因此，本地Gatt显然无法捕获真实世界安全处理器的可重用性，这证明了为什么我们将证明的执行处理器建模为全局共享功能。
图2：可组合的双方计算：双方都有安全的处理器。 AE表示经过验证的加密。 所有ITI的激活点都是不可重入的。 当激活点被多次调用时，ITI只输出⊥。 虽然没有明确指出，如果Gatt在查询时输出，，协议将中止输出⊥。 组参数（g，p）被硬编码到prog2pc中。
不幸的是，当Gatt是全球性的时，事实证明，当提交者C被破坏并且只有接收者具有安全处理器时，从普通设置中提取的同样不可能性将继续存在。在这种情况下，模拟器Sim还必须提取从C发出的抄本提交的输入。但是，如果模拟器Sim可以执行这样的提取，那么现实世界的接收器也是如此 - 注意在这种情况下是现实世界的接收器实际上比Sim更强大，因为在注册表中的真实接收器能够有意义地调用Gatt，而模拟器Sim不能！
很容易观察到，当损坏的提交者具有安全的处理器时，这种不可能性结果不再成立 - 在这种情况下，协议可能要求提交者C将其输入发送给Gatt。由于模拟器捕获了进出C的所有成绩单，因此可以简单地提取输入。实际上，我们表明，当双方都拥有安全的处理器时，不仅承诺，而且一般的双方计算也是可能的。
2.4当两者都具有安全处理器时可组合的双方计算
定理3（非正式）。假设存在安全密钥交换协议。然后存在UC-实现F2pc的Gatt-混合协议。此外，在该协议中，所有依赖于程序的评估都在包围区内执行而不是以加密方式执行。
我们在图2中给出了一个明确的协议（为了具体，我们在协议中使用Diffie-Hellman密钥交换，尽管相同的方法扩展到任何安全密钥交换）。该协议在其仅执行O（1）（与程序无关的）加密计算的意义上是有效的；并且所有依赖程序的计算都在飞地内部进行。我们现在简要解释一下协议。
•首先，双方的安全处理器执行密钥交换并为经过身份验证的加密方案建立密钥sk。
•然后，每方的飞地用sk加密方的输入。然后，该方将得到的经过身份验证的密文ct发送给另一方。
•现在每个飞地解密ct并执行评估，并且每一方都可以查询其本地飞地以获得输出。
•大多数协议都很自然，但一种技术对于模棱两可是必要的。特别是，飞地程序的“计算”入口点有一个后门表示为v。如果v =⊥，Gatt将签署真实的评估结果并返回证明的结果。另一方面，如果v̸=⊥，飞地将简单地签名并输出v本身。在现实世界的执行中，诚实的一方将始终提供v =⊥作为飞地项目的“计算”入口点的输入。但是，正如我们稍后解释的那样，模拟器将利用此后门v来执行模糊处理并对输出进行编程。
我们现在解释在上述协议的证明中出现的一些有趣的技术问题。
•提取。首先，由于每一方将其输入直接发送到其本地飞地，因此可以进行提取。如果一方腐败，模拟器将捕获此交互，然后模拟器可以提取腐败方的输入;
•Equivocate。我们现在解释飞地程序中的后门v如何允许证明中的模棱两可。回想一下，最初，模拟器不知道诚实方的输入。为了模拟对手的诚实方的消息（其中包含来自飞地的证明），模拟器必须代表诚实的一方向Gatt发送虚拟输入以获得证明。当模拟器设法提取损坏方的输入时，它将输入发送到理想功能F2pc并获得表示为outp 的计算结果。现在，当腐败的一方查询其本地飞地的输出时，模拟器必须让Gatt签署正确的输出（通常称为模棱两可）。为了实现这一点，模拟器将利用前面提到的后门v：而不是像现实世界协议那样向Gatt发送（ct，⊥），模拟器将（ct，outp *）发送给Gatt，这样Gatt就会签名OUTP *。
•关于匿名证明的说明。有趣的是要注意我们的协议如何依赖于安全性的匿名证明。具体来说，在证明中，模拟器需要为对手A模拟诚实方的消息。为此，模拟器将自己模拟最好的一方的飞地（即对手的）安全处理器 - 这样的模拟是可能是因为Gatt返回的证明是匿名的。如果证明不是匿名的（例如，绑定到该方的标识符），则模拟器将无法模拟诚实方的飞地（有关更多讨论，请参阅第8.4节）。
2.5用最小的全局设置来规避不可能性
实际上，如果我们能够在存在单个证明的执行处理器的情况下允许可组合的多方计算，那么显然是可取的。作为期望的用例，想象多个客户端（例如，医院），每个客户端具有敏感数据（例如，医疗记录），其希望对其联合数据执行一些计算（例如，用于临床研究的数据挖掘）。此外，他们希望将数据和计算外包给不受信任的第三方云提供商。具体而言，客户端可能没有安全处理器，但只要云服务器执行，我们希望允许外包安全多方计算。
我们现在演示如何引入最小的全局设置假设来规避这种不可能性。具体来说，我们将利用全局增强公共参考字符串（ACRS）[22]，此后表示为Gacrs。虽然Gacrs知道UC安全多方计算的可行性，即使没有安全处理器[22]，但现有协议涉及在程序运行时（至少）线性的加密计算。我们的目标是演示一个实用的协议，在安全区域内执行任何与程序相关的计算，并且只执行O（1）加密计算。
定理4（非正式）。假设存在安全密钥交换协议。然后，存在（Gacrs，Gatt） - 混合协议，UC实现Fmpc并且仅使用单个安全处理器。此外，该协议在安全处理器的包围区内执行所有与程序相关的计算（而不是加密）。
最小的全局设置Gacrs。为了理解这个结果，我们首先解释最小的全局设置Gacrs。首先，Gacrs提供全局公共引用字符串。其次，Gacrs还允许每个（损坏的）方P为自己查询身份密钥。通过使用全局主密钥对该方的标识符P进行签名来计算该身份密钥。请注意，这样的全局设置很小，因为诚实的各方永远不必查询其身份密钥。身份密钥只是提供给腐败方的后门。虽然初看起来向对手提供后门似乎是违反直觉的，但请注意，这个后门也提供给我们的模拟器 - 这增加了模拟器的功能，使我们能够规避前面提到的不可能性和设计诚实方可以拒绝参与的协议。
MPC具有单个安全处理器和Gacrs。我们考虑使用配备安全处理器的服务器以及没有安全处理器的多个客户端进行设置。
让我们首先关注服务器和客户端子集损坏时（更有趣）的情况。关键问题是如何在Gacrs的帮助下解决提取的不可能性 - 更具体地说，模拟器如何提取腐败客户的输入？我们的想法如下 - 为了方便读者，我们在向技术细节进行解释时跳过并提出图3中的详细协议，但我们将重新审视它并在第6节中提供正式的符号和证明。
图3：使用单个安全处理器的可组合多方计算。ψ（P，msg，σ）输出一个元组（msg，C，π），其中π是证明无法区分的证明，密文C加密msg上的有效证明σ，或加密P的身份密钥。 PKE和AE分别表示公钥加密和认证加密。 符号发送表示通过安全信道发送的消息。
paper 15.----22.
3.1
3.2
