基于智能合約的以太幣投票協議?

付利青 , 田海博

1(中山大學 數據科學與計算機學院,廣東 廣州 510006)

2(廣東省信息安全技術重點實驗室(中山大學),廣東 廣州 510006)

可信第三方(trusted third party,簡稱TTP)在安全協議中往往是功能較強大的一個設計模塊[1],如證書頒發機構(certificate authority,簡稱CA)是一種中心化TTP,可以證明身份和公鑰之間的綁定關系.計票系統中的計票機構(tally agent,簡稱TA)是另一種中心化TTP,負責誠實地統計選票.中心化TTP 通常知道一些敏感信息或者具備一些特殊的能力,例如TA 知道計票信息,可以權威地公布計票結果.這些信息和能力往往會引起外部攻擊者的興趣,增加了這些TTP 的安全風險.例如,敵手可以嘗試攻擊TA,在TA 公布選票前修改投票結果.此外,中心化TTP 也可能遭受內部攻擊,例如內部工作人員因為抵抗不住誘惑而拿敏感信息換取經濟利益.此外,中心化TTP自身的硬件和軟件也可能出現故障,使得服務中斷,威脅信息系統的可用性.另外,如果中心化TTP 的硬件和軟件跟不上業務的規模,中心化TTP 會成為整個安全協議的性能瓶頸.最后,中心化TTP 的業務范圍有限,往往只能服務一個區域,一般做不了全球的可信中心.總之,中心化的TTP 往往具有較低的可靠性和較高的安全風險.

區塊鏈技術為人們提供了一種基于點對點網絡的無中心的TTP,可以誠實地記錄交易和執行腳本.粗略地看,區塊鏈網絡中的節點通過某種共識機制產生一個新區塊,由創建了新區塊的節點記錄最近的交易并執行相關腳本.創建了新區塊的節點也可以從交易中收取交易費,甚至獲得獎勵.基于理性經濟人假設,區塊鏈網絡中的節點行為是可預期的.以比特幣為例,比特幣網絡的節點通過工作量證明的共識機制生成新的區塊,創建新區塊的節點可以獲得比特幣獎勵和交易費.比特幣系統自2009 年出現后,到目前為止運行良好.這在一定程度上說明無中心TTP 是可行的.以太坊[2]是比特幣系統的升級版,提供了圖靈完備的腳本語言,支持智能合約.

這種無中心TTP 所存儲的數據都是公開的,所以對以獲取秘密為目標的外部攻擊者而言沒有吸引力.另外,無中心TTP 的節點是動態加入、動態退出的,實現內部攻擊需要對共識算法進行顛覆才有可能,需要的代價非常大.同時,節點的動態性保證了單個節點的故障對全網影響不大.比較而言,區塊鏈這種無中心TTP 具有較高的可靠性和較低的安全風險[1].

無中心TTP 的優點自然吸引了不少協議設計者在區塊鏈中設計協議.目前,在以太坊平臺上有100 多個可部署的應用,包括投票、合同簽署、拍賣等應用[3].然而并不存在保護隱私的應用,例如投票協議中投票人的投票是公開的.Zhao 等人[4]提出了比特幣投票協議,通過比特幣交易來執行投票過程,并且保護了投票人的隱私.他們通過秘密分享、承諾、零知識證明[5]等技術生成秘密且可驗證的二選一的投票,之后,分別使用“索賠或退款”[6]和“聯合交易”[7]這兩種公平交換的模式給出了兩個投票過程.特別的,為了解決比特幣交易的延展性問題[7],他們使用了門限簽名體制,需要較多的交互次數和較高的計算代價.

本文汲取并擴展了Zhao 等人[4]的投票生成技術,支持生成對m個候選人的一般化投票;進而采用了智能合約來實現投票和資助過程,避免了采用門限簽名體制帶來的問題;最后,在模型檢測工具中對合約的主要邏輯進行了驗證.

1 相關工作

Zhao 等人[4]提出了比特幣投票的概念.n個投票人從2 個候選人中選擇1 個進行資助.要求每個候選人的投票是隱私的,并且是可驗證的.當投票結果揭曉后,獲勝者可以獲得所有投票人的資助.例如,每個投票人資助1比特幣,那么獲勝者可以獲得n比特幣.任何投票人不能因為不喜歡獲勝者而撤回資助.

