論文作者：

Ilya Sergey1and Aquinas Hobor2

1 University College London, United Kingdomi.sergey@ucl.ac.uk
2 Yale-NUS College and School of Computing, National University of Singaporehobor@comp.nus.edu.sg

翻譯：渡鴉

「讓國(guó)內(nèi)外的區(qū)塊鏈技術(shù)沒(méi)有時(shí)差」。

4、所有權(quán)和權(quán)限

替代禁止對(duì)合約不受歡迎的干預(yù)的另一種方法是設(shè)計(jì)一個(gè)定制的許可合約，控制不同方面允許的一組操作。

首先如果我們強(qiáng)制執(zhí)行有限的訪問(wèn)規(guī)則，則可以避免圖3 中的雙線程示例所展示的問(wèn)題，并阻止一個(gè)斷言其狀態(tài)x的任何內(nèi)容。例如，通過(guò)在任何時(shí)刻表示最多一個(gè)線程可以查詢/修改其狀態(tài)。這將授予相應(yīng)的線程在對(duì)象上的獨(dú)占所有權(quán)[30] ，因此，證明從線程本地做出的有關(guān)對(duì)象狀態(tài)的斷言。

獨(dú)占所有權(quán)，從傳統(tǒng)意義上講，是通過(guò)禁止任何干預(yù)來(lái)獲得的，但獨(dú)有者在合約狀態(tài)中進(jìn)行重大改變，Ethereum的合約中保證了獨(dú)特的所有權(quán)。例如，圖5 （左）顯示了Counter合約的更改版本，所以沒(méi)有其他方可以與它進(jìn)行交互，除了它的“所有者”。所有權(quán)規(guī)則由Solidity的修飾機(jī)制執(zhí)行，允許人們?yōu)楣δ芴峁┳远x的動(dòng)態(tài)檢查前/后置條件。在我們的示例中，byOwner修飾符將強(qiáng)制執(zhí)行，功能的獲取和設(shè)置將僅代表固定方 - 合約所有者引用。

圖.5.?獨(dú)占（左）和讀/鎖定（右）合約

這是一個(gè)相當(dāng)粗暴的解決方案，因?yàn)檫@意味著排除合約中的任何并發(fā)交互。然而，從一個(gè)角度來(lái)看，合約作為并發(fā)對(duì)象的觀點(diǎn)是很明顯的，請(qǐng)看我們的類比：帳號(hào)是線程。實(shí)際上，如圖5 所示，通過(guò)對(duì)合約施加特定所有權(quán)規(guī)則類似于通過(guò)對(duì)Thread進(jìn)行明確檢查來(lái)增強(qiáng)其Java對(duì)等體。currentThread（）.getId（）。

現(xiàn)在讓我們嘗試通過(guò)設(shè)計(jì)具有更詳細(xì)訪問(wèn)權(quán)限的計(jì)數(shù)器來(lái)進(jìn)一步推動(dòng)帳戶和線程之間的比較。我們將確保只要存在“有興趣”的帳戶（即“線程”）使其值不可變（因?yàn)閮?nèi)部邏輯可能依賴其不變性），則不允許其他方修改它。同樣，如果目前正好有一方擁有修改合約的唯一許可，則不得允許其他方閱讀。這種同步問(wèn)題的解決方案是通過(guò)名稱讀/鎖定[6]，這在并發(fā)社區(qū)中是眾所周知的。其實(shí)現(xiàn)需要跟蹤當(dāng)前正在讀取和寫入共享對(duì)象的線程，所以在執(zhí)行讀/寫操作之前，線程應(yīng)該明確獲取相應(yīng)的權(quán)限，然后在完成后釋放它。

圖5的右側(cè)部分顯示了讀/寫鎖定合約實(shí)現(xiàn)的基本部分。兩個(gè)新領(lǐng)域，跟蹤目前活躍的讀者和作家。新的修飾符canRead和canWrite將被用于省略的get和set操作。最后，只要在系統(tǒng)中沒(méi)有活動(dòng)寫入器，AcquReadRock允許其調(diào)用者獲取鎖定，通過(guò)讀取器映射注冊(cè)。

