論文作者：

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

翻譯：渡鴉

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

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

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

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

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

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

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

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

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

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

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

5討論

5.1合約的編寫

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

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

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

5.2活性

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

6、相關(guān)工作

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

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

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

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

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

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

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

6.2推動全球合約

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

7、結(jié)論

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

總而言之，我們留給讀者幾個猜測，靈感來自我們的觀察，但既沒有解決也不反對：

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

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

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

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

總結(jié)

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

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