與比特幣投票密切相關的工作之一自然是電子投票.“n個投票人從2 個候選人中選擇1 個”是一種典型的“贊成與否”的投票方式.這種投票可以一般化為“n個投票人從m個候選人中至少選擇kmin個、至多選擇kmax個候選人”[8].此外還有其他的一些投票方式,例如在m個候選人中分配一些選票,每個候選人獲得選票的數量有上限等.在選票的秘密性和可驗證性方面,電子投票也積累了豐富的實踐經驗.通常采用的技術包括同態加密、秘密分享、混合網絡、零知識證明等[8,9],這些設計方法在比特幣投票協議中顯然是可以借鑒的.

在Zhao 等人[4]的協議中使用了zkSNARK[10]這一特殊的零知識證明技術.該技術用于ZCash[10]中.與一般的零知識證明相比,zkSNARK 可以把哈希函數的原像或者對稱加密算法的明文作為輸入,給出原像或者明文具有某種可判別關系的證明.例如,給定兩個哈希值及其原像值,使用zkSNARK 可以給出一個證明,使得驗證人在僅有兩個哈希值及證明的情況下,驗證這兩個哈希值的原像是是否相等.

與比特幣投票密切相關的另外一類工作就是區塊鏈中的協議設計方法.例如,Zhao 等人[4]使用“索賠或退款”[6]和“聯合交易”[7]這兩種公平交換的模式來完成投票.其中,“索賠或退款”模式是Barder 等人[6]在設計公平的比特幣混合器時提出的,這一模式由Bentov 等人[11]在全局可組合模型中進行了定義.進一步地,Kiayias 等人[12]利用這一模式構建了一般的公平多方計算協議.Andrychowic 等人[13]指出“索賠或退款”模式容易受比特幣交易的延展性攻擊,進而提出“時間承諾”模式來設計公平的協議.進一步,Andrychowic 等人[7]進一步給出了“同步時間承諾”模式來提供雙方公平的安全協議.比特幣交易的延展性攻擊可以讓攻擊者改變交易的唯一標識,卻保持不變的語義.Decker 和Wattenhofer 認為,該問題是導致原比特幣交易市場MtGox 倒閉的原因[14].但是在最近的比特幣發展中,采用了隔離認證的方式,該方式通過區分交易內容和簽名字段也克服了可延展問題,這使得原來的“抵押-賠償”協議設計的方式重新成為一個可選項.

本文設計的是以太幣投票協議,基于以太坊平臺[2].以太坊平臺提供了完備圖靈機的能力和高級編程語言,同時具有以太幣,可以完成支付.以太坊中的智能合約是一種由事件驅動、具有狀態、運行在可復制的共享區塊鏈數據賬本上的計算機程序[15].該程序本身也部署在區塊鏈上,記入區塊鏈的特定區塊中.用戶通過調用智能合約實現智能合約的運行,以改變智能合約的狀態,生成新的交易,或者返回用戶希望的數據.

本文對合約的驗證使用了模型檢測工具.模型檢測通過模型狀態搜索的方法來驗證系統是否具有某些性質[16].給定描述合約邏輯的程序和規約條件,模型檢測工具生成對應的合約模型,并驗證規約條件在合約模型中是否成立.如果經過模型狀態搜索沒有發現違背規約條件的狀態,就證明合約滿足規約條件;如果發現了違背規約條件的狀態,則進行反向逆推,給出反例出現的路徑,以找到合約設計的缺陷.本文中使用進程元語言(process meta language,簡稱 Promela)[17]描述合約邏輯,用 Spin 模型檢測[18]工具進行驗證,用線性時態邏輯(linear temporal logic,簡稱LTL)[19,20]描述規約條件.

進一步地,本文用CCS 2016[21]中Luu 等人給出的一個專門針對以太坊智能合約的分析工具對合約進行了安全性測試.該工具旨在檢查可執行的分布式代碼合約(executable distributed code contract,簡稱EDCC)的缺陷,并且與任何基于以太坊的EDCC 語言兼容,包括Soldity,Serpent 和LLL.其檢測的智能合約的安全問題包括交易順序依賴、時間戳依賴、異常處理不當、可重入攻擊等.使用該工具時,需要輸入智能合約的代碼和以太坊的全局狀態,經過分析之后,該工具可以給出關于上述攻擊的安全性結論.經該工具檢測,僅提示本文的智能合約存在交易順序依賴問題.但是經過我們對合約邏輯的分析,本文的智能合約在規定的時間內只能執行符合約定條件的交易,并不存在交易順序依賴的問題.

