《電子技術(shù)應(yīng)用》
您所在的位置:首頁(yè) > 通信與網(wǎng)絡(luò) > 設(shè)計(jì)應(yīng)用 > The DAO事件的形式化分析
The DAO事件的形式化分析
信息技術(shù)與網(wǎng)絡(luò)安全
朱雪陽(yáng)1,2
(1.中國(guó)科學(xué)院 軟件研究所 計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室,北京100190;2.中國(guó)科學(xué)院大學(xué),北京100049)
摘要: 隨著區(qū)塊鏈應(yīng)用的推廣與深入,智能合約的作用越來越突出,智能合約的安全問題也更加突顯。由于區(qū)塊鏈不可篡改的特點(diǎn),智能合約一旦部署不可更改。在開發(fā)階段保證智能合約的可靠性顯得尤為重要。在The DAO事件中,由于智能合約中存在一種被稱為重入漏洞的錯(cuò)誤,黑客得以竊取在當(dāng)時(shí)價(jià)值巨大的以太幣。通過形式化分析來更清晰地展示重入漏洞的特點(diǎn)及重入攻擊行為,并以此為例介紹基于模型檢測(cè)技術(shù)的智能合約形式化驗(yàn)證方法。
中圖分類號(hào): TP301
文獻(xiàn)標(biāo)識(shí)碼: A
DOI: 10.19358/j.issn.2096-5133.2021.05.003
引用格式: 朱雪陽(yáng). The DAO事件的形式化分析[J].信息技術(shù)與網(wǎng)絡(luò)安全,2021,40(5):13-19.
Formal analysis of the DAO exploit
Zhu Xueyang1,2
(1.State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China; 2.University of the Chinese Academy of Sciences,Beijing 100049,China)
Abstract: Along with the spread and deepening of blockchain technology application, the role of smart contracts inevitably become more and more important, and the security of smart contracts must receive more attention. Due to the immutable nature of blockchain, once a smart contract is deployed,it cannot be changed. Therefore, it is particularly important to guarantee the reliability during the development stage of smart contracts. In the DAO exploit, hackers were able to steal lots of ether, which was of great value at the time, due to a vulnerability called Reentrancy. This paper illustrates the feature of the vulnerability and the attack behavior by formal analysis, and by which the model checking based formal verification of smart contracts is also introduced.
Key words : smart contract;formal verification;model checking;vulnerability

0 引言

化名為“中本聰”(Satoshi Nakamoto)的學(xué)者于2008年提出了比特幣概念并于2009年初發(fā)行了最初的50個(gè)比特幣[1]。隨后,人們發(fā)現(xiàn)比特幣底層所用的區(qū)塊鏈技術(shù)并不僅僅限于加密數(shù)字貨幣的應(yīng)用[2];特別是提供智能合約[3]編程的開放區(qū)塊鏈平臺(tái)以太坊(Ethereum)[4]的創(chuàng)立,使區(qū)塊鏈技術(shù)的發(fā)展更加生機(jī)勃勃。

區(qū)塊鏈?zhǔn)且环N將數(shù)據(jù)區(qū)塊按照時(shí)間順序組織起來的加密鏈?zhǔn)浇Y(jié)構(gòu),是一種不可篡改和不可偽造的去中心化共享賬本。加入智能合約后,區(qū)塊鏈技術(shù)可看作是一種新型的去中心化基礎(chǔ)架構(gòu)與分布式計(jì)算范式[5]。有了智能合約,開發(fā)人員能夠在區(qū)塊鏈上建立和發(fā)布各種分布式應(yīng)用,為區(qū)塊鏈技術(shù)的應(yīng)用提供了無限的可能。

智能合約最初由SZABO N提出[6](1997年正式發(fā)表[7]),是以數(shù)字形式定義的一組承諾,以及合約參與方執(zhí)行這些承諾所需的協(xié)議。智能合約的本質(zhì)是運(yùn)行于區(qū)塊鏈這一去中心化基礎(chǔ)架構(gòu)上的分布式程序,是運(yùn)行在共享區(qū)塊鏈數(shù)據(jù)賬本上的商業(yè)邏輯,在被觸發(fā)時(shí)自動(dòng)執(zhí)行。

正如軟件在網(wǎng)絡(luò)安全的研究與實(shí)踐中扮演著至關(guān)重要的角色,幾乎所有的網(wǎng)絡(luò)攻擊都是利用系統(tǒng)軟件或應(yīng)用軟件中存在的安全缺陷實(shí)施的[8]。在區(qū)塊鏈系統(tǒng)安全中,智能合約也扮演著重要的角色。如著名的The DAO事件[9],由于智能合約中存在安全漏洞,黑客得以竊取在當(dāng)時(shí)價(jià)值超過五千萬(wàn)美元的360萬(wàn)個(gè)以太幣。智能合約的安全(security)問題得到廣泛關(guān)注[10];許多用于合約漏洞檢查的原型工具應(yīng)運(yùn)而生,如采用符號(hào)化執(zhí)行[11]方法的工具Oyente[12]、Mythril[13]、Manticore[14]和Securify[15]等,以及在線檢查合約漏洞的工具如文獻(xiàn)[16]和文獻(xiàn)[17]等。



本文詳細(xì)內(nèi)容請(qǐng)下載:http://www.jysgc.com/resource/share/2000003545




作者信息:


朱雪陽(yáng)1,2

(1.中國(guó)科學(xué)院 軟件研究所 計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室,北京100190;2.中國(guó)科學(xué)院大學(xué),北京100049)


此內(nèi)容為AET網(wǎng)站原創(chuàng),未經(jīng)授權(quán)禁止轉(zhuǎn)載。
主站蜘蛛池模板: 美女下面直流白浆视频| jizz中国jizz欧洲/日韩在线| 手机免费在线**| 久久精品国产清自在天天线| 欧美人与动牲免费观看一| 亚洲综合激情另类小说区| 精品国产国产综合精品| 国产一级不卡毛片| 91香蕉视频成人| 国产白丝在线观看| 69av免费观看| 在私人影院里嗯啊h| chinese激烈高潮HD| 精品国产无限资源免费观看| 国产亚洲午夜精品| 黑人巨大无码中文字幕无码| 国产粉嫩白浆在线观看| 51精品国产人成在线观看| 国漫永生第二季在线观看| av免费不卡国产观看| 日韩亚洲综合精品国产| 亚洲一区二区观看播放| 欧美卡一卡2卡三卡4卡在线| 亚洲成色在线综合网站| 欧美精品黑人粗大| 亚洲综合无码一区二区三区 | 久久久噜久噜久久gif动图| 日韩在线精品视频| 久久精品国产精品亚洲精品| 最近中文字幕mv在线视频www | 人妻仑乱A级毛片免费看| 窈窕淑女韩国在线看| 全彩漫画口工令人垂延三尺| 精品国产一区二区三区不卡| 国产成人无码区免费内射一片色欲| 香蕉免费在线视频| 国产精品日本一区二区在线看| 8av国产精品爽爽ⅴa在线观看 | 美美女高清毛片视频免费观看| 国产AV日韩A∨亚洲AV电影| 色视频免费版高清在线观看|