基于符號執(zhí)行的智能合約自動化安全審計
發(fā)布時間:2021-11-04 23:54
以太坊智能合約因其可信交易、源碼公開、不可篡改的特點,被廣泛應(yīng)用于金融、游戲以及社交媒體等領(lǐng)域。盡管在可信交易方面具有得天獨厚的優(yōu)勢,智能合約作為一門新興技術(shù),缺乏成熟完善的安全編碼規(guī)范,因此很有可能存在著安全漏洞。智能合約中存在的安全漏洞,不僅有可能會影響智能合約功能的正常使用,而且很有可能會對合約用戶造成巨大的財產(chǎn)損失。因此,對智能合約進(jìn)行安全性檢測尤為重要。本文針對已有研究關(guān)注較少而又危害較大的三類智能合約安全漏洞:任意存儲寫入漏洞、任意目的地址跳轉(zhuǎn)漏洞和gas耗盡拒絕服務(wù)漏洞,設(shè)計并實現(xiàn)了一個自動化的安全審計系統(tǒng)。主要研究內(nèi)容如下:(1)自動化檢測方案的提出。通過對存在漏洞的具體合約實例從代碼層面和匯編碼層面進(jìn)行分析,總結(jié)出漏洞產(chǎn)生的原理和條件,提出相應(yīng)的自動化檢測方案。針對任意存儲寫入漏洞,通過檢測合約執(zhí)行指令流中“SSTORE”指令參數(shù)值可取值范圍來檢測合約是否存在漏洞;針對任意目的地址跳轉(zhuǎn)漏洞,通過檢測合約執(zhí)行指令流中跳轉(zhuǎn)指令目的地址取值范圍來檢測合約是否存在漏洞;針對gas耗盡拒絕服務(wù)漏洞,利用注解技術(shù)判斷合約執(zhí)行流中是否存在循環(huán),同時檢測循環(huán)中是否存在“SSTORE”...
【文章來源】:電子科技大學(xué)四川省 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】:83 頁
【學(xué)位級別】:碩士
【部分圖文】:
以太坊的兩種賬戶圖
電子科技大學(xué)碩士學(xué)位論文102.2.2交易費(fèi)用在以太坊區(qū)塊鏈網(wǎng)絡(luò)中,交易是指由外部賬戶發(fā)送至以太坊網(wǎng)絡(luò)的一段加密簽名數(shù)據(jù),它包含了一個賬戶發(fā)送給另一個賬戶的信息。如圖2-2所示,賬戶間的交易產(chǎn)生的價值轉(zhuǎn)移和信息狀態(tài)轉(zhuǎn)換將導(dǎo)致以太坊全局狀態(tài)的轉(zhuǎn)換。圖2-2以太坊交易的狀態(tài)裝換圖以太坊交易包含兩種類型:一種為產(chǎn)生消息調(diào)用的交易,另一種為通過代碼創(chuàng)建新的合約賬戶的交易。為了避免受到分布式拒絕服務(wù)(DistributedDenialofService,DDoS)攻擊,以太坊限制了每筆交易所觸發(fā)的代碼的可計算步驟。同時,以太坊用戶為了完成一筆交易,必須要為該交易所觸發(fā)的代碼的執(zhí)行向以太坊網(wǎng)絡(luò)支付適當(dāng)?shù)馁M(fèi)用gas。在以太坊網(wǎng)絡(luò)中,每一筆交易進(jìn)行前,交易的發(fā)起者需要在交易中設(shè)置gasLimit字段值,用來表示交易發(fā)起者愿意為這筆交易所花費(fèi)的最大費(fèi)用值,此最大費(fèi)用值不能低于21000。另外,交易發(fā)起者也需要在交易中設(shè)置gasPrice字段值,用來表示每個gas單位的花銷值。因此,交易發(fā)送者完成這筆交易將總共需要花費(fèi)gasLimit×gasPrice的gas。在執(zhí)行交易的過程中,如果交易發(fā)起者賬戶余額的以太幣數(shù)量始終大于用戶愿意花費(fèi)的費(fèi)用值,那么交易可正常進(jìn)行。gasUsed表示交易實際花費(fèi)的gas值總和,對于一筆交易而言,交易所花費(fèi)的實際費(fèi)用總額為gasUsed×gasPrice。交易完成后,如果交易的gas未全部消耗完,則這些剩下的gas將返還給發(fā)送者;若在執(zhí)行交易過程中,用戶發(fā)送的gas值不足夠完成交易全部動作而導(dǎo)致gas被耗盡,那么該筆交易涉及到的所有的狀態(tài)將會被回滾到初始狀態(tài),
電子科技大學(xué)碩士學(xué)位論文12圖2-4以太坊虛擬機(jī)常用匯編指令圖2.2.4智能合約的工作過程智能合約的工作過程分為如下三步[42]。(1)智能合約的構(gòu)建與部署。首先,用戶注冊為以太坊賬戶,獲得一個公私鑰對,公鑰的后20個字節(jié)字符串為地址,表示該賬戶在以太坊網(wǎng)絡(luò)中的賬戶地址;私鑰為一串16進(jìn)制字符串,是鑒定用戶的唯一標(biāo)識。然后用戶根據(jù)實際需求與其他用戶協(xié)商好合約內(nèi)容,再使用solidity編程語言實現(xiàn)合約代碼;最后,如圖2-5所示,用戶根據(jù)協(xié)商內(nèi)容確定合約代碼無誤后,調(diào)用SOLC編譯器將合約代碼編譯成EVM虛擬機(jī)字節(jié)碼,然后將EVM虛擬機(jī)字節(jié)碼通過RPC接口發(fā)送到以太坊網(wǎng)絡(luò)。圖2-5智能合約部署流程圖
【參考文獻(xiàn)】:
期刊論文
[1]基于符號執(zhí)行的智能合約漏洞檢測方案[J]. 趙偉,張問銀,王九如,王海峰,武傳坤. 計算機(jī)應(yīng)用. 2020(04)
[2]形式化驗證方法淺析[J]. 陳波,李夫明. 電腦知識與技術(shù). 2019(34)
[3]符號執(zhí)行中的約束求解問題研究進(jìn)展[J]. 鄒權(quán)臣,吳潤浦,馬金鑫,王欣,辛偉,侯長玉,李美聰. 北京理工大學(xué)學(xué)報. 2019(09)
[4]基于混合分析的二進(jìn)制程序控制流圖構(gòu)建方法[J]. 朱凱龍,陸余良,黃暉,鄧兆琨,鄧一杰. 浙江大學(xué)學(xué)報(工學(xué)版). 2019(05)
[5]智能合約安全漏洞挖掘技術(shù)研究[J]. 付夢琳,吳禮發(fā),洪征,馮文博. 計算機(jī)應(yīng)用. 2019(07)
[6]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明. 軟件學(xué)報. 2019(01)
[7]符號執(zhí)行研究綜述[J]. 葉志斌,嚴(yán)波. 計算機(jī)科學(xué). 2018(S1)
[8]《區(qū)塊鏈:從數(shù)字貨幣到信用社會》[J]. 長鋏,韓鋒. 國企管理. 2018(07)
[9]SMT求解技術(shù)的發(fā)展及最新應(yīng)用研究綜述[J]. 王翀,呂蔭潤,陳力,王秀利,王永吉. 計算機(jī)研究與發(fā)展. 2017(07)
[10]區(qū)塊鏈技術(shù)與應(yīng)用前瞻綜述[J]. 何蒲,于戈,張巖峰,鮑玉斌. 計算機(jī)科學(xué). 2017(04)
本文編號:3476653
【文章來源】:電子科技大學(xué)四川省 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】:83 頁
【學(xué)位級別】:碩士
【部分圖文】:
以太坊的兩種賬戶圖
電子科技大學(xué)碩士學(xué)位論文102.2.2交易費(fèi)用在以太坊區(qū)塊鏈網(wǎng)絡(luò)中,交易是指由外部賬戶發(fā)送至以太坊網(wǎng)絡(luò)的一段加密簽名數(shù)據(jù),它包含了一個賬戶發(fā)送給另一個賬戶的信息。如圖2-2所示,賬戶間的交易產(chǎn)生的價值轉(zhuǎn)移和信息狀態(tài)轉(zhuǎn)換將導(dǎo)致以太坊全局狀態(tài)的轉(zhuǎn)換。圖2-2以太坊交易的狀態(tài)裝換圖以太坊交易包含兩種類型:一種為產(chǎn)生消息調(diào)用的交易,另一種為通過代碼創(chuàng)建新的合約賬戶的交易。為了避免受到分布式拒絕服務(wù)(DistributedDenialofService,DDoS)攻擊,以太坊限制了每筆交易所觸發(fā)的代碼的可計算步驟。同時,以太坊用戶為了完成一筆交易,必須要為該交易所觸發(fā)的代碼的執(zhí)行向以太坊網(wǎng)絡(luò)支付適當(dāng)?shù)馁M(fèi)用gas。在以太坊網(wǎng)絡(luò)中,每一筆交易進(jìn)行前,交易的發(fā)起者需要在交易中設(shè)置gasLimit字段值,用來表示交易發(fā)起者愿意為這筆交易所花費(fèi)的最大費(fèi)用值,此最大費(fèi)用值不能低于21000。另外,交易發(fā)起者也需要在交易中設(shè)置gasPrice字段值,用來表示每個gas單位的花銷值。因此,交易發(fā)送者完成這筆交易將總共需要花費(fèi)gasLimit×gasPrice的gas。在執(zhí)行交易的過程中,如果交易發(fā)起者賬戶余額的以太幣數(shù)量始終大于用戶愿意花費(fèi)的費(fèi)用值,那么交易可正常進(jìn)行。gasUsed表示交易實際花費(fèi)的gas值總和,對于一筆交易而言,交易所花費(fèi)的實際費(fèi)用總額為gasUsed×gasPrice。交易完成后,如果交易的gas未全部消耗完,則這些剩下的gas將返還給發(fā)送者;若在執(zhí)行交易過程中,用戶發(fā)送的gas值不足夠完成交易全部動作而導(dǎo)致gas被耗盡,那么該筆交易涉及到的所有的狀態(tài)將會被回滾到初始狀態(tài),
電子科技大學(xué)碩士學(xué)位論文12圖2-4以太坊虛擬機(jī)常用匯編指令圖2.2.4智能合約的工作過程智能合約的工作過程分為如下三步[42]。(1)智能合約的構(gòu)建與部署。首先,用戶注冊為以太坊賬戶,獲得一個公私鑰對,公鑰的后20個字節(jié)字符串為地址,表示該賬戶在以太坊網(wǎng)絡(luò)中的賬戶地址;私鑰為一串16進(jìn)制字符串,是鑒定用戶的唯一標(biāo)識。然后用戶根據(jù)實際需求與其他用戶協(xié)商好合約內(nèi)容,再使用solidity編程語言實現(xiàn)合約代碼;最后,如圖2-5所示,用戶根據(jù)協(xié)商內(nèi)容確定合約代碼無誤后,調(diào)用SOLC編譯器將合約代碼編譯成EVM虛擬機(jī)字節(jié)碼,然后將EVM虛擬機(jī)字節(jié)碼通過RPC接口發(fā)送到以太坊網(wǎng)絡(luò)。圖2-5智能合約部署流程圖
【參考文獻(xiàn)】:
期刊論文
[1]基于符號執(zhí)行的智能合約漏洞檢測方案[J]. 趙偉,張問銀,王九如,王海峰,武傳坤. 計算機(jī)應(yīng)用. 2020(04)
[2]形式化驗證方法淺析[J]. 陳波,李夫明. 電腦知識與技術(shù). 2019(34)
[3]符號執(zhí)行中的約束求解問題研究進(jìn)展[J]. 鄒權(quán)臣,吳潤浦,馬金鑫,王欣,辛偉,侯長玉,李美聰. 北京理工大學(xué)學(xué)報. 2019(09)
[4]基于混合分析的二進(jìn)制程序控制流圖構(gòu)建方法[J]. 朱凱龍,陸余良,黃暉,鄧兆琨,鄧一杰. 浙江大學(xué)學(xué)報(工學(xué)版). 2019(05)
[5]智能合約安全漏洞挖掘技術(shù)研究[J]. 付夢琳,吳禮發(fā),洪征,馮文博. 計算機(jī)應(yīng)用. 2019(07)
[6]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明. 軟件學(xué)報. 2019(01)
[7]符號執(zhí)行研究綜述[J]. 葉志斌,嚴(yán)波. 計算機(jī)科學(xué). 2018(S1)
[8]《區(qū)塊鏈:從數(shù)字貨幣到信用社會》[J]. 長鋏,韓鋒. 國企管理. 2018(07)
[9]SMT求解技術(shù)的發(fā)展及最新應(yīng)用研究綜述[J]. 王翀,呂蔭潤,陳力,王秀利,王永吉. 計算機(jī)研究與發(fā)展. 2017(07)
[10]區(qū)塊鏈技術(shù)與應(yīng)用前瞻綜述[J]. 何蒲,于戈,張巖峰,鮑玉斌. 計算機(jī)科學(xué). 2017(04)
本文編號:3476653
本文鏈接:http://www.sikaile.net/kejilunwen/ruanjiangongchenglunwen/3476653.html
最近更新
教材專著