我們注意到,在金融密碼會2017 中,出現了基于智能合約的投票協議[22].該協議需要在智能合約中直接運行較為復雜的密碼運算,導致合約代碼較為復雜.它需要較多的燃料(gas)才能執行,是一種把復雜性放在以太坊區塊鏈上的技術選擇.本文采取了Zhao 等人[4]的思路,使用了zkSNARK 技術,合約代碼相對簡單,只需要目前以太坊支持的一些操作即可,是一種把復雜性放在客戶端的技術選擇.另外,有文獻提出采用Zcash 進行投票[23],屬于Zcash 框架的簡單應用,還需要較多的探索.

1.1 主要貢獻

總體上,本文提供了一種以太幣投票智能合約,通過該智能合約,投票發起人可以讓n個投票人出資并對m個候選人進行投票,可以要求每個投票人至少選擇kmin個候選人、至多選擇kmax個候選人.投票階段結束后,通過智能合約可以完成計票,揭示每個候選人的得票數,并擇優資助.

具體來看,在選票生成階段,本文把Zhao 等人[4]生成選票的協議進行了擴展,平凡推廣到m個候選人的情況,并增加了零知識證明確保投票的合法性.在投票階段,本文通過智能合約完成了“聯合交易”的邏輯和“時間承諾”的邏輯,實現了計票、資助等功能.此外,我們發現Zhao 等人的協議設計存在資金黑洞,即投票失敗時所有投票者的資助金會被鎖住,我們的投票協議成功地避免了此類問題.并且通過模型檢測工具,本文對合約的主要業務邏輯進行了檢驗,確認了合約的正確性.

2 以太幣投票協議

類似于比特幣投票協議,本文的協議也分為選票生成和投票兩個階段.

2.1 選票生成

本文的選票生成協議把Zhao 等人[4]的選票生成協議作為子程序來調用.該子程序稱為VCi(Oi),表示投票人pi對一個候選人的投票Oi做出的可驗證的承諾投票,其中,Oi∈{0,1},0 表示不贊成,1 表示贊成.pi執行VCi(Oi)的過程如下.

1.生成隨機數:pi生成n個零和的隨機數rij∈?N,j∈{1,…,n},n是所有投票人的數量,N是2 的冪次的一個整數且比n大.對于每一個隨機數,pi計算該隨機數的承諾(cij,kij)←commit(rij),其中,kij是打開承諾的密鑰;之后,pi用zkSNARK 證明,j∈{1,…,n};然后,pi廣播給其他投票人所有的承諾和zkSNARK證明.

2.驗證承諾的零和屬性:pi收到每個其他投票人的n個承諾和1 個zkSNARK 證明后,驗證其正確性.

3.分發打開承諾的密鑰:當pi收到所有其他投票人正確的承諾后,對所有j∈{1,…,n}{i},pi發送kij給pj.

4.生成選票:對所有的j∈{1,…,n}{i},pi等待pj發送的kji,并驗證rji=open(cji,kji)≠⊥.當pi收到所有其他投票人打開承諾的密鑰,并驗證非空后,計算,其中,Ki和都是打開承諾的密鑰.之后,pi用zkSNARK 生成如下的零知識證明:

5.廣播選票及其零知識證明:pi廣播承諾Ci,和兩個zkSNARK 的零知識證明.

6.驗證選票:pi接收每個投票人的承諾值,并與該投票人第1 次廣播的承諾值一起作為zkSNARK 的輸入,驗證其選票的正確性.

需要注意的是,第3 步分發打開承諾的密鑰時,pi需要與其他投票人建立安全通道,安全地遞交密鑰.另外,對每個投票人pi,其VCi(Oi)的運行需要n-1 次安全的單播和2 次廣播,同時需要3 次zkSNARK 證明和3(n-1)次驗證.

基于以上的VCi(Oi)子程序,我們設計一般的選票生成協議如下.

設m個候選人{1,…,m}.投票人pi對每一個候選人c∈{1,…,m}調用生成可驗證的選票,其中,是對該候選人c“贊成與否”的投票.之后,投票人pi生成并廣播以下零知識證明:

注意到pi有所有承諾的密鑰,可以完成上述證明.最后,pi接收并驗證其他投票人的零知識證明.此時,pi有其他每一個投票人關于選票的所有承諾,可以完成對零知識證明的驗證.

通過上述過程,每個投票人都可以從m個候選人中選擇至少kmin個、至多kmax個候選人,形成有效的選票.其中,pi的選票是

2.2 投票階段

投票階段采用智能合約完成,該智能合約對應的業務邏輯如下.

1.合約的創建者初始化m個候選人n個投票人的賬戶地址.

