基于智能合約的以太幣投票協(xié)議?

付利青 , 田海博

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

2(廣東省信息安全技術(shù)重點(diǎn)實(shí)驗(yàn)室(中山大學(xué)),廣東 廣州 510006)

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

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

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

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

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

1 相關(guān)工作

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

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

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

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

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

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

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

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

1.1 主要貢獻(xiàn)

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

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

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

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

2.1 選票生成

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

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

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

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

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

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

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

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

基于以上的VCi(Oi)子程序,我們?cè)O(shè)計(jì)一般的選票生成協(xié)議如下.

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

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

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

2.2 投票階段

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.2 投票階段智能合約的測(cè)試

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

1.Ballot函數(shù):Ballot函數(shù)是智能合約的構(gòu)造函數(shù),當(dāng)合約創(chuàng)建者在區(qū)塊鏈中部署合約時(shí)會(huì)觸發(fā)該函數(shù).在browser-solidity 開發(fā)環(huán)境中,通過點(diǎn)擊“Create”按鈕,即可完成智能合約的部署.如果合約部署成功,則開發(fā)環(huán)境中會(huì)給出智能合約的函數(shù)運(yùn)行接口和對(duì)應(yīng)的參數(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í)需要在對(duì)應(yīng)的參數(shù)輸入框傳入4 個(gè)地址,前兩個(gè)是候選人地址,后兩個(gè)是投票人地址:

?“0x14723a09acff6d2a60dcdf7aa4aff308fddc160c”;

?“0x4b0897b0513fdc7c541b6d9d7e929c4e5364d2db”;

?“0x583031d1113ad414f02576bd6afabfb302140225”;

?“0xdd870fa1b7c4700f2bd7f44238821c26f7392148”.

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

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

?“0x8d17b2536d3905e4b709f53152aaa15327030c1cc96e6828c41c63f558aba405”;

?“0xb7eecb2394b8fd348adecb8bffd0f75e45e5054a3386f36b2da11ca733bfe517”.

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

之后,voter1 在browser-solidity 開發(fā)環(huán)境中觸發(fā)Commits函數(shù),輸入上述選票和哈希值,設(shè)置運(yùn)行環(huán)境、賬戶、交易金額等信息,然后執(zhí)行該函數(shù).圖2 給出了該函數(shù)執(zhí)行的參數(shù)和結(jié)果信息,其中,“Environment”指明運(yùn)行環(huán)境是JavaScript VM,為本地虛擬調(diào)試模式;“Account”即voter1 的賬戶地址信息;“Gas limit”指明交易費(fèi)的上限;“Value”即交易金額,包括保證金和獎(jiǎng)金.該函數(shù)成功執(zhí)行后,會(huì)返回默認(rèn)結(jié)果“0X”;同時(shí),開發(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 類似地把自己的選票、哈希值、保證金、獎(jiǎng)金通過交易發(fā)布到以太坊中,其中,voter2 的選票是:

?“0x0c7c173185d95a8187b90977b78f7dd9724c64d64dad4fe82f8f479b65a61376”;

?“0x6e0b3b51af1129b42809b2c993c6d3d6a8a38da95e5ef95c24ea3654662d2dc1”.

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

如我們所期望的,兩個(gè)選票人的哈希值應(yīng)當(dāng)是一致的.

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

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

4.Claims函數(shù):投票人提交選票對(duì)應(yīng)的承諾值,取回保證金.在本測(cè)試?yán)?選票生成階段voter1 的真實(shí)投票是(“1”,“1”),即對(duì)兩個(gè)候選人投投了贊成票.選票生成階段,voter1 用于混淆真實(shí)投票的隨機(jī)數(shù)是(“3”,“7”),所以voter1 選票對(duì)應(yīng)的承諾值是(“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 的真實(shí)投票是(“0”,“1”),對(duì)應(yīng)的隨機(jī)數(shù)為(“-3”,“-7”),承諾值是(“-3”,“-6”).在browser-solidity開發(fā)環(huán)境中,voter2 提交(“-3”,“-6”),取回保證金.

5.winningProposal函數(shù)和Prize函數(shù):在所有投票人提交承諾值之后,任何實(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ù)獲得返回值

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

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

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

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

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

4 投票階段智能合約的邏輯驗(yàn)證

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

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

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

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

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

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

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

1.時(shí)間進(jìn)程

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

2.投票人進(jìn)程

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

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

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

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

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

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

3.候選人進(jìn)程

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

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

其中,count是在投票操作時(shí)記錄的投票.在測(cè)試?yán)?每個(gè)投票人要么選0 要么選1,不存在平票的情況.獎(jiǎng)金的流向也是要么給候選人A的賬戶moneyA,要么給候選人B的賬戶moneyB.

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

4.邏輯驗(yàn)證

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

我們期望驗(yàn)證的4 個(gè)資金流向邏輯描述如下.

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

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

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

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

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

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

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

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

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

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

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

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

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

5 結(jié) 論

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