基于符号执行的智能合约自动化安全审计
发布时间：2021-11-04 23:54
以太坊智能合约因其可信交易、源码公开、不可篡改的特点,被广泛应用于金融、游戏以及社交媒体等领域。尽管在可信交易方面具有得天独厚的优势,智能合约作为一门新兴技术,缺乏成熟完善的安全编码规范,因此很有可能存在着安全漏洞。智能合约中存在的安全漏洞,不仅有可能会影响智能合约功能的正常使用,而且很有可能会对合约用户造成巨大的财产损失。因此,对智能合约进行安全性检测尤为重要。本文针对已有研究关注较少而又危害较大的三类智能合约安全漏洞:任意存储写入漏洞、任意目的地址跳转漏洞和gas耗尽拒绝服务漏洞,设计并实现了一个自动化的安全审计系统。主要研究内容如下:（1）自动化检测方案的提出。通过对存在漏洞的具体合约实例从代码层面和汇编码层面进行分析,总结出漏洞产生的原理和条件,提出相应的自动化检测方案。针对任意存储写入漏洞,通过检测合约执行指令流中“SSTORE”指令参数值可取值范围来检测合约是否存在漏洞;针对任意目的地址跳转漏洞,通过检测合约执行指令流中跳转指令目的地址取值范围来检测合约是否存在漏洞;针对gas耗尽拒绝服务漏洞,利用注解技术判断合约执行流中是否存在循环,同时检测循环中是否存在“SSTORE”...
【文章来源】：电子科技大学四川省 211工程院校 985工程院校 教育部直属院校
【文章页数】：83 页
【学位级别】：硕士
【部分图文】：
以太坊的两种账户图
电子科技大学硕士学位论文102.2.2交易费用在以太坊区块链网络中，交易是指由外部账户发送至以太坊网络的一段加密签名数据，它包含了一个账户发送给另一个账户的信息。如图2-2所示，账户间的交易产生的价值转移和信息状态转换将导致以太坊全局状态的转换。图2-2以太坊交易的状态装换图以太坊交易包含两种类型：一种为产生消息调用的交易，另一种为通过代码创建新的合约账户的交易。为了避免受到分布式拒绝服务(DistributedDenialofService，DDoS)攻击，以太坊限制了每笔交易所触发的代码的可计算步骤。同时，以太坊用户为了完成一笔交易，必须要为该交易所触发的代码的执行向以太坊网络支付适当的费用gas。在以太坊网络中，每一笔交易进行前，交易的发起者需要在交易中设置gasLimit字段值，用来表示交易发起者愿意为这笔交易所花费的最大费用值，此最大费用值不能低于21000。另外，交易发起者也需要在交易中设置gasPrice字段值，用来表示每个gas单位的花销值。因此，交易发送者完成这笔交易将总共需要花费gasLimit×gasPrice的gas。在执行交易的过程中，如果交易发起者账户余额的以太币数量始终大于用户愿意花费的费用值，那么交易可正常进行。gasUsed表示交易实际花费的gas值总和，对于一笔交易而言，交易所花费的实际费用总额为gasUsed×gasPrice。交易完成后，如果交易的gas未全部消耗完，则这些剩下的gas将返还给发送者；若在执行交易过程中，用户发送的gas值不足够完成交易全部动作而导致gas被耗尽，那么该笔交易涉及到的所有的状态将会被回滚到初始状态，
电子科技大学硕士学位论文12图2-4以太坊虚拟机常用汇编指令图2.2.4智能合约的工作过程智能合约的工作过程分为如下三步[42]。（1）智能合约的构建与部署。首先，用户注册为以太坊账户，获得一个公私钥对，公钥的后20个字节字符串为地址，表示该账户在以太坊网络中的账户地址；私钥为一串16进制字符串，是鉴定用户的唯一标识。然后用户根据实际需求与其他用户协商好合约内容，再使用solidity编程语言实现合约代码；最后，如图2-5所示，用户根据协商内容确定合约代码无误后，调用SOLC编译器将合约代码编译成EVM虚拟机字节码，然后将EVM虚拟机字节码通过RPC接口发送到以太坊网络。图2-5智能合约部署流程图
【参考文献】：
期刊论文
[1]基于符号执行的智能合约漏洞检测方案[J]. 赵伟,张问银,王九如,王海峰,武传坤. 计算机应用. 2020(04)
[2]形式化验证方法浅析[J]. 陈波,李夫明. 电脑知识与技术. 2019(34)
[3]符号执行中的约束求解问题研究进展[J]. 邹权臣,吴润浦,马金鑫,王欣,辛伟,侯长玉,李美聪. 北京理工大学学报. 2019(09)
[4]基于混合分析的二进制程序控制流图构建方法[J]. 朱凯龙,陆余良,黄晖,邓兆琨,邓一杰. 浙江大学学报(工学版). 2019(05)
[5]智能合约安全漏洞挖掘技术研究[J]. 付梦琳,吴礼发,洪征,冯文博. 计算机应用. 2019(07)
[6]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
[7]符号执行研究综述[J]. 叶志斌,严波. 计算机科学. 2018(S1)
[8]《区块链：从数字货币到信用社会》[J]. 长铗,韩锋. 国企管理. 2018(07)
[9]SMT求解技术的发展及最新应用研究综述[J]. 王翀,吕荫润,陈力,王秀利,王永吉. 计算机研究与发展. 2017(07)
[10]区块链技术与应用前瞻综述[J]. 何蒲,于戈,张岩峰,鲍玉斌. 计算机科学. 2017(04)
本文编号：3476653
【文章来源】：电子科技大学四川省 211工程院校 985工程院校 教育部直属院校
【文章页数】：83 页
【学位级别】：硕士
【部分图文】：
以太坊的两种账户图
电子科技大学硕士学位论文102.2.2交易费用在以太坊区块链网络中，交易是指由外部账户发送至以太坊网络的一段加密签名数据，它包含了一个账户发送给另一个账户的信息。如图2-2所示，账户间的交易产生的价值转移和信息状态转换将导致以太坊全局状态的转换。图2-2以太坊交易的状态装换图以太坊交易包含两种类型：一种为产生消息调用的交易，另一种为通过代码创建新的合约账户的交易。为了避免受到分布式拒绝服务(DistributedDenialofService，DDoS)攻击，以太坊限制了每笔交易所触发的代码的可计算步骤。同时，以太坊用户为了完成一笔交易，必须要为该交易所触发的代码的执行向以太坊网络支付适当的费用gas。在以太坊网络中，每一笔交易进行前，交易的发起者需要在交易中设置gasLimit字段值，用来表示交易发起者愿意为这笔交易所花费的最大费用值，此最大费用值不能低于21000。另外，交易发起者也需要在交易中设置gasPrice字段值，用来表示每个gas单位的花销值。因此，交易发送者完成这笔交易将总共需要花费gasLimit×gasPrice的gas。在执行交易的过程中，如果交易发起者账户余额的以太币数量始终大于用户愿意花费的费用值，那么交易可正常进行。gasUsed表示交易实际花费的gas值总和，对于一笔交易而言，交易所花费的实际费用总额为gasUsed×gasPrice。交易完成后，如果交易的gas未全部消耗完，则这些剩下的gas将返还给发送者；若在执行交易过程中，用户发送的gas值不足够完成交易全部动作而导致gas被耗尽，那么该笔交易涉及到的所有的状态将会被回滚到初始状态，
电子科技大学硕士学位论文12图2-4以太坊虚拟机常用汇编指令图2.2.4智能合约的工作过程智能合约的工作过程分为如下三步[42]。（1）智能合约的构建与部署。首先，用户注册为以太坊账户，获得一个公私钥对，公钥的后20个字节字符串为地址，表示该账户在以太坊网络中的账户地址；私钥为一串16进制字符串，是鉴定用户的唯一标识。然后用户根据实际需求与其他用户协商好合约内容，再使用solidity编程语言实现合约代码；最后，如图2-5所示，用户根据协商内容确定合约代码无误后，调用SOLC编译器将合约代码编译成EVM虚拟机字节码，然后将EVM虚拟机字节码通过RPC接口发送到以太坊网络。图2-5智能合约部署流程图
【参考文献】：
期刊论文
[1]基于符号执行的智能合约漏洞检测方案[J]. 赵伟,张问银,王九如,王海峰,武传坤. 计算机应用. 2020(04)
[2]形式化验证方法浅析[J]. 陈波,李夫明. 电脑知识与技术. 2019(34)
[3]符号执行中的约束求解问题研究进展[J]. 邹权臣,吴润浦,马金鑫,王欣,辛伟,侯长玉,李美聪. 北京理工大学学报. 2019(09)
[4]基于混合分析的二进制程序控制流图构建方法[J]. 朱凯龙,陆余良,黄晖,邓兆琨,邓一杰. 浙江大学学报(工学版). 2019(05)
[5]智能合约安全漏洞挖掘技术研究[J]. 付梦琳,吴礼发,洪征,冯文博. 计算机应用. 2019(07)
[6]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
[7]符号执行研究综述[J]. 叶志斌,严波. 计算机科学. 2018(S1)
[8]《区块链：从数字货币到信用社会》[J]. 长铗,韩锋. 国企管理. 2018(07)
[9]SMT求解技术的发展及最新应用研究综述[J]. 王翀,吕荫润,陈力,王秀利,王永吉. 计算机研究与发展. 2017(07)
[10]区块链技术与应用前瞻综述[J]. 何蒲,于戈,张岩峰,鲍玉斌. 计算机科学. 2017(04)
本文编号：3476653
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/3476653.html