2.投票人pi計算所有投票人的選票的哈希值Hi=H(V0,…,Vn),其中,H是一個公用的哈希算法,例如SHA-256;然后,pi把自己的選票Vi、哈希值Hi、以太幣保證金和以太幣資助金發送到智能合約.

3.如果所有投票人不能在30 個區塊時間內把自己的選票、哈希值、以太幣保證金和以太幣資助金全部發送到智能合約,則此次投票失敗.每個已經發送了選票的投票人都可以把以太幣保證金和資助金取回.

4.當所有投票人發送了自己的選票、哈希值、以太幣保證金和以太幣資助金之后,投票人pi可以打開自己選票中的承諾,取回自己的保證金.

5.當所有投票人都打開選票中的承諾后,智能合約統計所有的投票,確定候選人各自的得票數,確定獲勝者,并由獲勝者獲得所有投票人的資助金.當獲勝者有多人時,平分所有投票人的資助金.

6.如果在20 個區塊時間內,有投票人沒有打開選票中的承諾,則這些投票人的保證金由m個候選人平分,同時把所有的資助金返還給各個投票人,投票失敗.

3 投票階段智能合約的實現和測試

3.1 投票階段智能合約的實現

我們在以太坊中使用Solidity 語言實現了投票階段智能合約.簡單起見,合約包含1 個合約創建者、2 個候選人和2 個投票人.多個投票人和候選人的情況可以類推.合約代碼的命名主要參考了Solidity 官網中電子投票的智能合約[24],然后根據我們的以太幣投票協議完善了投票功能.

首先,我們定義投票人和候選人的結構體.投票人結構體如下.

其中,id 代表投票人的地址,rights 代表是否被合約部署人授予投票權,voted 指是否承諾并投票,claimed 指是否打開承諾取回押金,commitA、commitB 和commits 分別代表投票人對候選人proposalA 和proposalB 的承諾值以及所有投票人選票的哈希值,openkeyA 和openkeyB 分別代表投票人對候選人proposalA 和proposalB打開承諾的值.

候選人結構體中,id 代表候選人地址,index 是候選人對應的一個數標,voteCount 統計該候選人的所有選票.

接下來,對應投票階段的6 個業務邏輯,依次實現了Ballot、Commits、stopVoting、Claims、winningProposal和Prize、proposalClaim這6 組功能函數.

1.合約創建者chairperson 部署智能投票合約到區塊鏈,并指定候選人proposalA和proposalB,投票人voter1 和voter2 的地址.初始化候選人結構體,設置候選人地址,初始化proposalA對應的index 為1,proposalB對應的index 為2.初始化投票人結構體,設置投票人地址,并賦予投票人具有參與投票的權利,其他參數默認為false 或者0.

2.投票人對兩個候選人的選票表示為_commitA和_commitB,對所有投票人選票的哈希值表示為_commits.每個投票人通過交易,調用智能合約的Commits函數發送自己的選票、哈希值,同時提交保證金和資助金.本實例中,把保證金deposit 設為10 以太幣,資助金fund 設為1 以太幣,每個投票人需要一定時間內提交amounts大小為11 以太幣.智能合約會判斷投票人交易中的amounts,確認保證金和資助金恰好是11 以太幣,若多了則返回,若不夠則退回投票人要求重新提交.另外,該函數還會統計提交選票的人數,且記錄第1 個選票提交時的區塊高度,以配合其他函數完成“時間承諾”的功能.與普通的“時間承諾”相比,我們規定了提交選票操作的允許時間段,開始時間為第1 個投票人提交選票的區塊時間,最多持續30 個區塊時間后結束.計時結束后不能再提交選票,只能取回提交的保證金并停止此次投票.另外,該函數會判斷每個人所提交的各自的_commits是否一致,并且在所有投票人提交選票后判斷每個人提交的_commits是否與智能合約按照每個人的選票計算的哈希值一致.這一步驟主要是為了判斷所有投票人是否就選票達成了一致,具有比特幣投票協議中“聯合交易”的特點.

下面給出該函數的部分核心代碼,其中,msg.sender表示合約接口的調用者,msg.value表示調用該合約接口交易發送給合約的交易金額.

3.注意到,在智能合約的Commits函數中,第1 個投票人調用時,合約會記錄下區塊高度.在30 個區塊之后,每個投票人都可以在投票失敗的情況下調用stopVoting函數來終止投票,取回保證金和資助金.該函數執行時,會首先根據當前區塊判斷時間是否已經超過了30 個區塊,如果確實超過了30 個區塊,并且所有的投票人確實沒有全部參與該次投票,而且該函數的調用方確實參與了投票,就可以把該參與方的保證金和資助金退回.如果以上條件不滿足,則不會執行任何操作.

