《電子技術應用》
您所在的位置:首頁 > 通信与网络 > 设计应用 > The DAO事件的形式化分析
The DAO事件的形式化分析
信息技术与网络安全
朱雪阳1,2
(1.中国科学院 软件研究所 计算机科学国家重点实验室,北京100190;2.中国科学院大学,北京100049)
摘要: 随着区块链应用的推广与深入,智能合约的作用越来越突出,智能合约的安全问题也更加突显。由于区块链不可篡改的特点,智能合约一旦部署不可更改。在开发阶段保证智能合约的可靠性显得尤为重要。在The DAO事件中,由于智能合约中存在一种被称为重入漏洞的错误,黑客得以窃取在当时价值巨大的以太币。通过形式化分析来更清晰地展示重入漏洞的特点及重入攻击行为,并以此为例介绍基于模型检测技术的智能合约形式化验证方法。
中圖分類號: TP301
文獻標識碼: A
DOI: 10.19358/j.issn.2096-5133.2021.05.003
引用格式: 朱雪陽. The DAO事件的形式化分析[J].信息技術與網絡安全,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)的學者于2008年提出了比特幣概念并于2009年初發行了最初的50個比特幣[1]。隨后,人們發現比特幣底層所用的區塊鏈技術并不僅僅限于加密數字貨幣的應用[2];特別是提供智能合約[3]編程的開放區塊鏈平臺以太坊(Ethereum)[4]的創立,使區塊鏈技術的發展更加生機勃勃。

區塊鏈是一種將數據區塊按照時間順序組織起來的加密鏈式結構,是一種不可篡改和不可偽造的去中心化共享賬本。加入智能合約后,區塊鏈技術可看作是一種新型的去中心化基礎架構與分布式計算范式[5]。有了智能合約,開發人員能夠在區塊鏈上建立和發布各種分布式應用,為區塊鏈技術的應用提供了無限的可能。

智能合約最初由SZABO N提出[6](1997年正式發表[7]),是以數字形式定義的一組承諾,以及合約參與方執行這些承諾所需的協議。智能合約的本質是運行于區塊鏈這一去中心化基礎架構上的分布式程序,是運行在共享區塊鏈數據賬本上的商業邏輯,在被觸發時自動執行。

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



本文詳細內容請下載:http://m.tom3567.com/resource/share/2000003545




作者信息:


朱雪陽1,2

(1.中國科學院 軟件研究所 計算機科學國家重點實驗室,北京100190;2.中國科學院大學,北京100049)


此內容為AET網站原創,未經授權禁止轉載。
主站蜘蛛池模板: 日韩欧美在线播放视频| 久久精品国产v日韩v亚洲| 国产欧美日韩视频| 国产精品久久久久免费| 亚洲一区精品电影| 亚洲字幕一区二区| 久久国产精品视频在线观看| 99精品在线免费视频| 久久久久免费精品国产| 亚洲综合最新在线| 国产精品91在线| 久久99视频免费| 欧美日韩福利视频| 日韩中文字幕av| 中文字幕av日韩精品| 国产精品麻豆va在线播放| 日韩一区二区三区资源| 国产欧美日韩中文| 日韩在线视频免费观看| 亚洲一区二区三区免费观看| 人妻少妇精品久久| 日韩中文字幕亚洲精品欧美| 国产精品一区二区免费看| 91精品国产91久久久久青草| 久久精品国产视频| 奇米影视亚洲狠狠色| 日本一区免费看| 久久久亚洲影院| 国产免费一区二区视频| 国产欧美日韩中文字幕| 91成人精品网站| 国产精品日韩av| 国产精品视频不卡| 美日韩精品视频免费看| 免费在线国产精品| 精品国产综合久久| 少妇人妻无码专区视频| 国产精品观看在线亚洲人成网| 久久久精品在线视频| 久久久久久久久久久久久久久久久久av | 亚洲日本无吗高清不卡|