我們可以看到，以線程方式類比是十分有效的。我們提出了一些解決可能的同步問(wèn)題的方案，可以從并發(fā)文獻(xiàn)中逐字逐句地進(jìn)行。所提出的解決方案的唯一缺點(diǎn)是它是相當(dāng)整體的事實(shí)：合約現(xiàn)在將數(shù)據(jù)結(jié)構(gòu)（即，計(jì)數(shù)器）的功能與同步原語(yǔ)（即，鎖）的功能相結(jié)合。我們將在第5節(jié)中討論提高實(shí)現(xiàn)模塊性的可能途徑。

關(guān)于正式推理和驗(yàn)證的注意事項(xiàng)。關(guān)于許可賬戶和所有狀態(tài)分離訪問(wèn)的正式推理是共享內(nèi)存并發(fā)文獻(xiàn)中長(zhǎng)期研究的主題（參見(jiàn)例如[8] 的概述）。正式主義，如并發(fā)分離邏輯和[30]分?jǐn)?shù)/計(jì)數(shù)權(quán)限[6]提供了一種靈活的方式來(lái)定義抽象所有權(quán)規(guī)則，并驗(yàn)證一個(gè)特定的實(shí)現(xiàn)是否忠實(shí)地遵循。例如，我們的讀/寫鎖合約可以通過(guò)Bornat等人的正式的權(quán)限模型證明是安全的（即禁止并發(fā)修改）[6]。

5討論

5.1合約的編寫

在第4節(jié)中考慮的鎖定合約“模式”具有重大的延伸：其設(shè)計(jì)是非模塊化的。也就是說(shuō)，鎖定機(jī)構(gòu)是由合約本身而不是由第三方數(shù)據(jù)實(shí)施的。這與軟件工程的良好做法不同，建議將同步原語(yǔ)（例如普通和可重入鎖）實(shí)現(xiàn)為獨(dú)立庫(kù)，可用于管理訪問(wèn)客戶端特定的資源。

但是一旦鎖定邏輯被解除合約之外，關(guān)于合約行為的推理就顯得更加困難，因?yàn)闉榱俗C明其內(nèi)部不變量的保存，需要了解鎖定協(xié)議的屬性，例如編者的獨(dú)特性，這在合約之外。換句話說(shuō)，合約的驗(yàn)證不能再以孤立的方式進(jìn)行，需要建立一個(gè)模型，允許對(duì)與其他嚴(yán)格指定的合約交互的合約進(jìn)行推理。解除合約邏輯的想法不只是我們這樣認(rèn)為的，而且在合約開發(fā)中是至關(guān)重要的。例如，同樣的想法被提倡作為通過(guò)引入和額外的間接層次來(lái)實(shí)施Ethereum可升級(jí)合約的一種方式[11]。擁有由任何一方可以援引的另一個(gè)合約的“合約工廠”構(gòu)成了與證明高階并發(fā)對(duì)象的安全屬性（即，與其他對(duì)象一起作用）類似的驗(yàn)證挑戰(zhàn)[19]。

使用并發(fā)邏輯的組合推理和相互依賴和高階并發(fā)對(duì)象驗(yàn)證的思想在過(guò)去十年中一直個(gè)熱門課題[12，33，34， 37]。而大多數(shù)都集中在協(xié)議的概念上，在同時(shí)更新的情況下，作為對(duì)象行為的抽象接口，同時(shí)隱藏低級(jí)實(shí)現(xiàn)細(xì)節(jié)（即實(shí)際代碼）。我們相信，通過(guò)利用我們的類比，我們將能夠開發(fā)一種用于這種多合約交互的模塊化驗(yàn)證的方法。

5.2活性

隨著鎖定和獨(dú)占訪問(wèn)的引入，出現(xiàn)了另一個(gè)并發(fā)相關(guān)問(wèn)題：推理合約實(shí)現(xiàn)的進(jìn)展和活動(dòng)屬性。例如，不難想象一種情況，其中在圖5 的示例中注冊(cè)為“讀者”的特定帳戶可能永遠(yuǎn)不會(huì)釋放讀卡器鎖，從而阻止其他人能夠更改合約未來(lái)的狀況。在這種情況下的活躍意味著最終會(huì)有好的事情發(fā)生，這意味著任何一方都有適當(dāng)?shù)募?lì)來(lái)解除鎖定。在并發(fā)詞匯中，這樣的假設(shè)可以被重新表述為系統(tǒng)調(diào)度器的公平性，使得可以重用現(xiàn)有的證明方法來(lái)進(jìn)行單個(gè)和多合約執(zhí)行中的進(jìn)展[25] 和終止[18]的模塊化推理。

