基于以太坊智能合约的形式化验证技术研究与实现

发布时间：2024-01-19 19:12

　　随着以太坊的蓬勃发展,智能合约作为以太坊区块链的核心,其安全性逐渐受到大众的重视。但应用场景的逐渐丰富,使得智能合约的代码量和复杂度也逐步递增。这使得测试或者人工分析这类传统的安全审计方法无法满足当前智能合约开发过程中的安全需求。形式化验证以数学理论为基础被大众认可为最为可靠的安全验证方法并且广泛的被运用在计算机的软硬件安全领域中。本文采用形式化验证中的定理证明方法对智能合约的合约代码分别从源代码和字节码,这两个角度进行形式化建模与验证,通过对智能合约的程序规范的形式化定义及证明来验证智能合约的安全性。结合以太坊的底层实现和其技术特点,本文给出了智能合约不同验证场景下的形式化验证方法,并设计了以太坊智能合约的形式化验证的验证框架,可以满足基于源代码和基于字节码的两种智能合约组织形式的形式化验证需求。通过验证框架详细描述了两种验证模式下的智能合约的验证流程,包括智能合约的形式化规范获取、智能合约的形式化建模、智能合约待验证定理和智能合约定理证明。智能合约的形式化验证的实现主要包含在辅助定理证明工具中分别构建关于solidity和字节码的推理系统。在推理系统中建模了以太坊运行环境,包括了运...

【文章页数】：110 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
第一章 绪论
    1.1 研究背景与意义
    1.2 国内外研究现状
    1.3 本论文的结构安排
第二章 相关理论、工具与平台
    2.1 以太坊
        2.1.1 世界状态
        2.1.2 合约交易
        2.1.3 以太坊区块
        2.1.4 EVM
    2.2 形式化方法
    2.3 Coq
        2.3.1 Coq系统架构
        2.3.2 基础语法
        2.3.3 命题与证明
    2.4 Isabelle
        2.4.1 Isabelle的系统结构
        2.4.2 Isabelle的理论创建
    2.5 本章小结
第三章 以太坊智能合约形式化验证方法
    3.1 智能合约的安全属性
    3.2 智能合约的形式化验证对象
    3.3 智能合约的形式化验证框架
    3.4 智能合约的形式化验证流程
        3.4.1 基于源代码的智能合约建模
        3.4.2 基于字节码的智能合约建模
    3.5 本章小结
第四章 面向SOLIDITY语言的形式化建模
    4.1 Solidity形式化语法集
        4.1.1 类型与操作数集
        4.1.2 表达式类型
        4.1.3 语句类型
    4.2 函数模型的解释执行
        4.2.1 状态模型
        4.2.2 函数语句级解释执行
        4.2.3 语句内表达式的运算
    4.3 本章小结
第五章 字节码的形式化建模
    5.1 形式化操作码
    5.2 虚拟机状态建模
        5.2.1 世界状态
        5.2.2 交易状态
        5.2.3 区块状态
        5.2.4 执行模型状态
    5.3 操作码的抽象解释
        5.3.1 操作码的形式语义
        5.3.2 操作码的状态断言
        5.3.3 操作码的形式语义实例
    5.4 操作码序列的解释执行
        5.4.1 智能合约的霍尔三元组
        5.4.2 操作码块的抽取
        5.4.3 操作码块的霍尔三元组
    5.5 本章小结
第六章 智能合约形式化验证实验
    6.1 源代码验证实例
        6.1.1 捐赠合约
        6.1.2 合约形式化模型
        6.1.3 函数属性与证明
    6.2 字节码验证实例
        6.2.1 代币合约
        6.2.2 合约形式化模型
        6.2.3 函数规范及证明
    6.3 工具验证效果对比
        6.3.1 对比特征
        6.3.2 对比分析
    6.4 本章小结
第七章 全文总结与展望
    7.1 全文总结
    7.2 后续工作展望
致谢
参考文献
攻读硕士学位期间取得的成果



本文编号：3880326