期刊文献+

The DAO事件的形式化分析 被引量:5

Formal analysis of the DAO exploit
下载PDF
导出
摘要 随着区块链应用的推广与深入,智能合约的作用越来越突出,智能合约的安全问题也更加突显。由于区块链不可篡改的特点,智能合约一旦部署不可更改。在开发阶段保证智能合约的可靠性显得尤为重要。在The DAO事件中,由于智能合约中存在一种被称为重入漏洞的错误,黑客得以窃取在当时价值巨大的以太币。通过形式化分析来更清晰地展示重入漏洞的特点及重入攻击行为,并以此为例介绍基于模型检测技术的智能合约形式化验证方法。 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.
作者 朱雪阳 Zhu Xueyang(State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China;University of the Chinese Academy of Sciences,Beijing 100049,China)
出处 《信息技术与网络安全》 2021年第5期13-19,共7页 Information Technology and Network Security
关键词 智能合约 形式化验证 模型检测 安全漏洞 smart contract formal verification model checking vulnerability
  • 相关文献

参考文献4

二级参考文献19

共引文献331

同被引文献52

引证文献5

二级引证文献59

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部