付利青 , 田海博

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

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

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

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

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

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

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

1 相關(guān)工作

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

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

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

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

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

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

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

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

1.1 主要貢獻

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

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

2 以太幣投票協(xié)議

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

2.1 選票生成

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

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

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

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

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

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

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

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

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

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

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

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

2.2 投票階段

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

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

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

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

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

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

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

3 投票階段智能合約的實現(xiàn)和測試

3.1 投票階段智能合約的實現(xiàn)

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

首先,我們定義投票人和候選人的結(jié)構(gòu)體.投票人結(jié)構(gòu)體如下.

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

候選人結(jié)構(gòu)體中,id 代表候選人地址,index 是候選人對應的一個數(shù)標,voteCount 統(tǒng)計該候選人的所有選票.

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

1.合約創(chuàng)建者chairperson 部署智能投票合約到區(qū)塊鏈,并指定候選人proposalA和proposalB,投票人voter1 和voter2 的地址.初始化候選人結(jié)構(gòu)體,設置候選人地址,初始化proposalA對應的index 為1,proposalB對應的index 為2.初始化投票人結(jié)構(gòu)體,設置投票人地址,并賦予投票人具有參與投票的權(quán)利,其他參數(shù)默認為false 或者0.

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

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

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

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

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

下面給出該函數(shù)的部分核心代碼.

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

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

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

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

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

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

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

?“0x14723a09acff6d2a60dcdf7aa4aff308fddc160c”;

?“0x4b0897b0513fdc7c541b6d9d7e929c4e5364d2db”;

?“0x583031d1113ad414f02576bd6afabfb302140225”;

?“0xdd870fa1b7c4700f2bd7f44238821c26f7392148”.

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

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

?“0x8d17b2536d3905e4b709f53152aaa15327030c1cc96e6828c41c63f558aba405”;

?“0xb7eecb2394b8fd348adecb8bffd0f75e45e5054a3386f36b2da11ca733bfe517”.

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

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

Fig.2 Parameters and results of the Commits function executed by the voter1圖2 voter1 執(zhí)行Commits 函數(shù)的參數(shù)及結(jié)果

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

?“0x0c7c173185d95a8187b90977b78f7dd9724c64d64dad4fe82f8f479b65a61376”;

?“0x6e0b3b51af1129b42809b2c993c6d3d6a8a38da95e5ef95c24ea3654662d2dc1”.

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

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

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

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

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

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

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

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

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

Fig.5 Trigger the winningProposal function and get the returned value圖5 觸發(fā)winningProposal 函數(shù)獲得返回值

此時,獲勝者proposalB可以觸發(fā)Prize函數(shù),獲得獎金,圖6 展示了該函數(shù)的執(zhí)行結(jié)果.

Fig.6 Execution status after a winner triggers the Prize function圖6 獲勝者觸發(fā)Prize 函數(shù)后的執(zhí)行情況

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

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

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

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

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

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

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

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

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

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

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

1.時間進程

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

2.投票人進程

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

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

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

在有投票人沒有參與Commits函數(shù)時,votersNum小于投票人的總數(shù),執(zhí)行下面的操作,實現(xiàn)了stopVoting相同功能.

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

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

3.候選人進程

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

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

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

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

4.邏輯驗證

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

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

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

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

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

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

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

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

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

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

5.邏輯驗證結(jié)果

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

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

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

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

5 結(jié) 論

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