以太坊代币智能合约形式化验证技术研究
发布时间：2020-12-31 07:55
随着以太坊区块链的发展,智能合约作为以太坊的核心技术也得到越来越多的应用,其中应用之一是用户通过代币智能合约进行新代币的开发。除以太币外,在以太坊主流代币标准协议ERC20的基础上,以太坊支持用户通过代币智能合约完成代币的构建发行、管理和交易。代币智能合约种类多,持有大量资金,易受到攻击者的攻击。目前代币智能合约已曝出存在多种类型的漏洞,也发生被攻击的安全事件,造成大量损失,因此保证合约的安全性并对合约进行安全审计是非常必要的。形式化验证方法是专门针对协议或系统的安全性所提出的一种检验分析方法,能够更全面、深入地研究合约的安全性。针对代币智能合约的安全问题,本文以代币智能合约的形式化建模与验证为研究重点,结合以太坊目前主流的ERC20代币标准协议,提出了面向ERC20标准的代币智能合约形式化模型,并将形式化模型应用到对代币智能合约造成威胁的高危漏洞的形式化分析中。具体研究内容如下:1.针对代币智能合约形式化建模的需求,提出了面向ERC20标准的代币智能合约形式化模型框架。描述了模型定义的具体函数行为和攻击者模型,对合约中函数行为进行抽象,利用多集合重写规则定义代币智能合约的建模规则。针...
【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校
【文章页数】：84 页
【学位级别】：硕士
【部分图文】：
图２．１以太坊整体架构??以太坊平台中的应用基于以太坊智能合约开展，智能合约像是一个以太坊??
?第２章相关技术???号，用户无法自定义其他的符号，这些符号可以表示积分、财产等。因此在以太??坊中，除了原生货币以太币之外，用户可开发新的代币以满足其不同的需求。??２．１．１以太坊区块??以太坊中的数据会被通过文件的形式永久存储记录，这些文件被称为以太??坊区块［３Ｇ］。区块可看作一种数据结构，区块上记录了在一段时间内产生的交易??和状态更变的结果。各种操作执行交易产生的各种信息存放在区块中，并通过指??针和前一个区块相连。以太坊区块主要由区块头和区块体构成，区块结构如下??图２．２所示。此外，我们用两个值来识别区块：区块头哈希值和区块高度。??区块头??版本号?时间敝?Ｍｅｒｋｌｅ根随机数??区块体???交易数Ｍ???交易?交易?｜交易?交易?交易?交易??图２．２区块结构示意图??区块头是区块的核心组成部分，区块头包括上一区块的哈希值、时间戳、??Ｍｅｒｋｌｅ根等相关信息，区块头详细结构和含义如表２．１所示。区块体中包含本区??块中所有和交易相关的信息，以太坊中交易是整体架构中的重要组成部分，交易??将以太坊中的账户连接起来，可实现资产价值的传递和转移。区块体详细结构和??含义如表２．２所示。??表２．１区块头详细结构??字段名?描述含义??版本?版本号，用于跟踪更新???区块哈希值－?引用链中前一区块的哈希值??时间戳?＾?该区块产生的近似时间??Ｍｅｒｋｌｅ根?该区块中有关交易的Ｍｅｒｋｌｅ根的哈希值??￣￣随机数?用于工作量证明的计数器??以太坊中的交易主要是指将交易从一个账户发送到另一个账户，交易主要??１０??
?包含发送者的签名、接收者签名、发送的金额数量等内容。交易中定义了交易费??用这样一个概念，交易费用由ｇａｓ表示，主要是为了防止用户在链中发送太多无??意义的交易，因此每一笔交易需要付出一定的代价。用户发送一笔交易时需要支??付一定的ｇａｓ费用用于这笔交易的执行，当执行一笔交易需要复杂繁琐的计算步??骤时，这笔交易消耗的ｇａｓ越多。交易执行完成后，支付的ｇａｓ若没有被消耗完，??则会返还给发起这笔交易的账户中。??２．１．２以太坊账户??以太坊中有两种账户：外部账户和合约账户。如图２．３所示，外部账户是由密??钥控制的账户，有账户余额，无代码，能触发交易，包括转账或执行合约。合约账??户是由代码控制的，有账户余额，有代码，能被触发执行智能合约代码，在合约??创建后自动运行。以太坊的账户信息本质上是由ｎｏｎｃｅ、ｂａｌａｎｃｅ、ｃｏｄｅＨａｓｈ、??ｓｔｏｒａｇｅＲｏｏｔ组成的一个数据结构。??合约账户??外部账户????Ｉ丨代码Ｉ???；?［??????ｎｏｎｃｅ?ｂａｌａｎｃｅ?ｎｏｎｃｅ?ｂａｌａｎｃｅ??ｓｔｏｒａｇｅ?ｃｏｄｅＨａ?ｓｔｏｒａｇｅ?ｃｏｄｅｌｌａ??Ｒｏｏｔ?ｓｈ?Ｒ〇〇ｔ?｜?ｓｈ??图２．３以太坊账户示意图??（１）?ｎｏｎｃｅ：当前账户发出的消息计数器，指账户发出过多少次交易。??１１??
本文编号：2949265
【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校
【文章页数】：84 页
【学位级别】：硕士
【部分图文】：
图２．１以太坊整体架构??以太坊平台中的应用基于以太坊智能合约开展，智能合约像是一个以太坊??
?第２章相关技术???号，用户无法自定义其他的符号，这些符号可以表示积分、财产等。因此在以太??坊中，除了原生货币以太币之外，用户可开发新的代币以满足其不同的需求。??２．１．１以太坊区块??以太坊中的数据会被通过文件的形式永久存储记录，这些文件被称为以太??坊区块［３Ｇ］。区块可看作一种数据结构，区块上记录了在一段时间内产生的交易??和状态更变的结果。各种操作执行交易产生的各种信息存放在区块中，并通过指??针和前一个区块相连。以太坊区块主要由区块头和区块体构成，区块结构如下??图２．２所示。此外，我们用两个值来识别区块：区块头哈希值和区块高度。??区块头??版本号?时间敝?Ｍｅｒｋｌｅ根随机数??区块体???交易数Ｍ???交易?交易?｜交易?交易?交易?交易??图２．２区块结构示意图??区块头是区块的核心组成部分，区块头包括上一区块的哈希值、时间戳、??Ｍｅｒｋｌｅ根等相关信息，区块头详细结构和含义如表２．１所示。区块体中包含本区??块中所有和交易相关的信息，以太坊中交易是整体架构中的重要组成部分，交易??将以太坊中的账户连接起来，可实现资产价值的传递和转移。区块体详细结构和??含义如表２．２所示。??表２．１区块头详细结构??字段名?描述含义??版本?版本号，用于跟踪更新???区块哈希值－?引用链中前一区块的哈希值??时间戳?＾?该区块产生的近似时间??Ｍｅｒｋｌｅ根?该区块中有关交易的Ｍｅｒｋｌｅ根的哈希值??￣￣随机数?用于工作量证明的计数器??以太坊中的交易主要是指将交易从一个账户发送到另一个账户，交易主要??１０??
?包含发送者的签名、接收者签名、发送的金额数量等内容。交易中定义了交易费??用这样一个概念，交易费用由ｇａｓ表示，主要是为了防止用户在链中发送太多无??意义的交易，因此每一笔交易需要付出一定的代价。用户发送一笔交易时需要支??付一定的ｇａｓ费用用于这笔交易的执行，当执行一笔交易需要复杂繁琐的计算步??骤时，这笔交易消耗的ｇａｓ越多。交易执行完成后，支付的ｇａｓ若没有被消耗完，??则会返还给发起这笔交易的账户中。??２．１．２以太坊账户??以太坊中有两种账户：外部账户和合约账户。如图２．３所示，外部账户是由密??钥控制的账户，有账户余额，无代码，能触发交易，包括转账或执行合约。合约账??户是由代码控制的，有账户余额，有代码，能被触发执行智能合约代码，在合约??创建后自动运行。以太坊的账户信息本质上是由ｎｏｎｃｅ、ｂａｌａｎｃｅ、ｃｏｄｅＨａｓｈ、??ｓｔｏｒａｇｅＲｏｏｔ组成的一个数据结构。??合约账户??外部账户????Ｉ丨代码Ｉ???；?［??????ｎｏｎｃｅ?ｂａｌａｎｃｅ?ｎｏｎｃｅ?ｂａｌａｎｃｅ??ｓｔｏｒａｇｅ?ｃｏｄｅＨａ?ｓｔｏｒａｇｅ?ｃｏｄｅｌｌａ??Ｒｏｏｔ?ｓｈ?Ｒ〇〇ｔ?｜?ｓｈ??图２．３以太坊账户示意图??（１）?ｎｏｎｃｅ：当前账户发出的消息计数器，指账户发出过多少次交易。??１１??
本文编号：2949265
本文链接：https://www.wllwen.com/guanlilunwen/bankxd/2949265.html
