摘要
現(xiàn)實(shí)的安全處理器，包括為學(xué)術(shù)和商業(yè)目的而構(gòu)建的處理器袜瞬，通常實(shí)現(xiàn)“證明執(zhí)行”抽象。盡管是現(xiàn)代安全處理器的事實(shí)上的標(biāo)準(zhǔn)身堡，但“證明執(zhí)行”抽象還沒有得到足夠的正式處理邓尤。我們?yōu)椤白C明執(zhí)行”的安全處理器提供正式的抽象，并嚴(yán)格探索其表達(dá)能力贴谎。我們的探索既展示了預(yù)期汞扎，也展示了令人驚訝的結(jié)果。
一方面赴精，我們表明佩捞，就像普遍的看法一樣，證明執(zhí)行非常強(qiáng)大蕾哟，并且允許人們實(shí)現(xiàn)強(qiáng)大的加密抽象一忱，例如有狀態(tài)的反映，即使在假設(shè)虛擬黑盒混淆和無狀態(tài)硬件令牌時(shí)谭确，其存在也是不可能的帘营。另一方面，我們驚訝地發(fā)現(xiàn)逐哈，使用經(jīng)過驗(yàn)證的執(zhí)行處理器實(shí)現(xiàn)可用的雙方計(jì)算并不像人們預(yù)期的那樣簡單芬迄。具體來說，只有當(dāng)雙方都配備了安全處理器時(shí)昂秃，我們才能實(shí)現(xiàn)可組合的雙方計(jì)算禀梳。如果其中一方?jīng)]有安全處理器，我們就表明無法進(jìn)行可組合的雙方計(jì)算肠骆。然而算途，在實(shí)踐中，期望允許多個(gè)傳統(tǒng)客戶端（沒有安全處理器）利用服務(wù)器的安全處理器來執(zhí)行多方計(jì)算任務(wù)蚀腿。我們將展示如何引入最少的額外設(shè)置假設(shè)來實(shí)現(xiàn)這一點(diǎn)嘴瓤。最后，我們表明，如果安全處理器沒有可信時(shí)鐘廓脆，那么一般功能的公平多方計(jì)算是不可能的筛谚。當(dāng)安全處理器具有可信時(shí)鐘時(shí)，如果雙方都配備了安全處理器停忿，我們就可以實(shí)現(xiàn)公平的雙方計(jì)算驾讲。但如果只有一方擁有安全的處理器（帶有可信時(shí)鐘），那么對(duì)于一般功能來說瞎嬉，公平性仍然是不可能的蝎毡。
1.介紹
網(wǎng)絡(luò)安全科學(xué)建立在一個(gè)基本的指導(dǎo)原則之上厚柳，即最小化系統(tǒng)的可信計(jì)算基礎(chǔ)（TCB）[78]氧枣。由于在實(shí)踐中特別是在遺留系統(tǒng)存在的情況下?lián)碛小巴昝馈避浖欠浅＠щy的，因此架構(gòu)社區(qū)提出了一種新的范例來從可信硬件（以下也稱為安全處理器）引導(dǎo)系統(tǒng)的安全性别垮。粗略地說便监，安全處理器旨在將敏感應(yīng)用程序的可信計(jì)算基礎(chǔ)僅減少到處理器本身（可能與最小軟件TCB（例如安全管理程序）結(jié)合）。特別是碳想，除了自身之外烧董，敏感應(yīng)用程序（例如，銀行應(yīng)用程序）不應(yīng)該信任任何其他軟件堆棧（包括操作系統(tǒng)胧奔，驅(qū)動(dòng)程序和其他應(yīng)用程序）來維護(hù)任務(wù)的機(jī)密性或完整性 - 關(guān)鍵數(shù)據(jù)（例如逊移，密碼或信用卡號(hào)）。即使軟件堆椓睿可能受到危害胳泉，安全性也會(huì)保留（只要敏感應(yīng)用程序本身完好無損）。除了軟件對(duì)手之外岩遗，一些安全的處理器也使其成為防御物理攻擊者的目標(biāo)扇商。特別是，即使對(duì)手（例如宿礁，云服務(wù)提供商的流氓員工或系統(tǒng)管理員）具有對(duì)計(jì)算平臺(tái)的物理訪問權(quán)并且可能能夠窺探或篡改內(nèi)存或系統(tǒng)總線案铺，他也不應(yīng)該收獲秘密信息或破壞程序的執(zhí)行。
通常認(rèn)為可信硬件為構(gòu)建安全系統(tǒng)提供了非常強(qiáng)大的抽象梆靖。潛在的應(yīng)用很多控汉，從云計(jì)算[13,35,59,69,70]，移動(dòng)安全[68]返吻，網(wǎng)絡(luò)安全到加密貨幣[82]姑子。在過去的三十年中，學(xué)術(shù)界和工業(yè)界已經(jīng)提出并證明了許多安全處理器[7,28,34,39,40,57,58,60,74,81];其中一些已經(jīng)商業(yè)化思喊，包括眾所周知的可信平臺(tái)模塊（TPM）[2]壁酬，Arm's TrustZone [6,8]等。值得注意的是，英特爾最近發(fā)布了名為SGX [7,33,60]的新型x86安全擴(kuò)展舆乔，引發(fā)了廣泛的興趣岳服，以構(gòu)建利用新興可信硬件產(chǎn)品的新型防彈系統(tǒng)。
1.1證明執(zhí)行安全處理器
雖然有許多關(guān)于可信硬件設(shè)計(jì)的建議希俩，但這些設(shè)計(jì)在架構(gòu)選擇吊宋，指令集，實(shí)現(xiàn)細(xì)節(jié)颜武，加密套件以及它們承諾防御的對(duì)抗模型方面差別很大 - 令人驚訝的是璃搜，它看起來不知何故大多數(shù)這些處理器已經(jīng)融合在一起提供了一個(gè)通用的抽象，從此被稱為證明的執(zhí)行抽象[2,7,34,60,74,77]鳞上。粗略地說这吻，一個(gè)經(jīng)過證實(shí)的執(zhí)行抽象實(shí)現(xiàn)了以下功能：
?配備有經(jīng)過驗(yàn)證的執(zhí)行處理器的平臺(tái)可以將程序和輸入（此后表示為（prog，inp））發(fā)送到其本地安全處理器篙议。安全處理器將通過輸入執(zhí)行程序唾糯，并計(jì)算outp：= prog（inp）。然后鬼贱，安全處理器將使用秘密簽名密鑰對(duì)元組（prog移怯，outp）進(jìn)行簽名以獲得數(shù)字簽名σ - 實(shí)際上，在簽名之前應(yīng)用散列函數(shù)这难。特別地舟误，該簽名σ通常被稱為“證明”，因此該整個(gè)執(zhí)行被稱為“證明執(zhí)行”姻乓。
?上述程序的執(zhí)行是在沙盒環(huán)境中進(jìn)行的（因此稱為飛地）嵌溢，因?yàn)檐浖?duì)手或物理對(duì)手不能篡改執(zhí)行，或檢查生活在其中的數(shù)據(jù)糖权。飛地堵腹。這對(duì)于實(shí)現(xiàn)隱私保護(hù)應(yīng)用程序非常重要。例如星澳，知道安全處理器的公鑰的遠(yuǎn)程客戶端可以與駐留在遠(yuǎn)程服務(wù)器S上的安全處理器建立安全信道疚顷。然后，客戶端可以將加密和認(rèn)證的數(shù)據(jù)（和/或程序）發(fā)送到安全處理器 - 同時(shí)消息通過中介S傳遞禁偎，S不能竊聽內(nèi)容腿堤，也不能篡改通信。
?最后如暖，各種安全處理器在如何實(shí)現(xiàn)上述安全沙盒機(jī)制方面做出了不同的具體選擇 - 這些選擇與安全處理器試圖防范的對(duì)抗能力密切相關(guān)笆檀。例如，粗略地說盒至，英特爾的SGX技術(shù)[7,60]針對(duì)的是受限制的軟件對(duì)手酗洒，它不會(huì)測(cè)量時(shí)序或其他可能的側(cè)通道士修，也不會(huì)觀察到飛地應(yīng)用程序的頁面交換行為（例如，飛地應(yīng)用程序）使用小內(nèi)存或設(shè)計(jì)數(shù)據(jù) - 遺忘）;它還可以防御能夠竊聽內(nèi)存的受限物理攻擊者樱衷，但無法點(diǎn)擊內(nèi)存總線上的地址或測(cè)量側(cè)信道信息（如時(shí)序和功耗）棋嘲。
我們將讀者推薦給Shi等人。 [72]用于可信硬件的通用介紹矩桂，以及各種安全處理器所做出的不同選擇的綜合比較沸移。
架構(gòu)社區(qū)已經(jīng)融合到“證明執(zhí)行”抽象的事實(shí)是有趣的。究竟如何成為事實(shí)上的抽象超出了本文的范圍侄榴，但有助于觀察證明的執(zhí)行抽象在實(shí)踐中具有成本效益雹锣，具體如下：
?通用：經(jīng)過證實(shí)的執(zhí)行抽象支持在安全區(qū)域內(nèi)計(jì)算通用的，用戶定義的程序癞蚕，因此可以實(shí)現(xiàn)廣泛的應(yīng)用程序;
?可重用性：它允許單個(gè)可信硬件令牌被多個(gè)應(yīng)用程序和世界上的每個(gè)人重用 - 有趣的是蕊爵，事實(shí)證明這種可重用性實(shí)際上產(chǎn)生了許多技術(shù)問題，將在本文后面討論;
?誠信和隱私：它提供完整性和隱私保障涣达。特別地在辆，盡管配備有可信硬件的平臺(tái)P在與可信硬件的每次交互中服務(wù)于中介，但是可以通過使遠(yuǎn)程用戶與安全處理器建立安全信道來引導(dǎo)隱私保證度苔。
在本文的其余部分，每當(dāng)我們使用術(shù)語“安全處理器”或“可信硬件”時(shí)浑度，除非另有說明寇窑，否則我們特別指的是證明執(zhí)行安全處理器。
1.2為什么安全處理器的正式抽象箩张？
雖然證明執(zhí)行已被社區(qū)接受為事實(shí)上的標(biāo)準(zhǔn)甩骏，但據(jù)我們所知，沒有人探討過以下基本問題：
1.準(zhǔn)確而正式地先慷，證明的執(zhí)行抽象是什么饮笛？
2.什么可以證明執(zhí)行表達(dá)，什么不能表達(dá)论熙？
如果我們能夠正式而準(zhǔn)確地闡明這些問題的答案福青，那么這些好處就可以廣泛傳播。它至少可以通過以下方式幫助生產(chǎn)者和可信硬件的消費(fèi)者：
?了解抽象的變化是否會(huì)導(dǎo)致表達(dá)能力的差異脓诡。首先无午，各種安全處理器可能提供類似但略有不同的抽象 - 這些差異是否與可信硬件的表現(xiàn)力有關(guān)？如果我們希望為安全處理器添加特定功能（例如祝谚，時(shí)序）宪迟，此功能是否會(huì)增加其表現(xiàn)力？
?正式使用可信硬件交惯。許多工作已經(jīng)證明了如何使用可信硬件來構(gòu)建各種安全系統(tǒng)[13,14,29,35,59,64,67,69-71]次泽。不幸的是穿仪，由于可信硬件提供的精確抽象甚至不清楚，大多數(shù)現(xiàn)有工作采用的方法范圍從啟發(fā)式安全到半正式推理意荤。
此外牡借，大多數(shù)已知的安全處理器暴露與密碼相關(guān)的指令（例如，涉及哈希鏈或數(shù)字簽名[2,7,33,60]）袭异，這使可信硬件的編程變得混淆 - 特別是钠龙，程序員基本上必須設(shè)計(jì)加密協(xié)議以利用可信硬件。很明顯御铃，用戶友好的高級(jí)編程抽象隱藏了加密細(xì)節(jié)將是非常需要的碴里，并且可能是可信硬件編程民主化的關(guān)鍵（事實(shí)上，通常是安全工程） - 然而上真，如果沒有準(zhǔn)確地表達(dá)可信硬件提供的正式抽象咬腋，顯然不可能在頂部構(gòu)建正式的正確的高級(jí)編程抽象。
?邁向正式安全的可信硬件睡互。最后根竿，了解可信硬件的“良好”抽象是什么，可以為可信硬件的設(shè)計(jì)者和制造商提供有用的反饋就珠。圣杯將是設(shè)計(jì)和實(shí)施正式安全的處理器寇壳。了解要實(shí)現(xiàn)的加密級(jí)正式抽象是實(shí)現(xiàn)這一長期目標(biāo)的必要的第一步 - 但實(shí)現(xiàn)這一目標(biāo)顯然需要額外的，互補(bǔ)的技術(shù)和機(jī)制妻怎，例如在正式方法社區(qū)中開發(fā)的那些[39壳炎， 65,66,81]，這可能使我們能夠確保實(shí)際的安全處理器實(shí)現(xiàn)符合規(guī)范逼侦。
1.3我們的貢獻(xiàn)摘要
據(jù)我們所知匿辩，我們是第一個(gè)為實(shí)際的，經(jīng)過證實(shí)的執(zhí)行安全處理器調(diào)查加密聲音和可組合的正式抽象的人榛丢。我們的研究結(jié)果證明了“預(yù)期”和（可能）“令人驚訝”铲球。
預(yù)期和令人驚訝的。一方面晰赞，我們證明了經(jīng)過驗(yàn)證的執(zhí)行處理器確實(shí)非常強(qiáng)大稼病，正如人們所期望的那樣，并且允許我們實(shí)現(xiàn)原語宾肺，否則即使在采用無狀態(tài)硬件令牌或虛擬黑盒安全加密混淆時(shí)也是不可能的溯饵。
另一方面，我們的調(diào)查揭示了在沒有正式建模的情況下可能容易被忽視的微妙技術(shù)細(xì)節(jié)锨用，我們得出了一些可能最初令人驚訝的結(jié)論（當(dāng)然丰刊，事后看來很自然）。例如增拥，
?我們表明啄巧，如果一方?jīng)]有這樣一個(gè)安全的處理器（而另一方就是這樣）寻歧，那么普遍可以組合的雙方計(jì)算是不可能的。
這對(duì)我們來說最初是令人驚訝的秩仆，因?yàn)槲覀兺ǔＵJ(rèn)為一個(gè)經(jīng)過證實(shí)的執(zhí)行處理器提供了一個(gè)可以計(jì)算通用的码泛，用戶定義的程序的“無所不能”的可信第三方。當(dāng)存在這樣的可信第三方時(shí)澄耍，似乎可以安全且非交互地評(píng)估任何功能噪珊，從而隱藏程序和數(shù)據(jù)。解釋我們的發(fā)現(xiàn)的一種方法是齐莲，這種直覺在技術(shù)上是不精確和假設(shè)的危險(xiǎn) - 雖然證明執(zhí)行處理器確實(shí)接近提供這種“可信第三方”理想抽象痢站，但有些方面對(duì)于這種理想的抽象是“不完美的”，不應(yīng)該被忽視选酗，并且必須采用嚴(yán)格的方法來正式使用可信硬件阵难。
多方計(jì)算的其他結(jié)果。我們還顯示以下結(jié)果：
?普遍適用的雙方計(jì)算可能會(huì)在任何一個(gè)配備了經(jīng)過驗(yàn)證的執(zhí)行處理器的情況下進(jìn)行芒填。我們給出了一個(gè)明確的結(jié)構(gòu)呜叫，并表明其設(shè)計(jì)和證明中有幾個(gè)有趣的技術(shù)（我們將很快評(píng)論）。處理這些技術(shù)細(xì)節(jié)也證明了一個(gè)可證明安全的協(xié)議候選者在重要細(xì)節(jié)上與最自然的協(xié)議候選者[49,64,70]從業(yè)人員會(huì)采用（不知道具有可證明的可組合安全性）的區(qū)別殿衰。這證實(shí)了正式建模和可證明安全性的重要性朱庆。
?盡管即使單方?jīng)]有安全的處理器也不可能進(jìn)行多方計(jì)算，但實(shí)際上仍然需要構(gòu)建多方應(yīng)用程序播玖，其中多個(gè)可能的舊客戶端將數(shù)據(jù)和計(jì)算外包給配備有單個(gè)云服務(wù)器的單個(gè)云服務(wù)器安全的處理器椎工。
我們展示了如何引入最小的全局設(shè)置假設(shè) - 更具體地說，通過采用全局?jǐn)U充公共參考字符串[22]（以下稱為Gacrs） - 來規(guī)避這種不可能性蜀踏。盡管即使沒有安全處理器[22]，Gacrs也知道通用UC安全MPC的理論可??行性掰吕，但是現(xiàn)有結(jié)構(gòu)涉及在要安全評(píng)估的程序的運(yùn)行時(shí)間中（至少）線性的加密計(jì)算果覆。相比之下，我們對(duì)僅涉及O（1）量的加密計(jì)算的實(shí)際構(gòu)造特別感興趣殖熟，而是在安全處理器內(nèi)執(zhí)行所有與程序相關(guān)的計(jì)算（而不是加密）局待。
技術(shù)。我們的結(jié)構(gòu)中出現(xiàn)了一些有趣的技術(shù)問題菱属。首先钳榨，組合式校樣通常要求模擬器攔截和修改與對(duì)手（和環(huán)境）之間的通信，以便對(duì)手無法區(qū)分它是與模擬器或現(xiàn)實(shí)世界的誠實(shí)方和安全處理器對(duì)話纽门。由于模擬器不知道誠實(shí)方的輸入（超出計(jì)算輸出所泄露的輸入）薛耻，由于不可分辨性，可以得出結(jié)論赏陵，對(duì)手也不能知道誠實(shí)的各方輸入饼齿。
?等同饲漾。我們的模擬器執(zhí)行此類模擬的能力受到安全處理器簽署證據(jù)的證據(jù)的阻礙 - 因?yàn)槟M器不具有秘密簽名密鑰，它不能修改這些消息并且必須直接將它們轉(zhuǎn)發(fā)給對(duì)手缕溉。要解決這個(gè)問題需要新的技術(shù)來執(zhí)行模棱兩可考传，這是標(biāo)準(zhǔn)協(xié)議組合證明中出現(xiàn)的技術(shù)性問題。為了實(shí)現(xiàn)模棱兩可证鸥，我們提出了在飛地項(xiàng)目中設(shè)置特殊后門的新技術(shù)僚楞。必須精心設(shè)計(jì)這樣的后門，以便它們?yōu)槟M器提供更多的動(dòng)力枉层，而不會(huì)給現(xiàn)實(shí)世界的對(duì)手額外的力量泉褐。通過這種方式，我們可以充分利用這兩個(gè)方面：1）誠實(shí)方的安全不會(huì)在實(shí)際執(zhí)行中受到傷害; 2）證明中的模擬器可以“編程”飛地應(yīng)用程序以簽署其選擇的任何輸出返干，只要它能夠展示正確的陷門兴枯。在幾乎所有的協(xié)議中，該技術(shù)以不同的形式重復(fù)使用矩欠。
?提取财剖。提取是協(xié)議組合證明中常見的另一個(gè)技術(shù)問題。這個(gè)技術(shù)問題最有趣的表現(xiàn)形式是我們的協(xié)議癌淮，它在全局公共參考字符串（Gacrs）和單個(gè)安全處理器（參見第6節(jié)）的情況下實(shí)現(xiàn)多方計(jì)算躺坟。在這里，我們?cè)俅卫迷陲w地計(jì)劃中種植特殊后門的想法來允許這樣的提取乳蓄。具體而言咪橙，當(dāng)提供一方的正確身份密鑰時(shí)，飛地程序?qū)⑿孤对摲綄?duì)呼叫者的輸入虚倒。誠實(shí)的參與方安全不會(huì)受到這個(gè)后門的傷害美侦，因?yàn)闆]有人在現(xiàn)實(shí)世界中學(xué)習(xí)誠實(shí)黨派的身份證，甚至連誠實(shí)黨派本身都沒有。然而，在模擬中种远，模擬器學(xué)習(xí)腐敗方的身份密鑰气破，因此它可以提取腐敗方的輸入。
值得信賴的時(shí)鐘和公平。最后，我們正式證明了抽象的差異如何導(dǎo)致表達(dá)能力的差異。特別是棺妓，許多安全處理器提供可信時(shí)鐘，我們?cè)诠降碾p方計(jì)算環(huán)境中探索這種可信時(shí)鐘的表現(xiàn)力炮赦。眾所周知怜跑，在標(biāo)準(zhǔn)設(shè)置中，一般功能的雙方計(jì)算中不可能存在公平性[32]眼五。然而妆艘，最近的一些研究表明彤灶，一般功能的不可能性并不意味著每種功能都是不可能的 - 有趣的是，存在一類可以在普通環(huán)境中公平計(jì)算的功能[9,46,47]批旺。我們?cè)谧C明的執(zhí)行處理器的背景下演示了幾個(gè)有趣的發(fā)現(xiàn)：
?首先幌陕，甚至比普通環(huán)境更公平地執(zhí)行計(jì)算機(jī)操作系統(tǒng)功能。具體來說汽煮，我們表明如果只有一方配備了經(jīng)過證實(shí)的執(zhí)行處理器搏熄，那么在平原設(shè)置中不可能進(jìn)行公平的雙方硬幣翻轉(zhuǎn)。
?不幸的是暇赤，我們證明單個(gè)證明的執(zhí)行處理器不足以完全計(jì)算一般的2方功能;
?從好的方面來說心例，我們證明如果雙方都配備了經(jīng)過驗(yàn)證的執(zhí)行處理器，那么確實(shí)可以公平地安全地計(jì)算任何功能鞋囊。
變體模型和其他結(jié)果止后。除了可信時(shí)鐘，我們還探討了抽象的變化及其含義 - 例如溜腐，我們比較非匿名證明和匿名證明译株，因?yàn)楦鞣N處理器似乎對(duì)此做出了不同的選擇。
我們還探索了一個(gè)名為“透明飛地”的有趣模型[79]挺益，由于對(duì)已知安全處理器的可能的旁道攻擊歉糜，飛地內(nèi)的秘密數(shù)據(jù)可能泄漏給對(duì)手，我們展示了如何實(shí)現(xiàn)有趣的任務(wù)望众，如UC-在這個(gè)較弱的模型中的安全承諾和零知識(shí)證明 - 這里我們的協(xié)議必須處理與提取和模棱兩可有關(guān)的有趣技術(shù)匪补。
1.4非目標(biāo)和常見問題
多個(gè)社區(qū)從不同角度研究了可信硬件，包括如何構(gòu)建安全處理器[7,28,34,39,40,57,58,60,75,81]烂翰，如何在應(yīng)用程序中應(yīng)用它們[13夯缺， 14,29,35,59,64,67,69-71]，側(cè)通道和其他攻擊[44,55,56,76,80,83]并防止此類攻擊[40,58,81,83] 甘耿。盡管有大量文獻(xiàn)喳逛，但加密聲音的正式抽象似乎是一個(gè)重要的缺失部分，這項(xiàng)工作旨在朝著這個(gè)方向邁出第一步棵里。然而，鑒于廣泛的文獻(xiàn)姐呐，關(guān)于本文的確切范圍出現(xiàn)了幾個(gè)自然但常見的問題殿怜，我們?cè)谙旅嬗懻撨@些問題。
首先曙砂，雖然我們的建耐访眨基于現(xiàn)實(shí)的安全處理器旨在提供的內(nèi)容，但我們并不打算聲稱任何現(xiàn)有的安全處理器可以實(shí)現(xiàn)我們的抽象鸠澈。我們強(qiáng)調(diào)柱告，提出這種性質(zhì)的任何主張（安全處理器正確地實(shí)現(xiàn)任何正式規(guī)范）是正式方法和編程語言社區(qū)中積極研究的領(lǐng)域[39,65,66,81]截驮，因此仍然具有挑戰(zhàn)性開放式問題 - 更不用說一些商業(yè)安全處理器設(shè)計(jì)是封閉源的事實(shí)。
其次际度，一個(gè)經(jīng)常被問到的問題是我們的正式抽象防御的對(duì)抗模型葵袭。這個(gè)問題的答案是特定于處理器的，因此超出了我們論文的范圍 - 我們將其留給安全的處理器本身來表達(dá)它所保護(hù)的精確對(duì)抗能力乖菱。本文中的形式模型和安全定理假設(shè)對(duì)手確實(shí)局限于特定安全處理器所承擔(dān)的能力坡锡。如前所述，一些處理器僅針對(duì)軟件對(duì)手進(jìn)行防御[34];其他人還防御物理攻擊者[40-42,58];其他人則抵制一類限制類軟件和/或不利用某些邊線渠道的物理攻擊者[2,7,57,60,75]窒所。我們將讀者引用到Shi等人的知識(shí)論文的全面系統(tǒng)化鹉勒。 [72]用于各種安全處理器的分類和比較。
最后吵取，我們的目標(biāo)也不是提出防御側(cè)通道攻擊的新技術(shù)禽额，或者建議如何更好地構(gòu)建安全處理器 - 這些問題正在正交但互補(bǔ)的研究領(lǐng)域中探索[34,39-42,58,81,83]。
2技術(shù)路線圖2.1正式建模
建模選擇皮官。為了啟用加密聲音推理脯倒，我們?cè)诮Ｖ胁捎猛ㄓ媒M合（UC）范例[21,22,26]。在高層次上臣疑，UC框架允許我們將復(fù)雜的加密系統(tǒng)抽象為簡單的理想功能盔憨，從而可以模塊化協(xié)議組合。 UC框架還提供通常被稱為“并發(fā)組合”和“環(huán)境友好”的內(nèi)容：實(shí)質(zhì)上讯沈，在UC框架中證明安全的協(xié)議可以在任何環(huán)境中運(yùn)行郁岩，例如1）可能同時(shí)執(zhí)行的任何其他程序或協(xié)議不會(huì)影響協(xié)議π的安全性，2）協(xié)議π不會(huì)產(chǎn)生影響系統(tǒng)中其他程序和協(xié)議的不良副作用（除了那些在理想抽象中明確聲明的副作用）缺狠。
更直觀地說问慎，如果涉及密碼術(shù)UC的系統(tǒng)實(shí)現(xiàn)了一些理想的功能，那么程序員可以簡單地對(duì)系統(tǒng)進(jìn)行編程挤茄，假裝他正在向受信任的第三方進(jìn)行遠(yuǎn)程過程調(diào)用如叼，而無需了解具體的加密實(shí)現(xiàn)。我們將讀者引用到附錄A穷劈，以獲得UC框架的更詳細(xì)概述笼恰。在我們開始之前，我們強(qiáng)調(diào)加密聲音推理的重要性：相比之下歇终，正式方法社區(qū)中的早期工作會(huì)假設(shè)加密和簽名等加密原語在沒有正式理由的情況下實(shí)現(xiàn)“最自然”的理想框 - 并且當(dāng)理想的盒子實(shí)際上用密碼學(xué)實(shí)例化時(shí)社证，已經(jīng)證明這些方法是有缺陷的[3-5,10,16,24,51,53,62,63]。
正式建模的路線圖评凝。我們首先描述了一個(gè)理想的功能Gatt追葡，它捕獲了一大類經(jīng)證實(shí)的執(zhí)行處理器打算提供的核心抽象。我們很清楚，各種經(jīng)過驗(yàn)證的執(zhí)行處理器都有不同的設(shè)計(jì)選擇 - 大多數(shù)都是實(shí)現(xiàn)級(jí)別的細(xì)節(jié)宜肉，并沒有在抽象級(jí)別上反映出來匀钧，但是一些選擇在抽象級(jí)別上很重要 - 例如安全處理器是否提供了可信時(shí)鐘以及它是否實(shí)現(xiàn)匿名或非匿名證明。
鑒于這些差異谬返，我們首先描述一種名為Gatt的基本匿名證明抽象之斯，它位于現(xiàn)成的安全處理器的核心，如英特爾SGX [7,60]朱浴。我們?cè)跔顟B(tài)混淆和多方計(jì)算的背景下探索這種基本抽象的表達(dá)能力吊圾。在本文后面，我們將探討抽象的變體翰蠢，例如非匿名證明和可信時(shí)鐘项乒。因此，總之梁沧，我們的結(jié)果旨在廣泛適用于廣泛的安全處理器設(shè)計(jì)檀何。
Gatt抽象。我們首先描述一個(gè)基本的Gatt抽象廷支，捕獲提供匿名證明的SGX類安全處理器的本質(zhì)（參見圖1）频鉴。在這里，我們簡要回顧一下Gatt抽象并解釋正式建模中出現(xiàn)的技術(shù)問題恋拍，但是將更詳細(xì)的討論推遲到第3節(jié)垛孔。
1.登記處。首先施敢，Gatt參與了一個(gè)注冊(cè)表項(xiàng)周荐，該注冊(cè)表項(xiàng)旨在捕獲所有配備了經(jīng)過驗(yàn)證的執(zhí)行處理器的平臺(tái)。為簡單起見僵娃，我們?cè)诒疚闹锌紤]靜態(tài)注冊(cè)表注冊(cè)概作。
2.有狀態(tài)飛地操作。注冊(cè)表reg中的平臺(tái)P可以調(diào)用安全區(qū)操作默怨，包括
?安裝：使用程序prog安裝新的飛地讯榕，此后稱為飛地程序。安裝后匙睹，Gatt只生成一個(gè)新的飛地標(biāo)識(shí)符eid并返回eid∮奁ǎ現(xiàn)在可以使用該包圍區(qū)標(biāo)識(shí)符來唯一地標(biāo)識(shí)包圍區(qū)實(shí)例。
?resume：恢復(fù)執(zhí)行輸入inp的現(xiàn)有飛地痕檬。在恢復(fù)調(diào)用時(shí)集绰，Gatt在輸入inp上執(zhí)行prog，并獲得輸出outp谆棺。然后Gatt將與outp以及其他元數(shù)據(jù)一起簽署prog，并返回outp和結(jié)果證明。
圖1：為類似SGX的安全處理器建模的全局功能改淑。 藍(lán)色（和星號(hào)*）激活點(diǎn)表示可重入激活點(diǎn)碍岔。 綠色激活點(diǎn)最多執(zhí)行一次。 飛地項(xiàng)目編程可能是概率性的朵夏，這對(duì)于保護(hù)隱私的應(yīng)用程序非常重要蔼啦。 Enclave程序輸出包含在匿名證明σ中。 對(duì)于誠實(shí)的各方仰猖，該功能驗(yàn)證安裝的安全區(qū)是否由當(dāng)前協(xié)議實(shí)例的會(huì)話ID sid參數(shù)化捏肢。
每個(gè)安裝的安全區(qū)都可以多次恢復(fù)，我們強(qiáng)調(diào)安全區(qū)操作可以跨多個(gè)恢復(fù)調(diào)用存儲(chǔ)狀態(tài)饥侵。這個(gè)有狀態(tài)的屬性后來證明對(duì)我們的一些應(yīng)用程序很重要鸵赫。
3.匿名證明。諸如SGX之類的安全處理器依賴于組簽名和其他匿名憑證技術(shù)[18,19]來提供“匿名證明”躏升。粗略地說辩棒，匿名證明允許用戶驗(yàn)證證明是由一些經(jīng)過證實(shí)的執(zhí)行處理器產(chǎn)生的，而不是識(shí)別哪一個(gè)膨疏。為了捕獲這樣的匿名證明一睁，我們的Gatt功能具有制造商公鑰和密鑰對(duì)（mpk，msk）佃却，并且通過簽名方案Σ進(jìn)行參數(shù)化者吁。當(dāng)調(diào)用安全區(qū)恢復(fù)操作時(shí)，Gatt使用簽名方案Σ對(duì)使用msk證明的任何輸出進(jìn)行簽名饲帅。粗略地說复凳，如果在SGX中采用組簽名方案，則可以將Σ視為使用“規(guī)范”簽名密鑰參數(shù)化的組簽名方案洒闸。 Gatt在查詢時(shí)向任何一方提供制造商公鑰mpk - 這模擬了存在分發(fā)mpk的安全密鑰分發(fā)渠道的事實(shí)染坯。通過這種方式，任何一方都可以驗(yàn)證由Gatt簽署的匿名證明丘逸。
全球共享功能单鹿。我們的Gatt功能基本上捕獲了世界上所有經(jīng)過驗(yàn)證的執(zhí)行處理器。此外深纲，我們強(qiáng)調(diào)Gatt是由所有用戶仲锄，所有應(yīng)用程序和所有協(xié)議全局共享的。特別是湃鹊，不是為每個(gè)不同的協(xié)議實(shí)例生成不同的（mpk儒喊，msk）對(duì)，而是全局共享相同的（mpk币呵，msk）對(duì)怀愧。
從技術(shù)上講侨颈，我們使用具有全局設(shè)置的通用組合（GUC）范例來捕獲跨協(xié)議的這種共享[22]。正如我們稍后所述芯义，這種加密密鑰的全局共享成為“不完美”的來源 - 特別是哈垢，由于共享（mpk，msk）扛拨，msk從一個(gè)協(xié)議實(shí)例（即應(yīng)用程序）簽名的證明可能現(xiàn)在在一個(gè)完全不相關(guān)的協(xié)議實(shí)例中帶有意義耘分，因此引入了破壞組成的潛在不良副作用。
其他討論和澄清绑警。我們推遲對(duì)我們的建模選擇進(jìn)行更詳細(xì)的討論求泰，更重要的是，澄清環(huán)境Z如何與Gatt進(jìn)行互動(dòng)在第三節(jié)中计盒。在本文中渴频，我們假設(shè)各方通過安全渠道互相交流≌掠簦可以通過密鑰交換從經(jīng)過身份驗(yàn)證的通道實(shí)現(xiàn)（UC安全）安全通道枉氮。在適用的情況下，我們會(huì)針對(duì)靜態(tài)損壞的情況說明我們的結(jié)果暖庄。
2.2證明執(zhí)行的權(quán)力：有狀態(tài)的混淆
我們證明了經(jīng)過驗(yàn)證的執(zhí)行抽象確實(shí)非常強(qiáng)大聊替，正如人們所期望的那樣。特別是培廓，我們證明了經(jīng)過證明的執(zhí)行處理器允許我們實(shí)現(xiàn)一種新的抽象惹悄，我們將其稱為“有狀態(tài)混淆”。
定理1（非正式）肩钠。假設(shè)存在安全密鑰交換協(xié)議泣港。存在Gatt混合協(xié)議，其實(shí)現(xiàn)非交互式有狀態(tài)混淆价匠，這在普通設(shè)置中是不可能的当纱，即使在假設(shè)無狀態(tài)硬件令牌或虛擬黑盒安全加密混淆時(shí)也是如此。
有狀態(tài)混淆允許（誠實(shí)）客戶端對(duì)程序進(jìn)行模糊處理并將其發(fā)送到服務(wù)器踩窖，使得服務(wù)器可以在多個(gè)輸入上評(píng)估混淆程序坡氯，而混淆程序在多個(gè)調(diào)用中保持（秘密）內(nèi)部狀態(tài)。我們考慮有狀態(tài)混淆的模擬安全概念洋腮，其中服務(wù)器應(yīng)該只學(xué)習(xí)與正在回應(yīng)服務(wù)器查詢的有狀態(tài)oracle（實(shí)現(xiàn)混淆程序）交互的信息箫柳。例如，有狀態(tài)混淆在以下應(yīng)用場(chǎng)景中可以是有用的原語：假設(shè)客戶端（例如啥供，醫(yī)院）將敏感數(shù)據(jù)庫（對(duì)應(yīng)于我們希望混淆的程序）外包給配備有可信硬件的云服務(wù)器∶趸校現(xiàn)在，分析師可以向服務(wù)器發(fā)送統(tǒng)計(jì)查詢并獲得差異私有答案伙狐。由于每個(gè)查詢都會(huì)消耗一些隱私預(yù)算涮毫，因此我們希望保證在預(yù)算耗盡后瞬欧，對(duì)數(shù)據(jù)庫的任何其他查詢都將返回⊥。我們正式展示了如何從證明的執(zhí)行處理器實(shí)現(xiàn)有狀態(tài)的混淆窒百。此外黍判，如上所述，我們證明在普通設(shè)置中無法進(jìn)行有狀態(tài)混淆篙梢，即使假設(shè)存在無狀態(tài)硬件令牌或假設(shè)虛擬黑盒安全混淆。
2.3使用單個(gè)安全處理器進(jìn)行可組合的雙方計(jì)算的不可能性
一個(gè)自然要問的問題是美旧，我們是否可以實(shí)現(xiàn)普遍可組合（即UC安全）多方計(jì)算渤滞，這在沒有任何設(shè)置假設(shè)的普通設(shè)置中是已知的 - 但是存在公共參考字符串時(shí)是可行的[ 21,23]，即為每個(gè)協(xié)議實(shí)例新近獨(dú)立地以可信賴的方式生成的公共隨機(jī)字符串榴嗅。從表面上看妄呕，Gatt似乎提供了比普通引用字符串更強(qiáng)大的功能，因此很自然地期望它能夠?qū)崿F(xiàn)UC安全的多方計(jì)算嗽测。然而绪励，經(jīng)過仔細(xì)研究，我們發(fā)現(xiàn)唠粥，或許有些令人驚訝的是疏魏，這種直覺是微妙的錯(cuò)誤，如下面的非正式定理所示晤愧。
定理2（非正式）大莫。如果至少有一方未配備經(jīng)過驗(yàn)證的執(zhí)行處理器，則在沒有額外設(shè)置假設(shè)的情況下（即使所有其他方都配備了經(jīng)過證實(shí)的執(zhí)行處理器）官份，也無法實(shí)現(xiàn)UC安全多方計(jì)算只厘。
在這里，微妙的技術(shù)性恰好源于Gatt是一個(gè)在所有用戶舅巷，應(yīng)用程序和協(xié)議實(shí)例之間共享的全局功能羔味。這產(chǎn)生了密碼學(xué)社區(qū)眾所周知的不可否認(rèn)性問題。由于制造商簽名密鑰（mpk钠右，msk）是全局共享的赋元，因此在一個(gè)協(xié)議實(shí)例中生成的證明可以將副作用帶入另一個(gè)協(xié)議實(shí)例中。因此爬舰，向其他方發(fā)送證明的大多數(shù)自然協(xié)議候選人將允許對(duì)手通過向第三方證明證明來暗示參與協(xié)議的誠實(shí)方们陆。此外，即使安全處理器簽署匿名證明情屹，這種不可否認(rèn)性仍然存在：因?yàn)槿绻⒎撬懈鞣蕉紦碛邪踩奶幚砥髌撼穑敲垂粽咧辽倏梢宰C明Gatt注冊(cè)表中的某些誠實(shí)方參與了協(xié)議，即使他無法證明哪一個(gè)垃你。直觀地說椅文，如果所有各方都配備了安全的處理器喂很，那么不可否認(rèn)性就會(huì)消失 - 請(qǐng)注意，這必然意味著對(duì)手本身也必須擁有安全的處理器皆刺。由于證明是匿名的少辣，因此對(duì)手將無法證明證明是由誠實(shí)的一方產(chǎn)生的，還是他只是要求他自己的本地處理器簽署證明羡蛾。這基本上允許誠實(shí)的一方拒絕參與協(xié)議漓帅。
提取不可能。我們將上述直覺形式化痴怨，并表明不僅發(fā)送證明的自然協(xié)議候選者遭受不可否認(rèn)性忙干，事實(shí)上，如果并非所有方都擁有安全處理器浪藻，則不可能實(shí)現(xiàn)UC安全多方計(jì)算捐迫。不可能性類似于在沒有共同參考字符串的情況下，UC安全承諾的不可能性[23]爱葵∈┐鳎考慮現(xiàn)實(shí)世界的提交者C是否已損壞且接收者是否誠實(shí)。在這種情況下萌丈，在模擬證明期間赞哗，當(dāng)真實(shí)世界C輸出一個(gè)承諾時(shí)，理想世界模擬器Sim必須捕獲相應(yīng)的記錄并提取值v commit浓瞪，并將v發(fā)送到承諾理想功能Fcom懈玻。然而，如果理想世界模擬器Sim可以執(zhí)行這樣的提取乾颁，那么真實(shí)世界的接收器也必須能夠（因?yàn)镾im沒有比真實(shí)接收器更多的能力） - 這違反了承諾必須隱藏的要求涂乌。正如Canetti和Fischlin所展示的[23]，一個(gè)共同的引用字符串允許我們通過為模擬器提供更多功能來規(guī)避這種不可能性英岭。由于公共參考字符串（CRS）是本地功能湾盒，因此在模擬期間，模擬器可以對(duì)CRS進(jìn)行編程并嵌入陷門 - 這個(gè)陷門將允許模擬器執(zhí)行提取诅妹。由于現(xiàn)實(shí)世界的接收器不具備這樣的陷門罚勾，因此協(xié)議仍然保留了對(duì)真實(shí)接收器的機(jī)密性。
實(shí)際上吭狡，如果我們的Gatt功能也是本地的尖殃，我們的模擬器Sim可以用類似的方式對(duì)Gatt進(jìn)行編程，并且提取很簡單划煮。然而送丰，實(shí)際上，本地Gatt功能意味著必須為每個(gè)協(xié)議實(shí)例生成新的密鑰制造商對(duì)（mpk弛秋，msk）（即器躏，甚至對(duì)于同一用戶的多個(gè)應(yīng)用）俐载。因此，本地Gatt顯然無法捕獲真實(shí)世界安全處理器的可重用性登失，這證明了為什么我們將證明的執(zhí)行處理器建模為全局共享功能遏佣。
圖2：可組合的雙方計(jì)算：雙方都有安全的處理器。 AE表示經(jīng)過驗(yàn)證的加密揽浙。 所有ITI的激活點(diǎn)都是不可重入的状婶。 當(dāng)激活點(diǎn)被多次調(diào)用時(shí)，ITI只輸出⊥馅巷。 雖然沒有明確指出太抓，如果Gatt在查詢時(shí)輸出，令杈，協(xié)議將中止輸出⊥。 組參數(shù)（g碴倾，p）被硬編碼到prog2pc中逗噩。
不幸的是，當(dāng)Gatt是全球性的時(shí)跌榔，事實(shí)證明异雁，當(dāng)提交者C被破壞并且只有接收者具有安全處理器時(shí)，從普通設(shè)置中提取的同樣不可能性將繼續(xù)存在僧须。在這種情況下纲刀，模擬器Sim還必須提取從C發(fā)出的抄本提交的輸入。但是担平，如果模擬器Sim可以執(zhí)行這樣的提取示绊，那么現(xiàn)實(shí)世界的接收器也是如此 - 注意在這種情況下是現(xiàn)實(shí)世界的接收器實(shí)際上比Sim更強(qiáng)大，因?yàn)樵谧?cè)表中的真實(shí)接收器能夠有意義地調(diào)用Gatt暂论，而模擬器Sim不能面褐！
很容易觀察到，當(dāng)損壞的提交者具有安全的處理器時(shí)取胎，這種不可能性結(jié)果不再成立 - 在這種情況下展哭，協(xié)議可能要求提交者C將其輸入發(fā)送給Gatt。由于模擬器捕獲了進(jìn)出C的所有成績單闻蛀，因此可以簡單地提取輸入匪傍。實(shí)際上，我們表明觉痛，當(dāng)雙方都擁有安全的處理器時(shí)役衡，不僅承諾，而且一般的雙方計(jì)算也是可能的秧饮。
2.4當(dāng)兩者都具有安全處理器時(shí)可組合的雙方計(jì)算
定理3（非正式）映挂。假設(shè)存在安全密鑰交換協(xié)議泽篮。然后存在UC-實(shí)現(xiàn)F2pc的Gatt-混合協(xié)議。此外柑船，在該協(xié)議中帽撑，所有依賴于程序的評(píng)估都在包圍區(qū)內(nèi)執(zhí)行而不是以加密方式執(zhí)行。
我們?cè)趫D2中給出了一個(gè)明確的協(xié)議（為了具體鞍时，我們?cè)趨f(xié)議中使用Diffie-Hellman密鑰交換亏拉，盡管相同的方法擴(kuò)展到任何安全密鑰交換）。該協(xié)議在其僅執(zhí)行O（1）（與程序無關(guān)的）加密計(jì)算的意義上是有效的逆巍；并且所有依賴程序的計(jì)算都在飛地內(nèi)部進(jìn)行及塘。我們現(xiàn)在簡要解釋一下協(xié)議。
?首先锐极，雙方的安全處理器執(zhí)行密鑰交換并為經(jīng)過身份驗(yàn)證的加密方案建立密鑰sk笙僚。
?然后，每方的飛地用sk加密方的輸入灵再。然后肋层，該方將得到的經(jīng)過身份驗(yàn)證的密文ct發(fā)送給另一方。
?現(xiàn)在每個(gè)飛地解密ct并執(zhí)行評(píng)估翎迁，并且每一方都可以查詢其本地飛地以獲得輸出栋猖。
?大多數(shù)協(xié)議都很自然，但一種技術(shù)對(duì)于模棱兩可是必要的汪榔。特別是蒲拉，飛地程序的“計(jì)算”入口點(diǎn)有一個(gè)后門表示為v。如果v =⊥痴腌，Gatt將簽署真實(shí)的評(píng)估結(jié)果并返回證明的結(jié)果雌团。另一方面，如果v?=⊥衷掷，飛地將簡單地簽名并輸出v本身辱姨。在現(xiàn)實(shí)世界的執(zhí)行中，誠實(shí)的一方將始終提供v =⊥作為飛地項(xiàng)目的“計(jì)算”入口點(diǎn)的輸入戚嗅。但是雨涛，正如我們稍后解釋的那樣，模擬器將利用此后門v來執(zhí)行模糊處理并對(duì)輸出進(jìn)行編程懦胞。
我們現(xiàn)在解釋在上述協(xié)議的證明中出現(xiàn)的一些有趣的技術(shù)問題替久。
?提取。首先躏尉，由于每一方將其輸入直接發(fā)送到其本地飛地蚯根，因此可以進(jìn)行提取。如果一方腐敗，模擬器將捕獲此交互颅拦，然后模擬器可以提取腐敗方的輸入;
?Equivocate蒂誉。我們現(xiàn)在解釋飛地程序中的后門v如何允許證明中的模棱兩可【嗨В回想一下右锨，最初，模擬器不知道誠實(shí)方的輸入碌秸。為了模擬對(duì)手的誠實(shí)方的消息（其中包含來自飛地的證明）绍移，模擬器必須代表誠實(shí)的一方向Gatt發(fā)送虛擬輸入以獲得證明。當(dāng)模擬器設(shè)法提取損壞方的輸入時(shí)讥电，它將輸入發(fā)送到理想功能F2pc并獲得表示為outp 的計(jì)算結(jié)果□褰眩現(xiàn)在，當(dāng)腐敗的一方查詢其本地飛地的輸出時(shí)恩敌，模擬器必須讓Gatt簽署正確的輸出（通常稱為模棱兩可）瞬测。為了實(shí)現(xiàn)這一點(diǎn)，模擬器將利用前面提到的后門v：而不是像現(xiàn)實(shí)世界協(xié)議那樣向Gatt發(fā)送（ct纠炮，⊥）涣楷，模擬器將（ct，outp *）發(fā)送給Gatt抗碰，這樣Gatt就會(huì)簽名OUTP *。
?關(guān)于匿名證明的說明绽乔。有趣的是要注意我們的協(xié)議如何依賴于安全性的匿名證明弧蝇。具體來說，在證明中折砸，模擬器需要為對(duì)手A模擬誠實(shí)方的消息看疗。為此，模擬器將自己模擬最好的一方的飛地（即對(duì)手的）安全處理器 - 這樣的模擬是可能是因?yàn)镚att返回的證明是匿名的睦授。如果證明不是匿名的（例如两芳，綁定到該方的標(biāo)識(shí)符），則模擬器將無法模擬誠實(shí)方的飛地（有關(guān)更多討論去枷，請(qǐng)參閱第8.4節(jié)）怖辆。
2.5用最小的全局設(shè)置來規(guī)避不可能性
實(shí)際上，如果我們能夠在存在單個(gè)證明的執(zhí)行處理器的情況下允許可組合的多方計(jì)算删顶，那么顯然是可取的竖螃。作為期望的用例，想象多個(gè)客戶端（例如逗余，醫(yī)院）特咆，每個(gè)客戶端具有敏感數(shù)據(jù)（例如，醫(yī)療記錄）录粱，其希望對(duì)其聯(lián)合數(shù)據(jù)執(zhí)行一些計(jì)算（例如腻格，用于臨床研究的數(shù)據(jù)挖掘）画拾。此外，他們希望將數(shù)據(jù)和計(jì)算外包給不受信任的第三方云提供商菜职。具體而言青抛，客戶端可能沒有安全處理器，但只要云服務(wù)器執(zhí)行些楣，我們希望允許外包安全多方計(jì)算脂凶。
我們現(xiàn)在演示如何引入最小的全局設(shè)置假設(shè)來規(guī)避這種不可能性。具體來說愁茁，我們將利用全局增強(qiáng)公共參考字符串（ACRS）[22]蚕钦，此后表示為Gacrs。雖然Gacrs知道UC安全多方計(jì)算的可行性鹅很，即使沒有安全處理器[22]嘶居，但現(xiàn)有協(xié)議涉及在程序運(yùn)行時(shí)（至少）線性的加密計(jì)算。我們的目標(biāo)是演示一個(gè)實(shí)用的協(xié)議促煮，在安全區(qū)域內(nèi)執(zhí)行任何與程序相關(guān)的計(jì)算邮屁，并且只執(zhí)行O（1）加密計(jì)算。
定理4（非正式）菠齿。假設(shè)存在安全密鑰交換協(xié)議佑吝。然后，存在（Gacrs绳匀，Gatt） - 混合協(xié)議芋忿，UC實(shí)現(xiàn)Fmpc并且僅使用單個(gè)安全處理器。此外疾棵，該協(xié)議在安全處理器的包圍區(qū)內(nèi)執(zhí)行所有與程序相關(guān)的計(jì)算（而不是加密）戈钢。
最小的全局設(shè)置Gacrs。為了理解這個(gè)結(jié)果是尔，我們首先解釋最小的全局設(shè)置Gacrs殉了。首先，Gacrs提供全局公共引用字符串拟枚。其次薪铜，Gacrs還允許每個(gè)（損壞的）方P為自己查詢身份密鑰。通過使用全局主密鑰對(duì)該方的標(biāo)識(shí)符P進(jìn)行簽名來計(jì)算該身份密鑰恩溅。請(qǐng)注意痕囱，這樣的全局設(shè)置很小，因?yàn)檎\實(shí)的各方永遠(yuǎn)不必查詢其身份密鑰暴匠。身份密鑰只是提供給腐敗方的后門鞍恢。雖然初看起來向?qū)κ痔峁┖箝T似乎是違反直覺的，但請(qǐng)注意，這個(gè)后門也提供給我們的模擬器 - 這增加了模擬器的功能帮掉，使我們能夠規(guī)避前面提到的不可能性和設(shè)計(jì)誠實(shí)方可以拒絕參與的協(xié)議弦悉。
MPC具有單個(gè)安全處理器和Gacrs。我們考慮使用配備安全處理器的服務(wù)器以及沒有安全處理器的多個(gè)客戶端進(jìn)行設(shè)置蟆炊。
讓我們首先關(guān)注服務(wù)器和客戶端子集損壞時(shí)（更有趣）的情況稽莉。關(guān)鍵問題是如何在Gacrs的幫助下解決提取的不可能性 - 更具體地說，模擬器如何提取腐敗客戶的輸入涩搓？我們的想法如下 - 為了方便讀者污秆，我們?cè)谙蚣夹g(shù)細(xì)節(jié)進(jìn)行解釋時(shí)跳過并提出圖3中的詳細(xì)協(xié)議，但我們將重新審視它并在第6節(jié)中提供正式的符號(hào)和證明昧甘。
圖3：使用單個(gè)安全處理器的可組合多方計(jì)算良拼。ψ（P，msg充边，σ）輸出一個(gè)元組（msg庸推，C，π）浇冰，其中π是證明無法區(qū)分的證明贬媒，密文C加密msg上的有效證明σ，或加密P的身份密鑰肘习。 PKE和AE分別表示公鑰加密和認(rèn)證加密际乘。 符號(hào)發(fā)送表示通過安全信道發(fā)送的消息。
paper 15.----22.
3.1
3.2
