隨著以太坊的蓬勃發(fā)展,智能合約作為以太坊區(qū)塊鏈的核心,其安全性逐漸受到大眾的重視。但應(yīng)用場(chǎng)景的逐漸豐富,使得智能合約的代碼量和復(fù)雜度也逐步遞增。這使得測(cè)試或者人工分析這類傳統(tǒng)的安全審計(jì)方法無法滿足當(dāng)前智能合約開發(fā)過程中的安全需求。形式化驗(yàn)證以數(shù)學(xué)理論為基礎(chǔ)被大眾認(rèn)可為最為可靠的安全驗(yàn)證方法并且廣泛的被運(yùn)用在計(jì)算機(jī)的軟硬件安全領(lǐng)域中。本文采用形式化驗(yàn)證中的定理證明方法對(duì)智能合約的合約代碼分別從源代碼和字節(jié)碼,這兩個(gè)角度進(jìn)行形式化建模與驗(yàn)證,通過對(duì)智能合約的程序規(guī)范的形式化定義及證明來驗(yàn)證智能合約的安全性。結(jié)合以太坊的底層實(shí)現(xiàn)和其技術(shù)特點(diǎn),本文給出了智能合約不同驗(yàn)證場(chǎng)景下的形式化驗(yàn)證方法,并設(shè)計(jì)了以太坊智能合約的形式化驗(yàn)證的驗(yàn)證框架,可以滿足基于源代碼和基于字節(jié)碼的兩種智能合約組織形式的形式化驗(yàn)證需求。通過驗(yàn)證框架詳細(xì)描述了兩種驗(yàn)證模式下的智能合約的驗(yàn)證流程,包括智能合約的形式化規(guī)范獲取、智能合約的形式化建模、智能合約待驗(yàn)證定理和智能合約定理證明。智能合約的形式化驗(yàn)證的實(shí)現(xiàn)主要包含在輔助定理證明工具中分別構(gòu)建關(guān)于solidity和字節(jié)碼的推理系統(tǒng)。在推理系統(tǒng)中建模了以太坊運(yùn)行環(huán)境,包括了運(yùn)...

【文章頁數(shù)】：110 頁

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
abstract
第一章 緒論
    1.1 研究背景與意義
    1.2 國(guó)內(nèi)外研究現(xiàn)狀
    1.3 本論文的結(jié)構(gòu)安排
第二章 相關(guān)理論、工具與平臺(tái)
    2.1 以太坊
        2.1.1 世界狀態(tài)
        2.1.2 合約交易
        2.1.3 以太坊區(qū)塊
        2.1.4 EVM
    2.2 形式化方法
    2.3 Coq
        2.3.1 Coq系統(tǒng)架構(gòu)
        2.3.2 基礎(chǔ)語法
        2.3.3 命題與證明
    2.4 Isabelle
        2.4.1 Isabelle的系統(tǒng)結(jié)構(gòu)
        2.4.2 Isabelle的理論創(chuàng)建
    2.5 本章小結(jié)
第三章 以太坊智能合約形式化驗(yàn)證方法
    3.1 智能合約的安全屬性
    3.2 智能合約的形式化驗(yàn)證對(duì)象
    3.3 智能合約的形式化驗(yàn)證框架
    3.4 智能合約的形式化驗(yàn)證流程
        3.4.1 基于源代碼的智能合約建模
        3.4.2 基于字節(jié)碼的智能合約建模
    3.5 本章小結(jié)
第四章 面向SOLIDITY語言的形式化建模
    4.1 Solidity形式化語法集
        4.1.1 類型與操作數(shù)集
        4.1.2 表達(dá)式類型
        4.1.3 語句類型
    4.2 函數(shù)模型的解釋執(zhí)行
        4.2.1 狀態(tài)模型
        4.2.2 函數(shù)語句級(jí)解釋執(zhí)行
        4.2.3 語句內(nèi)表達(dá)式的運(yùn)算
    4.3 本章小結(jié)
第五章 字節(jié)碼的形式化建模
    5.1 形式化操作碼
    5.2 虛擬機(jī)狀態(tài)建模
        5.2.1 世界狀態(tài)
        5.2.2 交易狀態(tài)
        5.2.3 區(qū)塊狀態(tài)
        5.2.4 執(zhí)行模型狀態(tài)
    5.3 操作碼的抽象解釋
        5.3.1 操作碼的形式語義
        5.3.2 操作碼的狀態(tài)斷言
        5.3.3 操作碼的形式語義實(shí)例
    5.4 操作碼序列的解釋執(zhí)行
        5.4.1 智能合約的霍爾三元組
        5.4.2 操作碼塊的抽取
        5.4.3 操作碼塊的霍爾三元組
    5.5 本章小結(jié)
第六章 智能合約形式化驗(yàn)證實(shí)驗(yàn)
    6.1 源代碼驗(yàn)證實(shí)例
        6.1.1 捐贈(zèng)合約
        6.1.2 合約形式化模型
        6.1.3 函數(shù)屬性與證明
    6.2 字節(jié)碼驗(yàn)證實(shí)例
        6.2.1 代幣合約
        6.2.2 合約形式化模型
        6.2.3 函數(shù)規(guī)范及證明
    6.3 工具驗(yàn)證效果對(duì)比
        6.3.1 對(duì)比特征
        6.3.2 對(duì)比分析
    6.4 本章小結(jié)
第七章 全文總結(jié)與展望
    7.1 全文總結(jié)
    7.2 后續(xù)工作展望
致謝
參考文獻(xiàn)
攻讀碩士學(xué)位期間取得的成果



本文編號(hào)：3880326