4.如果所有投票人都發送了自己的選票、哈希值、保證金和資助金,每個投票人就可以通過調用Claims函數,打開自己選票的承諾值以取回自己的保證金.該函數的輸入包括每個選票中的承諾的打開密鑰,在本實例中,選票的承諾值就是哈希值,所以相應的承諾打開密鑰就是哈希值的原像,對一個候選人而言,就是選票生成階段的.該函數會首先驗證調用合約的投票人是否已經取回保證金.若是,則退出合約.否則,該函數繼續驗證投票人是否能正確打開承諾,如果能夠順利打開承諾,則返還投票人保證金,更新投票人狀態為已返還保證金,累加打開承諾的人數;如果不能正確打開承諾,則退出合約.

同時,該函數還會記錄第1 次有投票人打開承諾時的區塊高度,投票人只能在第1 次打開承諾后20 個區塊內打開承諾取回保證金,否則會被候選人平分.

下面給出該函數的部分核心代碼.

5.當所有投票人都打開選票中的承諾后,智能合約統計所有的投票,確定候選人各自的得票數,確定獲勝者.所有人都可以通過winningProposal函數查看獲勝者.獲勝者可以通過Prize函數獲得所有投票人的資助金.當獲勝者有多人時,獲勝者中的任意一人調用Prize函數,智能合約平分所有投票人的資助金給所有獲勝者.

6.如果在第1 次打開承諾后,有20 個新區塊生成還有投票人沒有打開承諾,則投票失敗,由候選人平分所有沒有取回的保證金,同時把投票人交的資助金返還.只有候選人才能調用proposalClaim函數.該函數首先判斷是否所有承諾者打開了承諾.若是,則退出合約.否則,繼續判斷在第1 次打開承諾后是否已有20 個新區塊生成:若是,則統計所有沒取回的保證金,由候選人平分,同時把資助金返還給投票人;否則,退出合約.

3.2 投票階段智能合約的測試

我們使用基于智能合約瀏覽器的開發環境browser-solidity 進行了仿真測試,驗證了上述代碼的正確性.

1.Ballot函數:Ballot函數是智能合約的構造函數,當合約創建者在區塊鏈中部署合約時會觸發該函數.在browser-solidity 開發環境中,通過點擊“Create”按鈕,即可完成智能合約的部署.如果合約部署成功,則開發環境中會給出智能合約的函數運行接口和對應的參數輸入框,如圖1 所示.

Fig.1 Costs and smart contract interfaces returned by the development environment after a successful deployment圖1 部署智能合約成功后開發環境返回的合約函數接口和相關開銷

合約創建者在部署智能合約時需要在對應的參數輸入框傳入4 個地址,前兩個是候選人地址,后兩個是投票人地址:

?“0x14723a09acff6d2a60dcdf7aa4aff308fddc160c”;

?“0x4b0897b0513fdc7c541b6d9d7e929c4e5364d2db”;

?“0x583031d1113ad414f02576bd6afabfb302140225”;

?“0xdd870fa1b7c4700f2bd7f44238821c26f7392148”.

當合約部署成功后,開發環境會返回交易的相關開銷.圖1 中,“Execution cost”是存儲全局變量和方法調用運行時間的所有開銷,“Transaction cost”是由編譯合約的開銷加上“Execution cost”的開銷得到的.如果合約部署失敗會提示相應的錯誤.

2.Commits函數:兩個投票人提交保證金、獎金和選票和哈希值.注意到,選票是在選票生成階段得到的,采用的是哈希函數,投票人voter1 的選票是:

?“0x8d17b2536d3905e4b709f53152aaa15327030c1cc96e6828c41c63f558aba405”;

?“0xb7eecb2394b8fd348adecb8bffd0f75e45e5054a3386f36b2da11ca733bfe517”.

投票人voter1 使用在選票生成階段獲得的voter2 的選票,計算包括雙方選票的哈希值:

之后,voter1 在browser-solidity 開發環境中觸發Commits函數,輸入上述選票和哈希值,設置運行環境、賬戶、交易金額等信息,然后執行該函數.圖2 給出了該函數執行的參數和結果信息,其中,“Environment”指明運行環境是JavaScript VM,為本地虛擬調試模式;“Account”即voter1 的賬戶地址信息;“Gas limit”指明交易費的上限;“Value”即交易金額,包括保證金和獎金.該函數成功執行后,會返回默認結果“0X”;同時,開發環境顯示此次函數執行的相關開銷.

