以太坊代币智能合约形式化验证技术研究

目录

声明

摘要

第1章绪论

1．1研究背景及意义

1．2国内外研究现状

1．2．1基于符号执行的方法

1．2．2基于软件测试的方法

1．2．3基于形式化验证的方法

1．2．4研究现状总结

1．3主要研究内容

1．4本论文结构安排

第2章相关技术

2．1以太坊相关技术

2．1．1 以太坊区块

2．1．2以太坊账户

2．1．3以太坊虚拟机

2．1．4 gas机制

2．2代币标准协议

2．3形式化验证研究

2．3．1形式化方法

2．3．2形式化验证工具

2．4本章小结

第3章代币智能合约的形式化建模

3．1 形式化分析对象和流程

3．2模型定义

3．3 安全属性

3．3．1 基本属性

3．3．2 交易属性

3．3．3权限属性

3．4攻击者模型

3．5建模分析

3．5．1 建模方法

3．5．2约束规则

3．5．3建模规则

3．6本章小结

第4章代币智能合约中整数溢出漏洞的形式化建模分析

4．1 整数溢出漏洞攻击原理

4．2整数溢出漏洞安全属性

4．3攻击者模型分析

4．4整数溢出漏洞的形式化建模

4．4．1建模难点

4．4．2建模过程

4．5整数溢出漏洞的改进措施

4．6本章小结

第5章代币智能合约中重入漏洞的形式化建模研究

5．1 重入漏洞攻击原理

5．2重入漏洞安全属性和攻击者模型

5．3重入漏洞的建模过程分析

5．3．1 建模难点

5．3．2建模过程

5．4重入漏洞的改进措施

5．5本章小结

第6章形式化验证实验与分析

6．1 方案概述

6．2实验结果与分析

6．2．1 ERC20代币合约实例验证

6．2．2整数溢出漏洞验证实验

6．2．3重入漏洞形式化验证实验

6．3本章小结

第7章总结与展望

7．1 本文主要研究工作及总结

7．2未来展望

参考文献

致谢

在读期间发表的学术论文与取得的研究成果