关键词:
区块链
以太坊
去中心化应用
智能合约
模型检查
摘要:
由于区块链不可篡改特性,已经部署上线的智能合约代码,将无法修改或升级。一旦智能合约因为自身代码设计产生的问题,导致的智能合约安全漏洞,以致整个区块链应用土崩瓦解,或将产生不可逆转的重大损失。而使用一些代码缺陷检查方法,例如模型检查、静态代码分析等技术,提前发现程序缺陷代码,及时修改问题代码,可起防患于未然的作用。本文基于以太坊区块链平台,以开发安全的去中心的区块链应用作为切入点,对区块链技术原理、以太坊区块链去中心化应用框架、区块链智能合约开发、以太坊智能合约缺陷漏洞方面等展开深入研究,并提出一种结合形式化验证的模型检查技术和静态代码检查技术的,对智能合约缺陷漏洞进行验证的工具框架。本文最后基于区块链应用框架和安全验证的工具框架,开发了一款区块链去中心化应用“加密熊猫”,和一个自动化以太坊智能合约漏洞安全检查工具,并详细介绍去中心化应用“加密熊猫”和智能合约验证工具的开发过程和技术原理。论文主要研究分为以下几个方面(1)研究区块链技术和以太坊区块链平台,总结了一个以太坊区块链平台去中心化的应用框架;并依据该框架,在以太坊平台上开发了一款区块链去中心化应用。(2)总结了以太坊区块链平台上的智能合约几种常见的安全漏洞模型,结合区块链技术和代码安全检查技术,分析了各智能合约漏洞产生的原因和不同漏洞安全验证的方法(3)结合形式化验证的模型检查和静态代码检查技术,基于智能合约漏洞模型和安全验证方法,提出了一种自动化智能合约安全验证工具框架,并基于该框架,开发了一款自动化以太坊智能合约漏洞安全验证工具论文最后对区块链应用和智能合约安全验证工具进行演示和性能测试,从测试结果来看,论文开发的区块链去中心化应用具备透明、可追踪、不可篡改、隐私保护等特性,对比传统应用来看,有革命性意义;漏洞安全检查工具也可以有效的检查出区块链智能合约代码中基本的缺陷漏洞,效果作用明显,对开发安全的区块链应用,有非常重要的意义。