Fig.2 Parameters and results of the Commits function executed by the voter1圖2 voter1 執行Commits 函數的參數及結果

投票人voter2 類似地把自己的選票、哈希值、保證金、獎金通過交易發布到以太坊中,其中,voter2 的選票是:

?“0x0c7c173185d95a8187b90977b78f7dd9724c64d64dad4fe82f8f479b65a61376”;

?“0x6e0b3b51af1129b42809b2c993c6d3d6a8a38da95e5ef95c24ea3654662d2dc1”.

其計算的哈希值包括選票生成階段獲得的voter1 的選票信息:

如我們所期望的,兩個選票人的哈希值應當是一致的.

3.stopVoting函數:投票人可以隨時觸發該函數,但是根據該函數的實現邏輯,只有某些投票人不在30 個區塊時間內提交選票時,已提交過選票的投票人觸發該函數才是有意義的.這些提交過選票的投票人可以通過該函數要回自己的保證金和獎金.此時該輪投票已經失敗,需要合約創建者重新觸發Ballot函數,才能發起一輪新的投票.圖3 是在voter1 投票完成、voter2 沒有投票時,由voter1 觸發的函數執行結果,執行成功返回的是默認結果“0X”.

Fig.3 A voter gets back their deposits and rewards,and stops the voting圖3 投票人取回保證金和獎金并結束投票

4.Claims函數:投票人提交選票對應的承諾值,取回保證金.在本測試例中,選票生成階段voter1 的真實投票是(“1”,“1”),即對兩個候選人投投了贊成票.選票生成階段,voter1 用于混淆真實投票的隨機數是(“3”,“7”),所以voter1 選票對應的承諾值是(“4”,“8”).

在browser-solidity 開發環境中,voter1 提交(“4”,“8”),取回保證金,如圖4 所示.

Fig.4 voter1 submits the commitment value of their ballot and gets back their deposit圖4 voter1 提交選票的承諾值,取回保證金

類似地,voter2 的真實投票是(“0”,“1”),對應的隨機數為(“-3”,“-7”),承諾值是(“-3”,“-6”).在browser-solidity開發環境中,voter2 提交(“-3”,“-6”),取回保證金.

5.winningProposal函數和Prize函數:在所有投票人提交承諾值之后,任何實體都可以調用winningProposal函數查看獲勝者.圖5 展示了觸發winningProposal后得到的返回結果.可以看到,返回的結果是2,表明獲勝者是proposalB.

Fig.5 Trigger the winningProposal function and get the returned value圖5 觸發winningProposal 函數獲得返回值

此時,獲勝者proposalB可以觸發Prize函數,獲得獎金,圖6 展示了該函數的執行結果.

Fig.6 Execution status after a winner triggers the Prize function圖6 獲勝者觸發Prize 函數后的執行情況

6.proposalClaim函數:如果有投票人在第1 個投票人公布承諾值之后的20 個區塊時間內不公布自己的承諾值,其保證金作為罰金由候選人平分.在測試例中,voter1 提交了承諾值,voter2 沒有提交承諾值,此時,任意候選人都可以調用該函數,由候選人平分保證金.該函數會返回“Vote Fail Fine”提示,如圖7 所示.

Fig.7 Execution status of sharing deposits after a candidate triggers the proposalClaim function圖7 候選人觸發proposalClaim 函數平分保證金的執行情況

上述智能合約的測試表明:在兩個投票人、兩個候選人、一個合約創建者的情況下,可以通過智能合約完成電子投票.當投票人和候選人的數量增加后,可以通過適應性的修改代碼,完成投票.在本測試例中,proposalB得到了2 票,因為只有兩個投票人,可以無異議地推斷出每個投票人對于proposalB的真實投票,這種信息泄露自然是允許的.對于proposalA,通過查詢可以知道其獲得的投票是1 票,那么通過“4”和“-3”無法推斷出這一票到底是誰投的,投票人具有隱私性.

4 投票階段智能合約的邏輯驗證

4.1 投票階段智能合約的模型

我們采用了模型檢驗工具來驗證投票階段智能合約的內在邏輯,主要驗證了步驟2～步驟6 以太幣流通的內在邏輯,包括:

(1)投票人根據步驟2 的合約內容提交保證金和資助金,如果在規定時間內有的投票人沒有提交保證金和資助金,則步驟3 的合約內容能夠順利執行,即已經提交以太幣的投票人能夠順利地取回自己的保證金和資助金.

