無bug編程是一項(xiàng)艱巨的任務(wù)，也是關(guān)鍵系統(tǒng)面臨的基本挑戰(zhàn)。為此，形式化方法提供了開發(fā)程序和驗(yàn)證程序正確性的技術(shù)。正式核查是一項(xiàng)艱苦的
無bug編程是一項(xiàng)艱巨的任務(wù)，也是關(guān)鍵系統(tǒng)面臨的基本挑戰(zhàn)。為此，形式化方法提供了開發(fā)程序和驗(yàn)證程序正確性的技術(shù)。
正式核查是一項(xiàng)艱苦的工作。它要求很高，需要大量的腦力，需要大量的投資，但它已經(jīng)成為軟件行業(yè)許多領(lǐng)域的強(qiáng)制性標(biāo)準(zhǔn)。
從區(qū)塊鏈的早期開始，這種科學(xué)似乎就違背了開發(fā)人員采用這種技術(shù)的必要性，但同時(shí)也降低了這種必要性。最流行的智能合約語言的成功難道不歸功于它類似javascript的語言嗎?
但是，采用這種方式是一把雙刃劍:與以前的任何其他網(wǎng)絡(luò)相比，經(jīng)濟(jì)上都會(huì)直接受到威脅。
既然新的共識(shí)方法和區(qū)塊鏈協(xié)議的安全性得到了越來越多的科學(xué)文獻(xiàn)的支持，現(xiàn)在是時(shí)候重新引入正式的方法，讓智能合與開發(fā)人員受益了。經(jīng)過幾十年的研究，這門科學(xué)是建立分散式應(yīng)用信心的必要紐帶。
本文旨在介紹正式的驗(yàn)證，回顧區(qū)塊鏈時(shí)代的現(xiàn)有工具，并強(qiáng)調(diào)以太坊特有的挑戰(zhàn)。
正式驗(yàn)證的簡短介紹
智能合約是一種自我執(zhí)行的工具，它的增長是隨著區(qū)塊鏈的興起而出現(xiàn)的。隨著這項(xiàng)技術(shù)的采用，這些金融工具的實(shí)際存款額不斷增加，同時(shí)它們的復(fù)雜性也嚴(yán)重升級(jí)。這種情況會(huì)周期性地導(dǎo)致代價(jià)高昂的bug和漏洞，從而為更嚴(yán)格的程序分析方法帶來光明。
在這方面，在永久部署分散式的應(yīng)用程序之前，測(cè)試和審計(jì)通常為開發(fā)人員和用戶提供一定的保證。但是，由于沒有代碼檢查可以100%保證消除所有bug，所以正式的驗(yàn)證可以通過數(shù)學(xué)方法帶來更高的可信度。這就是為什么這一領(lǐng)域受到以太坊基金會(huì)的積極支持，并可能迅速得到更廣泛的應(yīng)用。
在進(jìn)一步討論之前，應(yīng)該簡要介紹一些數(shù)學(xué)概念。
正確性: 如果一個(gè)程序執(zhí)行分配給它的任務(wù)沒有錯(cuò)誤，并且在所有可能的情況下都是正確的，那么這個(gè)程序就是正確的。
規(guī)范: 程序的規(guī)范是對(duì)分配給它的任務(wù)和允許用例的明確描述。指定一個(gè)程序需要抽象它的屬性，因此是一項(xiàng)困難的任務(wù)。根據(jù)規(guī)范驗(yàn)證程序?qū)崿F(xiàn)的正確性也很困難。
動(dòng)態(tài)分析包括執(zhí)行代碼或模擬代碼，以發(fā)現(xiàn)任何bug。創(chuàng)建測(cè)試計(jì)劃包括列出要測(cè)試的用例，并為每個(gè)用例建立一個(gè)測(cè)試。由于這些測(cè)試不能全面，動(dòng)態(tài)分析一般不能構(gòu)成正確性的證明。
另一方面，靜態(tài)分析包括遍歷代碼而不執(zhí)行代碼，以證明某些屬性。存在不同的方法，例如基于模型檢查或Hoare邏輯。形式驗(yàn)證依賴于靜態(tài)分析。
Hoare邏輯有助于證明，從驗(yàn)證某些屬性的初始狀態(tài)(前置條件)開始，通過執(zhí)行一系列指令，我們可以獲得驗(yàn)證其他屬性的狀態(tài)(后置條件)。如果總是這樣，這就叫做完全正確。
如果有一個(gè)帶有Hoare三元組(前置條件-指令-后置條件)的自然演繹，那么程序相對(duì)于其前置條件和后置條件是正確的。
像Coq這樣的證明助手幫助交互式地構(gòu)建這樣的演繹樹。
總結(jié)一下，要理解正式驗(yàn)證智能合約的挑戰(zhàn)，必須牢記兩個(gè)基本概念:
1. 我們不能證明合約是明智的。我們證明了它們的一些性質(zhì)。我們根據(jù)規(guī)范證明了它們的正確性。
2. 要被認(rèn)為是有效的，必須在一個(gè)單一的、可信的邏輯框架內(nèi)生成一個(gè)證明，從規(guī)范語言級(jí)別到虛擬機(jī)執(zhí)行級(jí)別。
在構(gòu)建區(qū)塊鏈時(shí)考慮到驗(yàn)證
2016 年初,一組研究人員分析了部署在以太坊主網(wǎng)上的字節(jié)碼,以查找常見的安全缺陷。他們驚人的評(píng)估被大量引用:在19366份研究合約中，8833份至少存在一次安全漏洞。在本文提倡改進(jìn)以太坊的操作語義以幫助形式化驗(yàn)證的同時(shí)，出現(xiàn)了一個(gè)問題:一些區(qū)塊鏈框架是否比其他框架更不容易進(jìn)行形式化驗(yàn)證?
很難否認(rèn)，每個(gè)區(qū)塊鏈都是為了滿足特定的期望子集而設(shè)計(jì)的，比如快速采用或安全性。
直接的結(jié)果是，正式的驗(yàn)證在一些框架上是當(dāng)前的現(xiàn)實(shí)，而在另一些框架上可能是長期的目標(biāo)。
在這方面,2018年發(fā)表的一份有趣的研究報(bào)告概述了合同語言和驗(yàn)證方法,作為對(duì)當(dāng)前解決方案的全面調(diào)查。它有助于確定以下區(qū)分因素,并概述當(dāng)前主要框架上正式方法的可用性。
合約語言
在軟件行業(yè)，特別是在區(qū)塊鏈領(lǐng)域，區(qū)分三種類型的語言是很有幫助的:
· 高級(jí)語言，如以太坊上的solability或Vyper, Tezos上的Liquidity，都旨在易于學(xué)習(xí)，并幫助大型開發(fā)人員社區(qū)編寫智能契約。
· 底層基于堆棧的語言，如比特幣腳本，代表了實(shí)際機(jī)器之前的最后一個(gè)抽象步驟
· 中間表示，如Tezos上的Michelson或Ziliqa上的Scilla，是對(duì)合約驗(yàn)證和代碼優(yōu)化最合適的支持。
圖1:不同級(jí)別的智能合約語言和編譯過程。(A)與更直接的(B)相比，便于驗(yàn)證和代碼優(yōu)化。
只有一種低級(jí)語言，比特幣腳本在于第一個(gè)區(qū)塊鏈上編寫智能合約。當(dāng)圖靈完備的區(qū)塊鏈框架出現(xiàn)時(shí)，就需要更富表現(xiàn)力的高級(jí)合約語言。
它們中的一些本質(zhì)上允許直接編譯字節(jié)碼，如(B) path(圖1)所示。例如，在以太坊上，solid作為一種智能合約語言被廣泛采用，開發(fā)人員的代碼可以直接編譯為EVM字節(jié)碼。
還設(shè)計(jì)了其他高級(jí)語言，以便可以首先將合約代碼編譯為中級(jí)表示，然后再編譯為低級(jí)語言，如(a) path(圖1)所示。
由于促進(jìn)了中間代碼的正式驗(yàn)證，不同的區(qū)塊鏈框架在驗(yàn)證智能合約方面的能力出現(xiàn)了重大差異。
驗(yàn)證方法
根據(jù)前面對(duì)語言的分類，我們可以區(qū)分出三種主要的驗(yàn)證方法:
(I):規(guī)范可以直接在字節(jié)碼級(jí)別進(jìn)行評(píng)估。由于合約源不一定可用，因此提供了一種方法來評(píng)估已經(jīng)部署的合約上的一些屬性。
(II):中間表示形式可專門設(shè)計(jì)為驗(yàn)證工具(例如證明助手)的目標(biāo)。這可以根據(jù)規(guī)范為代碼優(yōu)化和動(dòng)態(tài)驗(yàn)證提供非常合適的環(huán)境。中間代碼表示形式可以來自高級(jí)合約的編譯，也可以來自低級(jí)代碼的反編譯。
(III):一些工具也直接針對(duì)高級(jí)語言進(jìn)行推理。這種方法在驗(yàn)證時(shí)為開發(fā)人員提供了寶貴的直接反饋。
圖2:基于與規(guī)范化比較對(duì)象的不同驗(yàn)證方法。
正式的語義
當(dāng)新的編程語言出現(xiàn)時(shí)，它們的語義可能被正式地描述出來。程序的確切行為由正式語義定義，而對(duì)于具有非正式語義的語言，則需要更靈活性的編譯器。
在大多數(shù)情況下，定義在任何級(jí)別上使用的所有語言的正式語義都是至關(guān)重要的，因?yàn)樗鼮殚_發(fā)單個(gè)可信邏輯框架提供了條件，在這個(gè)框架中，從一種形式主義到另一種形式的轉(zhuǎn)換都要經(jīng)過正式建模和驗(yàn)證。
所有翻譯的正確性決定了一個(gè)人對(duì)整個(gè)框架的信心程度。如果對(duì)程序的中間表示形式執(zhí)行形式化驗(yàn)證，則反向翻譯將允許以更高級(jí)別的原始語言顯示有意義的消息。此外，如果轉(zhuǎn)換成機(jī)器字節(jié)碼不安全，那么沒有人可以正式信任它的執(zhí)行，無論在其他級(jí)別的驗(yàn)證工作如何。
例如,與Tezos和Cardano相反,EVM的正式語義只被描述在帖子前。并且,由于 Solidity 編譯器變化迅速,在缺少允許逐構(gòu)造自動(dòng)生成驗(yàn)證工具的正式語義的情況下,后者也需要遵循變化的速度。這些原因使得在以太坊上對(duì)智能合約的正式驗(yàn)證比其他區(qū)塊鏈更難。
到目前為止，以太坊的實(shí)際合約驗(yàn)證
如上所述，靜態(tài)分析可以用多種方法進(jìn)行。在智能合約中，大多數(shù)都是基于模型或基于驗(yàn)證的。在以太坊上介紹有前途的項(xiàng)目，并將注意力吸引到他們的LIM上，這可能會(huì)帶來驚人的啟示。
在以上綜述的基礎(chǔ)上，介紹以太坊上有前途的項(xiàng)目，并提請(qǐng)注意它們的局限性，這可能具有驚人的啟示意義。
智能合約的模型檢查表明,由于狀態(tài)組合，智能合約在實(shí)踐中不可行。基于VeriSolid•的模型提供了一個(gè)方便的界面來排列，還避免了已知安全流而構(gòu)建的塊,從而強(qiáng)加一些屬性,并自動(dòng)生成正確的Solidity 智能合約。但是,到目前為止,僅支持一組屬性,不能將 Solidity 代碼編譯為字節(jié)碼。
基于Hoare 邏輯的幾個(gè)項(xiàng)目尋求帶來的益處,以正式驗(yàn)證其源代碼中智能合約。一些人試圖對(duì) Solidity 代碼進(jìn)行說明 ,而另一些人則選擇直接使用ML 函數(shù)式編程語言進(jìn)行開發(fā),從而獲得正確的構(gòu)建程序。這種類型的努力可能會(huì)引起很多關(guān)注,因?yàn)樗鼈儠?huì)導(dǎo)致強(qiáng)大的開發(fā)人員工具和出色的經(jīng)驗(yàn)。
然而，應(yīng)該指出的是，在Why3中實(shí)現(xiàn)所有可靠類型和邏輯(公共/私有函數(shù)、gas注意事項(xiàng)……)需要大量的工作，而且目前還沒有從Why3到EVM的可生產(chǎn)的完整編譯器。
研究團(tuán)隊(duì)還嘗試對(duì)字節(jié)碼進(jìn)行全編譯,以驗(yàn)證中間表示的前期/后期樣式中的協(xié)定屬性。但更復(fù)雜的合約需要全面實(shí)施 EVM 字節(jié)碼,例如,可以這樣評(píng)估一些GAS消耗屬性。當(dāng)還支持從高級(jí)語言翻譯為相同的中間表示形式時(shí),可以驗(yàn)證功能正確性,并使在兩個(gè)中間表示形式(一個(gè)來自高級(jí)代碼的編譯,另一個(gè)來自字節(jié)碼的反編譯)等效。如果沒有，由于缺乏可用的用戶反饋，這種方法不太可能幫助開發(fā)人員在實(shí)踐中驗(yàn)證他們的智能合約。
目前在以太坊上可用的最完整的環(huán)境可能是K-framework。如果定義了語言的正式規(guī)范，它就可以處理各種工具的自動(dòng)生成，比如解釋器和編譯器。盡管如此，這個(gè)框架要求很高(需要大量規(guī)范的手工翻譯，這很容易出錯(cuò))，而且仍然存在一些缺陷(例如，主網(wǎng)上的EVM實(shí)現(xiàn)可能與機(jī)器語義不匹配)。盡管如此，已經(jīng)進(jìn)行了大量的工作來使這個(gè)現(xiàn)有的框架適應(yīng)區(qū)塊鏈。
結(jié)論
隨著區(qū)塊鏈價(jià)值的增加和分散化應(yīng)用程序復(fù)雜性的增加，推廣一種更嚴(yán)格的程序分析方法似乎是向客戶和合與所有者提供更高安全級(jí)別的唯一可接受的方法。
形式驗(yàn)證是一門成熟的科學(xué)，可以為實(shí)現(xiàn)這一目標(biāo)作出重大貢獻(xiàn)。但是，盡管一些區(qū)塊鏈的設(shè)計(jì)考慮到了這一目標(biāo)，但在以太坊上驗(yàn)證智能合與，尤其是那些以可靠方式編寫的合與，還遠(yuǎn)遠(yuǎn)不夠明顯。然而，在其他框架上，今天可以進(jìn)行正式的驗(yàn)證。現(xiàn)在要靠分散式應(yīng)用程序的創(chuàng)建者來迎接這一挑戰(zhàn)，并努力為更安全的智能合約鋪平道路。（考拉）