6、相關(guān)工作

智能合約的正式推理是一個(gè)新興和令人興奮的，適用于描述合約行為的抽象行為，是值得研究的課題。在本節(jié)中，我們將我們的觀察結(jié)果與正式化和驗(yàn)證合約屬性的現(xiàn)有結(jié)果聯(lián)系起來(lái)，概述將從我們的并發(fā)類比中受益的領(lǐng)域。

6.1驗(yàn)證合約實(shí)施

自從DAO bug [9] 以來(lái)，Ethereum社區(qū)一直專注于防止類似錯(cuò)誤，借助通用工具進(jìn)行程序驗(yàn)證。

目前，Solidity所寫的合約可以用Hoare樣式的前置/后置條件注釋，并轉(zhuǎn)換為OCaml代碼[32]，所以他們可以使用Why3工具進(jìn)行驗(yàn)證，該工具使用自動(dòng)化來(lái)排除生成的驗(yàn)證條件[16] 。這種方法對(duì)于驗(yàn)證Solidity程序的基本安全屬性是有效的，例如總是位于特定數(shù)組索引邊界內(nèi)的特定變量，以及保留一般合約不變量（通常以一個(gè)形式表示，如果在uint值變量的值上的線性方程式）方法邊界和執(zhí)行外部合約調(diào)用之前–這也正是DAO合約違反的。

Bhargavan等人最近翻譯了Solidity子集（無(wú)循環(huán)和遞歸）[5] 到F-a編程語(yǔ)言和驗(yàn)證框架，基于依賴類型[35] 。他們還提供了從EVM字節(jié)碼到F程序的翻譯。這兩種方法可以使用F作為驗(yàn)證合約屬性的統(tǒng)一工具，例如不變量保存和不存在未處理的異常，通過(guò)F對(duì)索引Hoaremonad的支持而被編碼為效果[36] 。Pettersson和Edstr [31]采用了一種類似的指定合約行為和依賴類型的方法，他們實(shí)現(xiàn)了一種基于效果的小型合約DSL作為淺埋嵌入到Idris[7] 中，其可執(zhí)行代碼提取到Serpent[14] 一種Python風(fēng)格的合約語(yǔ)言。

Hirai最近將Lem[28] 中的EthereumVirtual Maine [22] 的完整規(guī)范正式提交給了Isabelle/ HOL驗(yàn)證助手，對(duì)于編譯為EVM字節(jié)碼的合約的機(jī)械化驗(yàn)證，具有許多安全屬性包括對(duì)可變狀態(tài)的斷言以及潛在的可重入的缺失。與以前的方法不同，Hirai的正式化并沒(méi)有提供構(gòu)造和組合證明的句法方式（例如通過(guò)Hoare式程序邏輯），所有關(guān)于合約行為的推理都是從低級(jí)執(zhí)行語(yǔ)義[38]中進(jìn)行的。

與這些主要側(cè)重于低級(jí)別安全性質(zhì)和不變性保存的工作相比，我們的觀察提示了更高層次的形式意義，用于捕獲合約行為的屬性及其與外界的溝通模式。特別地，我們考慮將抽象狀態(tài)轉(zhuǎn)換系統(tǒng)（STS）[29]作為適當(dāng)?shù)男问絹?lái)進(jìn)行通信，使用諸如TLA+[24]等已建立的工具集來(lái)跟蹤合約執(zhí)行和活動(dòng)屬性。為了將這樣的抽象表示與低級(jí)合約代碼連接起來(lái)，必須證明高級(jí)和低級(jí)表示之間，即在STS和代碼之間的細(xì)化[3] 。從某種意義上說(shuō)，找到一個(gè)合適的合約不變量，并通過(guò)Why3或F證明它驗(yàn)證一個(gè)狀態(tài)轉(zhuǎn)換系統(tǒng)之間的細(xì)化，使得唯一的狀態(tài)是不變量描述的狀態(tài)，以及保留它的一個(gè)實(shí)現(xiàn)。然而，我們預(yù)計(jì)將需要更復(fù)雜的STS才能推理具有搶占并發(fā)性的合約。