(2)投票人根據步驟4 的合約內容提交選票后,可以順利取回保證金.

(3)候選人根據步驟5 的合約內容,獲勝者可以順利領到獎金.

(4)候選人根據步驟6 的合約內容,如果在規定時間內有的投票人沒有取回保證金,則能夠平分沒有取回的保證金.

由于上述驗證的智能合約只涉及以太幣的流通情況,我們把原智能合約中步驟2 提交選票和步驟4 提交選票承諾值的過程簡化為在步驟4 直接提交真實選票.這當然意味著我們的驗證邏輯不涉及隱私性的驗證.但是這樣簡化之后,對以太幣的流通情況并沒有任何的修改,所以驗證的結果對于原智能合約的以太幣流通情況是有效的.事實上,通過邏輯驗證,我們確認了Zhao 等人的比特幣投票協議[4]并沒有完備地考慮比特幣的流通.例如,當誠實的投票人公開承諾值,取回保證金之后,如果有不誠實的投票人沒有公開承諾值,則所有投票人的資助金不能被候選人領取,也不能退還投票人.這形成了事實上的資助金“黑洞”.由于礦工可以把交易的輸入輸出差額作為自己的收入,這在事實上鼓勵了礦工不誠實的執行協議,以形成資助金黑洞,獲得比特幣.本文使用了Spin 模型,給出1 個時間進程、5 個投票人進程和2 個候選人進程來驗證以太幣的流通情況.

1.時間進程

時間進程用于模擬智能合約中投票人和候選人在不同的時間段內執行不同操作的行為.我們根據進程的執行時間,保守地選取了2s 作為一個時間段.具體來說,投票人需要在程序開始執行后2s 以內完成保證金和獎金的提交,2s～4s 內完成選票的提交,超過 4s 停止計時.注意到,在智能合約的實現上,Commits、Claims、proposalClaim等函數都有計時器的功能,與該時間進程對應.使用Promela 描述,時間進程核心代碼如下.

2.投票人進程

投票人進程是投票人允許的所有操作.根據時間進程的不同,投票人在0～2s、2s～4s 這樣兩個時間段可以執行3 個不同的原子操作.原子操作在Spin 中用關鍵字atomic標識,標識范圍內的代碼執行時不可分割.我們設置了5 個投票人,每個投票人用其進程號減去1 的值(pid-1)來標識,可以看作不同投票人的編號.對每一個投票人,我們設置了usrmoney來表示該投票人的賬戶余額,初始化每個賬戶為11,設置了Contractmoney代表智能合約的余額.注意,在在智能合約中,投票人的對手方是智能合約.與投票協議相關的變量包括rights、voted和votersNum,其中,rights表示用戶有一次的投票權,voted表示投票者是否提交了保證金和資助金到智能合約,而votersNum則統計了提交保證金和資助金到智能合約的人數,分別與智能合約的狀態變量一一對應.

在0～2s,投票人的原子操作如下所示,對應實現了智能合約步驟2 的資金流向和投票狀態的改變.

在2s 后,投票人的原子操作分兩種情況:一種是Commits順利執行的情況,對應Claims函數;一種是Commits階段有投票人沒有參與的情況,對應stopVoting函數.這兩種情況涵蓋了智能合約步驟3 和步驟4 的資金流向和投票狀態的改變.

在有投票人沒有參與Commits函數時,votersNum小于投票人的總數,執行下面的操作,實現了stopVoting相同功能.

同樣在2s～4s,當所有投票人都參與了Commits函數時,投票人可以執行Claims函數.該函數對應的操作如下.

其中,voteId代表隨機選擇的候選人,count[voteId]用來統計候選人的投票總數,這兩個狀態量表示了簡化的投票過程;claimed標記是否已參與Commits函數,用backNum統計取回保證金的人數,與Claims函數的backNum對應.

3.候選人進程

候選人進程對應候選人可以運行的所有操作.從時間進程上看,候選人的操作時間有兩個起點:一個是2s～4s 內投票人完成投票后,候選人可以開始確認勝利者和獲得獎金;一個是4s 后依舊有投票人沒有投票,候選人從4s 開始可以平分投票人的保證金.第1 種情況使用backNum這個記錄返回保證金的狀態量來標識,投票人在2s～4s 內完成投票取回保證金,那么這個狀態量是5;第2 種情況使用了時間和backNum狀態量以及votersNum狀態量來標識,其中,votersNum表示Commits階段成功執行了,是候選人平分保證金的前提條件.

投票人完成投票時,候選人的操作如下所示,對應winningProposal函數和Prize函數.

其中,count是在投票操作時記錄的投票.在測試例中,每個投票人要么選0 要么選1,不存在平票的情況.獎金的流向也是要么給候選人A的賬戶moneyA,要么給候選人B的賬戶moneyB.

如果投票人完成了承諾卻沒有完成投票,時間也大于 4s 了,候選人就可以平分投票人的保證金.對應proposalClaim函數,其中,getDepositA和getDepositB表明候選人取得了保證金.

4.邏輯驗證

前面我們定義了投票人、候選人、時間進程,這些進程運行之后模擬智能合約投票階段的運行,運行的結果可以反映資金的可能流向.我們使用LTL 描述期望的運行結果,如果實際的運行結果與期望的運行結果相同,則表明資金的流向滿足我們的期望;否則,表明資金流向存在問題.鑒于投票人進程運行的代碼是完全一致的,我們在驗證資金流向時,僅選取了一個下標為0 的投票人,即第1 個投票人的進程.

我們期望驗證的4 個資金流向邏輯描述如下.

?ltlbackMoney{[?]((votersNum＜5 &&voted[0]==1)-＞＜＞(userMoney[0]==11))}

該邏輯定義為backMoney.投票人根據步驟2的合約內容提交保證金和資助金.如果在規定時間內有的投票人沒有提交保證金和資助金,根據投票人的定義,即votersNum＜5.此時,已經提交保證金和資助金的投票人根據投票人的定義,voted[0]為1.那么,這樣的投票人應該可以取回保證金和資助金,即可以期望userMoney[0]為11.

?ltlIfrightsThenbackDeposit{[?](claimed[0]==1-＞＜＞(userMoney[0]==10))}

該邏輯定義為IfVotedThenbackDeposit.根據投票人的定義,如果投票人完成了投票,那么claimed[0]應該為1.此時,投票人應該同時取回了保證金,所以期望賬戶余額userMoney應該是10.對應智能合約的Claims函數的資金流向.

?ltlIfSuccessThenOneGetPrize{[?](backNum==5-＞＜＞(moneyA==5 &&moneyB==5))}

該邏輯定義為IfSuccessThenOneGetPrize.根據候選人的定義,如果backNum==5 即投票成功了.此時,可以期望候選人獲得了獎金,則此時獲勝者賬戶余額應該為5.

?ltlIfFaildThenGetDeposit{[?]((votersNum==5 &&backNum＜5)-＞＜＞(getDepositA==1 &&getDepositB==1))}

該邏輯定義為IfFaildThenGetDeposit.根據候選人的定義,若所有投票人交了保證金和資助金(votersNum==5),但是有投票人沒有取回保證金(backNum＜5),那么可以期望候選人A和B平分投票人沒有取回的保證金,即getDepositA和getDepositB都是1.

5.邏輯驗證結果

我們把第3 節的各種進程的定義和第4 節的邏輯驗證形成了4 個ballotContract.pml 文件,每個文件中包含完整的進程定義和1 個單獨的邏輯驗證條件.對于每一個邏輯驗證條件,在Windows 平臺的命令行界面下運行6.4.3 版本的Spin 程序,執行spin -a ballotContract.pml,生成c 語言的模型檢測程序pan.c,并在命令行中顯示該代碼所檢測的邏輯驗證條件.然后執行gcc -o pan pan.c 命令編譯,生成可執行程序pan.該pan 程序運行時間進程、投票人進程、候選人進程,嘗試所有可能的狀態,以判斷投票人進程和候選人進程能否滿足其邏輯驗證條件.

如圖8 所示,4 個邏輯驗證條件的運行結果是類似的,只有相關狀態和運行序列的不同,而遍歷的狀態總數是確定的,結論也是相同的,即滿足邏輯驗證條件(errors=0).

Fig.8 Logic verification result of the smart contracts圖8 智能合約邏輯驗證結果

Fig.8 Logic verification result of the smart contracts (Continued)圖8 智能合約邏輯驗證結果(續)

5 結 論

本文給出了一個保持隱私的以太幣投票協議,特別是其投票階段的智能合約.我們給出了在以太坊中智能合約的詳細實現過程,并給出了測試結果.進一步地,我們對智能合約和實現的代碼進行了邏輯驗證,確保智能合約的資金流向是符合預期的.我們同時指出了Zhao 等人給出的比特幣投票協議因為缺乏邏輯驗證的過程,存在資金流向黑洞的問題.