6.2推動(dòng)全球合約

[27].Luu等人發(fā)現(xiàn)，由于干擾現(xiàn)象，一些合約容易出現(xiàn)無(wú)意或者對(duì)抗性濫用的觀點(diǎn)。他們將問(wèn)題類似于我們?cè)诘? 節(jié)中的計(jì)數(shù)器示例中所表現(xiàn)，即交易順序依賴性（TOD），根據(jù)我們的并發(fā)類比可以將其概括為無(wú)限制干擾的問(wèn)題。Luu等人提出的TOD問(wèn)題的解決方案需要改變Ethereum事務(wù)的語(yǔ)義，提供一個(gè)與圖4中的testAndSet類似的原語(yǔ)。雖然這種方法的優(yōu)點(diǎn)是沒(méi)有需要修改已經(jīng)部署的合約（只有與客戶端代碼交互的代碼需要更改），才需要所有相關(guān)的用戶升級(jí)他們的客戶端應(yīng)用程序，以便考慮更改。本質(zhì)上，Luu等人的解決方案針對(duì)非常具體的并發(fā)模式：通過(guò)添加塊支持的讀 - 修改 - 寫入原語(yǔ)來(lái)加強(qiáng)由原子寄存器提供的同步。意識(shí)到問(wèn)題的本質(zhì)，暗示我們的類比，可能會(huì)提出替代合約解決方案，例如工程化鎖定代理合約。然而，這種方法的缺點(diǎn)在于，在設(shè)計(jì)和部署合約的時(shí)刻需要預(yù)見(jiàn)這種行為。也就是說(shuō)，這樣一種對(duì)這種行為進(jìn)行建模的能力讓我們相信我們的比喻能夠?qū)崿F(xiàn)的。

7、結(jié)論

我們相信，我們?cè)谥悄芎霞s和并發(fā)對(duì)象之間的比較可以提供新的視角，刺激研究，并允許有效地重用現(xiàn)有的結(jié)果，工具以及了解，調(diào)試和驗(yàn)證分布式分類帳中復(fù)雜的合約行為的見(jiàn)解。作為比喻，我們不應(yīng)該逐字地采取行動(dòng)：一方面，確實(shí)存在并發(fā)問(wèn)題，在合約規(guī)劃中似乎幾乎不可觀察到; 另一方面，智能合約執(zhí)行者也應(yīng)該謹(jǐn)慎對(duì)待并發(fā)領(lǐng)域沒(méi)有直接對(duì)應(yīng)的觀念，例如氣體執(zhí)行和資金管理。

總而言之，我們留給讀者幾個(gè)猜測(cè)，靈感來(lái)自我們的觀察，但既沒(méi)有解決也不反對(duì)：

- 非垃圾收集語(yǔ)言中的常見(jiàn)并發(fā)挑戰(zhàn)是跟蹤堆位置的唯一性，這可以被后期回收和重用 - 被稱為ABA問(wèn)題[10] 。由于缺乏應(yīng)有的謹(jǐn)慎，ABA問(wèn)題可能導(dǎo)致違反對(duì)象狀態(tài)完整性。我們可以想象在多合約環(huán)境中有類似的情況嗎？

- 繼續(xù)比較，如果將區(qū)塊鏈看作共享狀態(tài)，那么挖掘協(xié)議定義了調(diào)度的優(yōu)先級(jí)。我們可以利用有效的并發(fā)線程管理的洞察力來(lái)分析和改進(jìn)現(xiàn)有的分布式分類帳？

- 線性化[21] （又名原子性）是指定無(wú)鎖并發(fā)對(duì)象的高級(jí)行為的正確性的標(biāo)準(zhǔn)概念。對(duì)于具有多種交易操作的復(fù)合合約（例如BlockKing），什么是等同的事實(shí)上的一致性概念？

原文：?https://zhuanlan.zhihu.com/p/29354702

總結(jié)

以上是生活随笔為你收集整理的从并发视角来看智能合约（下）【渡鸦论文系列】的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。